2 all: demo1 demo2 demo3 demo4 demo5 demo6 demo7 demo8 demo9
5 yosys-smtbmc
--dump-vcd demo1.vcd demo1.smt2
6 yosys-smtbmc
-i
--dump-vcd demo1.vcd demo1.smt2
9 yosys-smtbmc
-g
--dump-vcd demo2.vcd
--dump-smtc demo2.smtc
--dump-vlogtb demo2_tb.v demo2.smt2
10 iverilog
-g2012
-o demo2_tb demo2_tb.v demo2.v
11 vvp demo2_tb
+vcd
=demo2_tb.vcd
14 yosys-smtbmc
--dump-vcd demo3.vcd
--smtc demo3.smtc demo3.smt2
17 yosys-smtbmc
-s yices
--dump-vcd demo4.vcd
--smtc demo4.smtc demo4.smt2
20 yosys-smtbmc
-g
-t
50 --dump-vcd demo5.vcd demo5.smt2
23 yosys-smtbmc
-t
1 demo6.smt2
26 yosys-smtbmc
-t
10 demo7.smt2
29 yosys-smtbmc
-s z3
-t
1 -g demo8.smt2
32 yosys-smtbmc
-s z3
-t
1 -g demo9.smt2
35 yosys
-ql demo1.yslog
-p
'read_verilog -formal demo1.v; prep -top demo1 -nordff; write_smt2 -wires demo1.smt2'
38 yosys
-ql demo2.yslog
-p
'read_verilog -formal demo2.v; prep -top demo2 -nordff; write_smt2 -wires demo2.smt2'
41 yosys
-ql demo3.yslog
-p
'read_verilog -formal demo3.v; prep -top demo3 -nordff; write_smt2 -wires demo3.smt2'
44 yosys
-ql demo4.yslog
-p
'read_verilog -formal demo4.v; prep -top demo4 -nordff; write_smt2 -wires demo4.smt2'
47 yosys
-ql demo5.yslog
-p
'read_verilog -formal demo5.v; prep -top demo5 -nordff; write_smt2 -wires demo5.smt2'
50 yosys
-ql demo6.yslog
-p
'read_verilog demo6.v; prep -top demo6 -nordff; assertpmux; opt -keepdc -fast; write_smt2 -wires demo6.smt2'
53 yosys
-ql demo7.yslog
-p
'read_verilog -formal demo7.v; prep -top demo7 -nordff; write_smt2 -wires demo7.smt2'
56 yosys
-ql demo8.yslog
-p
'read_verilog -formal demo8.v; prep -top demo8 -nordff; write_smt2 -stbv -wires demo8.smt2'
59 yosys
-ql demo9.yslog
-p
'read_verilog -formal demo9.v; prep -top demo9 -nordff; write_smt2 -stbv -wires demo9.smt2'
62 rm -f demo1.yslog demo1.smt2 demo1.vcd
63 rm -f demo2.yslog demo2.smt2 demo2.vcd demo2.smtc demo2_tb.v demo2_tb demo2_tb.vcd
64 rm -f demo3.yslog demo3.smt2 demo3.vcd
65 rm -f demo4.yslog demo4.smt2 demo4.vcd
66 rm -f demo5.yslog demo5.smt2 demo5.vcd
67 rm -f demo6.yslog demo6.smt2
68 rm -f demo7.yslog demo7.smt2
69 rm -f demo8.yslog demo8.smt2
70 rm -f demo9.yslog demo9.smt2
72 .PHONY
: demo1 demo2 demo3 demo4 demo5 demo6 demo7 demo8 demo9
clean