Add smtbmc stbv support

diff --git a/sbysrc/demo3.sby b/sbysrc/demo3.sby
new file mode 100644 (file)
index 0000000..2bb0679
--- /dev/null
+++ b/sbysrc/demo3.sby
@@ -0,0 +1,53 @@
+[options]
+depth 10
+mode bmc
+
+[engines]
+smtbmc yices
+
+[script]
+read_verilog -formal demo.v
+prep -top top
+
+[file demo.v]
+module top (
+  input clk,
+  input [7:0] addr,
+  input [7:0] wdata,
+  output [7:0] rdata,
+);
+  const rand reg [7:0] test_addr;
+  reg [7:0] test_data;
+  reg test_valid = 0;
+
+  always @(posedge clk) begin
+    if (addr == test_addr) begin
+      if (test_valid)
+        assert(test_data == rdata);
+      test_data <= wdata;
+      test_valid <= 1;
+    end
+  end
+
+  memory uut (
+    .clk  (clk  ),
+    .addr (addr ),
+    .wdata(wdata),
+    .rdata(rdata)
+  );
+endmodule
+
+
+module memory (
+  input clk,
+  input [7:0] addr,
+  input [7:0] wdata,
+  output [7:0] rdata,
+);
+  reg [7:0] mem [0:255];
+
+  always @(posedge clk)
+    mem[addr] <= wdata;
+
+  assign rdata = mem[addr];
+endmodule

diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py
index dd1e380b079e8fb14f4e57a5b9e2f1b8bd3388ff..228597e4b81fd114ae038ca12c50d428ee9463d1 100644 (file)
--- a/sbysrc/sby_core.py
+++ b/sbysrc/sby_core.py
@@ -314,20 +314,23 @@ class SbyJob:
 
             return [task]
 
-        if model_name in ["smt2", "smt2_syn", "smt2_nomem", "smt2_syn_nomem"]:
+        if re.match(r"^smt2(_syn)?(_nomem)?(_stbv)?$", model_name):
             with open("%s/model/design_%s.ys" % (self.workdir, model_name), "w") as f:
                 print("# running in %s/model/" % (self.workdir), file=f)
                 print("read_ilang design.il", file=f)
-                if model_name in ["smt2_nomem", "smt2_syn_nomem"]:
+                if "_nomem" in model_name:
                     print("memory_map", file=f)
                     print("opt -keepdc -fast", file=f)
-                if model_name in ["smt2_syn", "smt2_syn_nomem"]:
+                if "_syn" in model_name:
                     print("techmap", file=f)
                     print("opt -fast", file=f)
                     print("abc", file=f)
                     print("opt_clean", file=f)
                 print("stat", file=f)
-                print("write_smt2 -wires design_%s.smt2" % model_name, file=f)
+                if "_stbv" in model_name:
+                    print("write_smt2 -stbv -wires design_%s.smt2" % model_name, file=f)
+                else:
+                    print("write_smt2 -wires design_%s.smt2" % model_name, file=f)
 
             task = SbyTask(self, model_name, self.model("ilang"),
                     "cd %s/model; %s -ql design_%s.log design_%s.ys" % (self.workdir, self.exe_paths["yosys"], model_name, model_name))

diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py
index 52ccb9cfe51fce777a2c5370f41b40910330b7bd..7cb37cd639d85fa9a1ab27039110afc4f7f99208 100644 (file)
--- a/sbysrc/sby_engine_smtbmc.py
+++ b/sbysrc/sby_engine_smtbmc.py
@@ -23,14 +23,17 @@ def run(mode, job, engine_idx, engine):
     smtbmc_opts = []
     nomem_opt = False
     syn_opt = False
+    stbv_opt = False
 
-    opts, args = getopt.getopt(engine[1:], "s:", ["nomem", "syn"])
+    opts, args = getopt.getopt(engine[1:], "s:", ["nomem", "syn", "stbv"])
 
     for o, a in opts:
         if o == "--nomem":
             nomem_opt = True
         elif o == "--syn":
             syn_opt = True
+        elif o == "--stbv":
+            stbv_opt = True
         else:
             assert False
 
@@ -40,6 +43,7 @@ def run(mode, job, engine_idx, engine):
     model_name = "smt2"
     if syn_opt: model_name += "_syn"
     if nomem_opt: model_name += "_nomem"
+    if stbv_opt: model_name += "_stbv"
 
     if mode == "prove":
         run("prove_basecase", job, engine_idx, engine)