Merge pull request #170 from programmerjake/add-simcheck-option

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

sbysrc/sby_core.py

@@ -552,7 +552,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:
@@ -569,7 +569,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:
@@ -577,7 +577,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)
 
@@ -610,7 +610,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)
@@ -643,7 +643,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:
@@ -675,7 +675,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)

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

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