Added $anyconst support to yosys-smtbmc

diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index 9668a64256d3e3df13d04df37ab1bcd3c49f44c7..30a6bb19cef0b7b1bc8f2888a46050d1f46e242a 100644 (file)
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -420,6 +420,8 @@ struct Smt2Worker
                        if (cell->type == "$anyconst")
                        {
                                registers.insert(cell);
+                               decls.push_back(stringf("; yosys-smt2-%s %s#%d %s\n", cell->type.c_str() + 1, get_id(module), idcounter,
+                                               cell->attributes.count("\\src") ? cell->attributes.at("\\src").decode_string().c_str() : get_id(cell)));
                                decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) (_ BitVec %d)) ; %s\n",
                                                get_id(module), idcounter, get_id(module), GetSize(cell->getPort("\\Y")), log_signal(cell->getPort("\\Y"))));
                                register_bv(cell->getPort("\\Y"), idcounter++);
@@ -669,7 +671,7 @@ struct Smt2Worker
                                string name_a = get_bool(cell->getPort("\\A"));
                                string name_en = get_bool(cell->getPort("\\EN"));
                                decls.push_back(stringf("; yosys-smt2-%s %s#%d %s\n", cell->type.c_str() + 1, get_id(module), idcounter,
-                                       cell->attributes.count("\\src") ? cell->attributes.at("\\src").decode_string().c_str() : get_id(cell)));
+                                               cell->attributes.count("\\src") ? cell->attributes.at("\\src").decode_string().c_str() : get_id(cell)));
                                decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) Bool (or %s (not %s))) ; %s\n",
                                                get_id(module), idcounter, get_id(module), name_a.c_str(), name_en.c_str(), get_id(cell)));
                                if (cell->type == "$assert")

diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index 9096654f06bb9db877420a468988b2ff244e9018..fa887dd1540b09f2d9260359ed458e9dc8b57a54 100644 (file)
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -504,6 +504,20 @@ def print_failed_asserts(state, final=False):
         print_failed_asserts_worker(topmod, "s%d" % state, topmod)
 
 
+def print_anyconsts_worker(mod, state, path):
+    assert mod in smt.modinfo
+
+    for cellname, celltype in smt.modinfo[mod].cells.items():
+        print_anyconsts_worker(celltype, "(|%s_h %s| %s)" % (mod, cellname, state), path + "." + cellname)
+
+    for fun, info in smt.modinfo[mod].anyconsts.items():
+        print("%s Value for anyconst in %s (%s): %d" % (smt.timestamp(), path, info, smt.bv2int(smt.get("(|%s| %s)" % (fun, state)))))
+
+
+def print_anyconsts(state):
+    print_anyconsts_worker(topmod, "s%d" % state, topmod)
+
+
 if tempind:
     retstatus = False
     skip_counter = step_size
@@ -535,10 +549,12 @@ if tempind:
         if smt.check_sat() == "sat":
             if step == 0:
                 print("%s Temporal induction failed!" % smt.timestamp())
+                print_anyconsts(num_steps)
                 print_failed_asserts(num_steps)
                 write_trace(step, num_steps+1, '%')
 
             elif dumpall:
+                print_anyconsts(num_steps)
                 print_failed_asserts(num_steps)
                 write_trace(step, num_steps+1, "%d" % step)
 
@@ -598,6 +614,7 @@ else: # not tempind
 
                 if smt.check_sat() == "sat":
                     print("%s BMC failed!" % smt.timestamp())
+                    print_anyconsts(step)
                     for i in range(step, last_check_step+1):
                         print_failed_asserts(i)
                     write_trace(0, last_check_step+1, '%')
@@ -623,6 +640,7 @@ else: # not tempind
 
                     if smt.check_sat() == "sat":
                         print("%s BMC failed!" % smt.timestamp())
+                        print_anyconsts(i)
                         print_failed_asserts(i, final=True)
                         write_trace(0, i+1, '%')
                         retstatus = False
@@ -644,11 +662,13 @@ else: # not tempind
                 break
 
             elif dumpall:
+                print_anyconsts(0)
                 write_trace(0, last_check_step+1, "%d" % step)
 
         step += step_size
 
     if gentrace:
+        print_anyconsts(0)
         write_trace(0, num_steps, '%')
 
 

diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index da9d4830f9051557bd65af8e3dea0eae344fa771..fc7d1e13d19b1a5b95fe4f0a0dff9fcbbd6bdcfa 100644 (file)
--- a/backends/smt2/smtio.py
+++ b/backends/smt2/smtio.py
@@ -32,6 +32,7 @@ class smtmodinfo:
         self.wsize = dict()
         self.cells = dict()
         self.asserts = dict()
+        self.anyconsts = dict()
 
 class smtio:
     def __init__(self, solver=None, debug_print=None, debug_file=None, timeinfo=None, opts=None):
