6 abcprog
="../../yosys-abc" # default to built-in version of abc
10 A
) abcprog
="$OPTARG" ;;
15 # NB: *.aag and *.aig must contain a symbol table naming the primary
16 # inputs and outputs, otherwise ABC and Yosys will name them
17 # arbitrarily (and inconsistently with each other).
20 # Since ABC cannot read *.aag, read the *.aig instead
21 # (which would have been created by the reference aig2aig utility,
22 # available from http://fmv.jku.at/aiger/)
24 $abcprog -q "read -c ${aag%.*}.aig; write ${aag%.*}_ref.v"
26 read_verilog ${aag%.*}_ref.v
29 read_aiger -clk_name clock $aag
32 design -import gold -as gold
33 design -import gate -as gate
34 miter -equiv -flatten -make_assert -make_outputs gold gate miter
35 sat -verify -prove-asserts -show-ports -seq 16 miter
41 $abcprog -q "read -c $aig; write ${aig%.*}_ref.v"
43 read_verilog ${aig%.*}_ref.v
46 read_aiger -clk_name clock $aig
49 design -import gold -as gold
50 design -import gate -as gate
51 miter -equiv -flatten -make_assert -make_outputs gold gate miter
52 sat -verify -prove-asserts -show-ports -seq 16 miter
58 ..
/..
/yosys
-ql ${y%.*}.log
$y