From ef236eeddc81176672ac8c3d3a71d938fe31317c Mon Sep 17 00:00:00 2001
From: Jannis Harder <me@jix.one>
Date: Fri, 1 Apr 2022 19:25:09 +0200
Subject: [PATCH] Regression test: do not merge FFs with unconstrained initvals

Currently done by `opt -keepdc` via `opt_merge` but not valid in a
formal context.
---
 tests/.gitignore                  |  1 +
 tests/invalid_ff_dcinit_merge.sby | 29 +++++++++++++++++++++++++++++
 2 files changed, 30 insertions(+)
 create mode 100644 tests/invalid_ff_dcinit_merge.sby

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