summaryrefslogtreecommitdiff
path: root/examples/aiger/demo.sh
blob: 8728b6722a1bdd6e6e27b1363179075e11f7a02d (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
	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