From: Jannis Harder <me@jix.one>
Date: Wed, 29 Jun 2022 16:00:52 +0000 (+0200)
Subject: test uninited FFs with const clks and fix btor script for this
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ff802086b4b1b9d9ca0c74fd5fa521b5316bbe4c;p=SymbiYosys.git

test uninited FFs with const clks and fix btor script for this
---

diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py
index 4e57b21..5580d09 100644
--- a/sbysrc/sby_core.py
+++ b/sbysrc/sby_core.py
@@ -653,7 +653,7 @@ class SbyTask(SbyConfig):
                     print("abc", file=f)
                     print("opt_clean", file=f)
                 else:
-                    print("opt -fast", file=f)
+                    print("opt -fast -keepdc", file=f)
                 print("delete -output", file=f)
                 print("dffunmap", file=f)
                 print("stat", file=f)
diff --git a/tests/regression/const_clocks.sby b/tests/regression/const_clocks.sby
new file mode 100644
index 0000000..245358b
--- /dev/null
+++ b/tests/regression/const_clocks.sby
@@ -0,0 +1,43 @@
+[tasks]
+btor
+smt
+btor_m btor multiclock
+smt_m smt multiclock
+
+[options]
+mode bmc
+
+multiclock: multiclock on
+
+[engines]
+#smtbmc
+btor: btor btormc
+smt: smtbmc boolector
+
+[script]
+read_verilog -formal const_clocks.sv
+prep -flatten -top top
+
+[file const_clocks.sv]
+module top(
+    input clk,
+    input [7:0] d
+);
+
+    (* keep *)
+    wire [7:0] some_const = $anyconst;
+
+    wire [7:0] q;
+
+    ff ff1(.clk(1'b0), .d(d), .q(q));
+
+    initial assume (some_const == q);
+    initial assume (q != 0);
+
+
+    always @(posedge clk) assert(some_const == q);
+endmodule
+
+module ff(input clk, input [7:0] d, (* keep *) output reg [7:0] q);
+    always @(posedge clk) q <= d;
+endmodule