blob: caaa447619e826c4834efab1c9d191a36d439d51 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
#!/bin/bash
set -ex
yosys -p '
read_verilog -formal demo.v
prep -flatten -nordff -top demo
write_smt2 -wires demo.smt2
miter -assert demo
memory_map; opt -full
techmap; opt -fast
abc -fast -g AND; opt_clean
write_aiger -miter -zinit -map demo.aim demo.aig
'
super_prove demo.aig > demo.aiw
yosys-smtbmc --dump-vcd demo.vcd --aig demo demo.smt2
|