2016-12-01 06:42:17 -06:00
|
|
|
#!/bin/bash
|
|
|
|
|
set -ex
|
|
|
|
|
yosys -p '
|
|
|
|
|
read_verilog -formal demo.v
|
|
|
|
|
prep -flatten -nordff -top demo
|
|
|
|
|
write_smt2 -wires demo.smt2
|
2016-12-03 06:20:29 -06:00
|
|
|
flatten demo; delete -output
|
2016-12-01 06:42:17 -06:00
|
|
|
memory_map; opt -full
|
|
|
|
|
techmap; opt -fast
|
|
|
|
|
abc -fast -g AND; opt_clean
|
2016-12-03 06:20:29 -06:00
|
|
|
write_aiger -map demo.aim demo.aig
|
2016-12-01 06:42:17 -06:00
|
|
|
'
|
|
|
|
|
super_prove demo.aig > demo.aiw
|
|
|
|
|
yosys-smtbmc --dump-vcd demo.vcd --aig demo demo.smt2
|
