From aa25a4cec66bfde84f9142b21679e82ba90ee910 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Tue, 30 Aug 2016 19:27:42 +0200 Subject: [PATCH] Added $anyconst support to yosys-smtbmc --- backends/smt2/smt2.cc | 4 +++- backends/smt2/smtbmc.py | 20 ++++++++++++++++++++ backends/smt2/smtio.py | 4 ++++ examples/smtbmc/.gitignore | 3 +++ examples/smtbmc/Makefile | 9 ++++++++- examples/smtbmc/demo5.v | 18 ++++++++++++++++++ frontends/ast/genrtlil.cc | 2 ++ 7 files changed, 58 insertions(+), 2 deletions(-) create mode 100644 examples/smtbmc/demo5.v 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; -- 2.30.2