@@ -137,6 +138,9 @@ class smtio:
         if fields[1] == "yosys-smt2-assert":
             self.modinfo[self.curmod].asserts[fields[2]] = fields[3]
 
+        if fields[1] == "yosys-smt2-anyconst":
+            self.modinfo[self.curmod].anyconsts[fields[2]] = fields[3]
+
     def hiernets(self, top, regs_only=False):
         def hiernets_worker(nets, mod, cursor):
             for netname in sorted(self.modinfo[mod].wsize.keys()):

diff --git a/examples/smtbmc/.gitignore b/examples/smtbmc/.gitignore
index fbddafa8a7bdb2927ab2f7f714fc422be5202684..88d264c63f3d10b700b8da9301153953a0f90156 100644 (file)
--- a/examples/smtbmc/.gitignore
+++ b/examples/smtbmc/.gitignore
@@ -13,3 +13,6 @@ demo3.yslog
 demo4.smt2
 demo4.vcd
 demo4.yslog
+demo5.smt2
+demo5.vcd
+demo5.yslog

diff --git a/examples/smtbmc/Makefile b/examples/smtbmc/Makefile
index 6078fc64fb22220ea7c19480c8f425427f1444ab..a2d4f444b3d0d85b3ae14b2cc63dd3bbb196feaf 100644 (file)
--- a/examples/smtbmc/Makefile
+++ b/examples/smtbmc/Makefile
@@ -16,6 +16,9 @@ demo3: demo3.smt2
 demo4: demo4.smt2
        yosys-smtbmc -s yices --dump-vcd demo4.vcd --smtc demo4.smtc demo4.smt2
 
+demo5: demo5.smt2
+       yosys-smtbmc -g -t 50 --dump-vcd demo5.vcd demo5.smt2
+
 demo1.smt2: demo1.v
        yosys -ql demo1.yslog -p 'read_verilog -formal demo1.v; prep -top demo1 -nordff; write_smt2 -wires demo1.smt2'
 
@@ -28,11 +31,15 @@ demo3.smt2: demo3.v
 demo4.smt2: demo4.v
        yosys -ql demo4.yslog -p 'read_verilog -formal demo4.v; prep -top demo4 -nordff; write_smt2 -wires demo4.smt2'
 
+demo5.smt2: demo5.v
+       yosys -ql demo5.yslog -p 'read_verilog -formal demo5.v; prep -top demo5 -nordff; write_smt2 -wires demo5.smt2'
+
 clean:
        rm -f demo1.yslog demo1.smt2 demo1.vcd
        rm -f demo2.yslog demo2.smt2 demo2.vcd demo2.smtc demo2_tb.v demo2_tb demo2_tb.vcd
        rm -f demo3.yslog demo3.smt2 demo3.vcd
        rm -f demo4.yslog demo4.smt2 demo4.vcd
+       rm -f demo5.yslog demo5.smt2 demo5.vcd
 
-.PHONY: demo1 demo2 demo3 demo4 clean
+.PHONY: demo1 demo2 demo3 demo4 demo5 clean
 

diff --git a/examples/smtbmc/demo5.v b/examples/smtbmc/demo5.v
new file mode 100644 (file)
index 0000000..63ace30
--- /dev/null
+++ b/examples/smtbmc/demo5.v
@@ -0,0 +1,18 @@
+// Demo for $anyconst
+
+module demo5 (input clk);
+       wire [7:0] step_size = $anyconst;
+       reg [7:0] state = 0, count = 0;
+       reg [31:0] hash = 0;
+
+       always @(posedge clk) begin
+               count <= count + 1;
+               hash <= ((hash << 5) + hash) ^ state;
+               state <= state + step_size;
+       end
+
+       always @* begin
+               if (count == 42)
+                       assert(hash == 32'h A18FAC0A);
+       end
+endmodule

diff --git a/frontends/ast/genrtlil.cc b/frontends/ast/genrtlil.cc
index 569d2b6ab013ea03c18ff4c5d297f103e95dae50..03596411fb017390ee55093184c4e16a1245226b 100644 (file)
--- a/frontends/ast/genrtlil.cc
+++ b/frontends/ast/genrtlil.cc
@@ -1468,9 +1468,11 @@ RTLIL::SigSpec AstNode::genRTLIL(int width_hint, bool sign_hint)
                                                        RTLIL::unescape_id(str).c_str(), filename.c_str(), linenum);
 
                                Cell *cell = current_module->addCell(myid, str.substr(1));
+                               cell->attributes["\\src"] = stringf("%s:%d", filename.c_str(), linenum);
                                cell->parameters["\\WIDTH"] = width;
 
                                Wire *wire = current_module->addWire(myid + "_wire", width);
+                               wire->attributes["\\src"] = stringf("%s:%d", filename.c_str(), linenum);
                                cell->setPort("\\Y", wire);
 
                                is_signed = sign_hint;