aboutsummaryrefslogtreecommitdiffstats
path: root/examples/aiger/demo.sh
diff options
context:
space:
mode:
Diffstat (limited to 'examples/aiger/demo.sh')
-rw-r--r--examples/aiger/demo.sh4
1 files changed, 2 insertions, 2 deletions
diff --git a/examples/aiger/demo.sh b/examples/aiger/demo.sh
index caaa44761..8728b6722 100644
--- a/examples/aiger/demo.sh
+++ b/examples/aiger/demo.sh
@@ -4,11 +4,11 @@ yosys -p '
read_verilog -formal demo.v
prep -flatten -nordff -top demo
write_smt2 -wires demo.smt2
- miter -assert demo
+ flatten demo; delete -output
memory_map; opt -full
techmap; opt -fast
abc -fast -g AND; opt_clean
- write_aiger -miter -zinit -map demo.aim demo.aig
+ write_aiger -map demo.aim demo.aig
'
super_prove demo.aig > demo.aiw
yosys-smtbmc --dump-vcd demo.vcd --aig demo demo.smt2