mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-04-24 01:25:33 +00:00
Code Activity

Added $assert/$assume support to AIGER back-end

Browse source
This commit is contained in:
Clifford Wolf 2016-12-03 13:20:29 +01:00
parent 37760541bd
commit a44cc7a3d1
3 changed files with 53 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

4
examples/aiger/demo.sh
View file

@ -4,11 +4,11 @@ yosys -p '
read_verilog -formal demo.v
prep -flatten -nordff -top demo
write_smt2 -wires demo.smt2
miter -assert demo
flatten demo; delete -output
memory_map; opt -full
techmap; opt -fast
abc -fast -g AND; opt_clean
write_aiger -miter -zinit -map demo.aim demo.aig
write_aiger -map demo.aim demo.aig
'
super_prove demo.aig > demo.aiw
yosys-smtbmc --dump-vcd demo.vcd --aig demo demo.smt2

2
examples/aiger/demo.v
View file

@ -4,7 +4,7 @@ module demo(input clk, reset, ctrl);
initial counter[NBITS-2] = 0;
initial counter[0] = 1;
always @(posedge clk) begin
counter <= reset ? 0 : ctrl ? counter + 1 : counter - 1;
counter <= reset ? 1 : ctrl ? counter + 1 : counter - 1;
assume(counter != 0);
assume(counter != 1 << (NBITS-1));
assert(counter != (1 << NBITS)-1);