diff --git a/tests/.gitignore b/tests/.gitignore index 21f5f780..f91f05ae 100644 --- a/tests/.gitignore +++ b/tests/.gitignore @@ -12,4 +12,5 @@ /submod_props*/ /multi_assert*/ /aim_vs_smt2_nonzero_start_offset*/ +/invalid_ff_dcinit_merge*/ /2props1trace*/ diff --git a/tests/invalid_ff_dcinit_merge.sby b/tests/invalid_ff_dcinit_merge.sby new file mode 100644 index 00000000..a23d8f02 --- /dev/null +++ b/tests/invalid_ff_dcinit_merge.sby @@ -0,0 +1,29 @@ +[options] +mode bmc +depth 4 +expect fail + +[engines] +smtbmc + +[script] +read -formal top.sv +prep -top top + +[file top.sv] +module top( +input clk, d +); + +reg q1; +reg q2; + +always @(posedge clk) begin + q1 <= d; + q2 <= d; +end; + +// q1 and q2 are unconstrained in the initial state, so this should fail +always @(*) assert(q1 == q2); + +endmodule