aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--backends/smt2/smt2.cc4
-rw-r--r--backends/smt2/smtbmc.py20
-rw-r--r--backends/smt2/smtio.py4
-rw-r--r--examples/smtbmc/.gitignore3
-rw-r--r--examples/smtbmc/Makefile9
-rw-r--r--examples/smtbmc/demo5.v18
-rw-r--r--frontends/ast/genrtlil.cc2
7 files changed, 58 insertions, 2 deletions
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index 9668a6425..30a6bb19c 100644
--- 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 9096654f0..fa887dd15 100644
--- 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 da9d4830f..fc7d1e13d 100644
--- 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 fbddafa8a..88d264c63 100644
--- 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 6078fc64f..a2d4f444b 100644
--- 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
index 000000000..63ace307c
--- /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 569d2b6ab..03596411f 100644
--- 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;
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-11 19:16:14 +0000