mirror of https://github.com/YosysHQ/yosys.git
Made examples/smtbmc/demo1.v more interesting
This commit is contained in:
parent
948aac9e1e
commit
068d5bc02f
|
@ -9,7 +9,7 @@ module demo1(input clk, input addtwo, output iseven);
|
||||||
|
|
||||||
`ifdef FORMAL
|
`ifdef FORMAL
|
||||||
assert property (cnt != 15);
|
assert property (cnt != 15);
|
||||||
initial assume (!cnt[3] && !cnt[0]);
|
initial assume (!cnt[2]);
|
||||||
`endif
|
`endif
|
||||||
endmodule
|
endmodule
|
||||||
|
|
||||||
|
|
Loading…
Reference in New Issue