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

Fixes: #168
Depends on: https://github.com/YosysHQ/yosys/pull/3391

diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py
index ab10614fc6906f0594dfc2b748d0dbbc91c76f8e..3592c31addef97b3052b253ce10265b1f9eda854 100644 (file)
--- 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 (file)
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 (file)
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