summaryrefslogtreecommitdiff
path: root/examples/aiger/demo.sh
diff options
context:
space:
mode:
Diffstat (limited to 'examples/aiger/demo.sh')
-rw-r--r--examples/aiger/demo.sh14
1 files changed, 14 insertions, 0 deletions
diff --git a/examples/aiger/demo.sh b/examples/aiger/demo.sh
new file mode 100644
index 00000000..8728b672
--- /dev/null
+++ b/examples/aiger/demo.sh
@@ -0,0 +1,14 @@
+#!/bin/bash
+set -ex
+yosys -p '
+ read_verilog -formal demo.v
+ prep -flatten -nordff -top demo
+ write_smt2 -wires demo.smt2
+ flatten demo; delete -output
+ memory_map; opt -full
+ techmap; opt -fast
+ abc -fast -g AND; opt_clean
+ write_aiger -map demo.aim demo.aig
+'
+super_prove demo.aig > demo.aiw
+yosys-smtbmc --dump-vcd demo.vcd --aig demo demo.smt2