Added $anyconst support to yosys-smtbmc

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++);

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, '%')
 
 

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()):

examples/smtbmc/.gitignore

@@ -13,3 +13,6 @@ demo3.yslog
 demo4.smt2
 demo4.vcd
 demo4.yslog
+demo5.smt2
+demo5.vcd
+demo5.yslog

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
 

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

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;