quicklogic-sv-empty-param-workaround/examples/aiger/demo.sh

#!/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
Added examples/aiger/ 2016-12-01 13:42:17 +01:00			`#!/bin/bash`
			`set -ex`
			`yosys -p '`
			`read_verilog -formal demo.v`
			`prep -flatten -nordff -top demo`
			`write_smt2 -wires demo.smt2`
Added $assert/$assume support to AIGER back-end 2016-12-03 13:20:29 +01:00			`flatten demo; delete -output`
Added examples/aiger/ 2016-12-01 13:42:17 +01:00			`memory_map; opt -full`
			`techmap; opt -fast`
			`abc -fast -g AND; opt_clean`
Added $assert/$assume support to AIGER back-end 2016-12-03 13:20:29 +01:00			`write_aiger -map demo.aim demo.aig`
Added examples/aiger/ 2016-12-01 13:42:17 +01:00			`'`
			`super_prove demo.aig > demo.aiw`
			`yosys-smtbmc --dump-vcd demo.vcd --aig demo demo.smt2`