mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-11-03 21:09:12 +00:00
Code Activity

Use ABC to convert AIGER to Verilog, then sat against Yosys

Browse source
This commit is contained in:
Eddie Hung 2019-06-07 11:05:36 -07:00
parent 1b113a0574
commit ebe29b6659
1 changed files with 15 additions and 21 deletions
Download patch file Download diff file Expand all files Collapse all files

36
tests/aiger/run-test.sh
View file

@ -1,24 +1,18 @@
#!/bin/bash #!/bin/bash
OPTIND=1 set -e
seed="" # default to no seed specified for aig in *.aig; do
while getopts "S:" opt ../../yosys-abc -c "read -c $aig; write ${aig%.*}_ref.v"
do ../../yosys -p "
case "$opt" in read_verilog ${aig%.*}_ref.v
S) arg="${OPTARG#"${OPTARG%%[![:space:]]*}"}" # remove leading space prep
seed="SEED=$arg" ;; design -stash gold
esac read_aiger -clk_name clock $aig
prep
design -stash gate
design -import gold -as gold
design -import gate -as gate
miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -show-ports -seq 16 miter
"
done done
shift "$((OPTIND-1))"
# check for Icarus Verilog
if ! which iverilog > /dev/null ; then
echo "$0: Error: Icarus Verilog 'iverilog' not found."
exit 1
fi
echo "===== AAG ======"
${MAKE:-make} -f ../tools/autotest.mk $seed *.aag EXTRA_FLAGS="-f aiger"
echo "===== AIG ======"
exec ${MAKE:-make} -f ../tools/autotest.mk $seed *.aig EXTRA_FLAGS="-f aiger"