From: Jacob Lifshay <programmerjake@gmail.com>
Date: Thu, 23 Jun 2022 04:17:29 +0000 (-0700)
Subject: switch to using hierarchy -smtcheck for smtlib2 solvers, allowing smtlib2_module... 
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=refs%2Fheads%2Fadd-simcheck-option;p=SymbiYosys.git

switch to using hierarchy -smtcheck for smtlib2 solvers, allowing smtlib2_module modules.

Fixes: #168

Depends on: https://github.com/YosysHQ/yosys/pull/3391
---

diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py
index ab10614..3592c31 100644
--- a/sbysrc/sby_core.py
+++ b/sbysrc/sby_core.py
@@ -465,7 +465,7 @@ class SbyTask(SbyConfig):
         if not os.path.isdir(f"{self.workdir}/model"):
             os.makedirs(f"{self.workdir}/model")
 
-        def print_common_prep():
+        def print_common_prep(check):
             if self.opt_multiclock:
                 print("clk2fflogic", file=f)
             else:
@@ -482,7 +482,7 @@ class SbyTask(SbyConfig):
             print("setundef -anyseq", file=f)
             print("opt -keepdc -fast", file=f)
             print("check", file=f)
-            print("hierarchy -simcheck", file=f)
+            print(f"hierarchy {check}", file=f)
 
         if model_name == "base":
             with open(f"""{self.workdir}/model/design.ys""", "w") as f:
@@ -490,7 +490,7 @@ class SbyTask(SbyConfig):
                 for cmd in self.script:
                     print(cmd, file=f)
                 # the user must designate a top module in [script]
-                print("hierarchy -simcheck", file=f)
+                print("hierarchy -smtcheck", file=f)
                 print(f"""write_jny -no-connections ../model/design.json""", file=f)
                 print(f"""write_rtlil ../model/design.il""", file=f)
 
@@ -522,7 +522,7 @@ class SbyTask(SbyConfig):
                     print("memory_map", file=f)
                 else:
                     print("memory_nordff", file=f)
-                print_common_prep()
+                print_common_prep("-smtcheck")
                 if "_syn" in model_name:
                     print("techmap", file=f)
                     print("opt -fast", file=f)
@@ -555,7 +555,7 @@ class SbyTask(SbyConfig):
                     print("memory_map", file=f)
                 else:
                     print("memory_nordff", file=f)
-                print_common_prep()
+                print_common_prep("-simcheck")
                 print("flatten", file=f)
                 print("setundef -undriven -anyseq", file=f)
                 if "_syn" in model_name:
@@ -587,7 +587,7 @@ class SbyTask(SbyConfig):
                 print(f"# running in {self.workdir}/model/", file=f)
                 print("read_ilang design.il", file=f)
                 print("memory_map", file=f)
-                print_common_prep()
+                print_common_prep("-simcheck")
                 print("flatten", file=f)
                 print("setundef -undriven -anyseq", file=f)
                 print("setattr -unset keep", file=f)
diff --git a/tests/unsorted/blackbox.sby b/tests/unsorted/blackbox.sby
new file mode 100644
index 0000000..ca9400e
--- /dev/null
+++ b/tests/unsorted/blackbox.sby
@@ -0,0 +1,31 @@
+[options]
+mode bmc
+depth 1
+expect error
+
+[engines]
+smtbmc
+
+[script]
+read_verilog -formal test.v
+prep -top top
+
+[file test.v]
+(* blackbox *)
+module submod(a, b);
+	input [7:0] a;
+	output [7:0] b;
+endmodule
+
+module top;
+	wire [7:0] a = $anyconst, b;
+
+	submod submod(
+		.a(a),
+		.b(b)
+	);
+
+	always @* begin
+		assert(~a == b);
+	end
+endmodule
diff --git a/tests/unsorted/smtlib2_module.sby b/tests/unsorted/smtlib2_module.sby
new file mode 100644
index 0000000..43dfcb2
--- /dev/null
+++ b/tests/unsorted/smtlib2_module.sby
@@ -0,0 +1,32 @@
+[options]
+mode bmc
+depth 1
+
+[engines]
+smtbmc
+
+[script]
+read_verilog -formal test.v
+prep -top top
+
+[file test.v]
+(* blackbox *)
+(* smtlib2_module *)
+module submod(a, b);
+	input [7:0] a;
+	(* smtlib2_comb_expr = "(bvnot a)" *)
+	output [7:0] b;
+endmodule
+
+module top;
+	wire [7:0] a = $anyconst, b;
+
+	submod submod(
+		.a(a),
+		.b(b)
+	);
+
+	always @* begin
+		assert(~a == b);
+	end
+endmodule