Fixes: #168
Depends on: https://github.com/YosysHQ/yosys/pull/3391
if not os.path.isdir(f"{self.workdir}/model"):
os.makedirs(f"{self.workdir}/model")
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:
if self.opt_multiclock:
print("clk2fflogic", file=f)
else:
print("setundef -anyseq", file=f)
print("opt -keepdc -fast", file=f)
print("check", file=f)
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:
if model_name == "base":
with open(f"""{self.workdir}/model/design.ys""", "w") as f:
for cmd in self.script:
print(cmd, file=f)
# the user must designate a top module in [script]
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)
print(f"""write_jny -no-connections ../model/design.json""", file=f)
print(f"""write_rtlil ../model/design.il""", file=f)
print("memory_map", file=f)
else:
print("memory_nordff", file=f)
print("memory_map", file=f)
else:
print("memory_nordff", file=f)
+ print_common_prep("-smtcheck")
if "_syn" in model_name:
print("techmap", file=f)
print("opt -fast", file=f)
if "_syn" in model_name:
print("techmap", file=f)
print("opt -fast", file=f)
print("memory_map", file=f)
else:
print("memory_nordff", file=f)
print("memory_map", file=f)
else:
print("memory_nordff", file=f)
+ print_common_prep("-simcheck")
print("flatten", file=f)
print("setundef -undriven -anyseq", file=f)
if "_syn" in model_name:
print("flatten", file=f)
print("setundef -undriven -anyseq", file=f)
if "_syn" in model_name:
print(f"# running in {self.workdir}/model/", file=f)
print("read_ilang design.il", file=f)
print("memory_map", file=f)
print(f"# running in {self.workdir}/model/", file=f)
print("read_ilang design.il", file=f)
print("memory_map", file=f)
+ print_common_prep("-simcheck")
print("flatten", file=f)
print("setundef -undriven -anyseq", file=f)
print("setattr -unset keep", file=f)
print("flatten", file=f)
print("setundef -undriven -anyseq", file=f)
print("setattr -unset keep", file=f)
--- /dev/null
+[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
--- /dev/null
+[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