diff options
Diffstat (limited to 'backends/smt2')
| -rw-r--r-- | backends/smt2/smt2.cc | 13 | ||||
| -rw-r--r-- | backends/smt2/smtbmc.py | 45 | ||||
| -rw-r--r-- | backends/smt2/smtio.py | 11 |
3 files changed, 59 insertions, 10 deletions
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index 54783cf1b..7434b13da 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -559,6 +559,9 @@ struct Smt2Worker if (cell->type.in(ID($_FF_), ID($_DFF_P_), ID($_DFF_N_))) { registers.insert(cell); + SigBit q_bit = cell->getPort(ID::Q); + if (q_bit.is_wire()) + decls.push_back(witness_signal("reg", 1, 0, "", idcounter, q_bit.wire)); makebits(stringf("%s#%d", get_id(module), idcounter), 0, log_signal(cell->getPort(ID::Q))); register_bool(cell->getPort(ID::Q), idcounter++); recursive_cells.erase(cell); @@ -589,9 +592,12 @@ struct Smt2Worker if (cell->type.in(ID($ff), ID($dff))) { registers.insert(cell); - for (auto chunk : cell->getPort(ID::Q).chunks()) + int smtoffset = 0; + for (auto chunk : cell->getPort(ID::Q).chunks()) { if (chunk.is_wire()) - decls.push_back(witness_signal("reg", chunk.width, chunk.offset, "", idcounter, chunk.wire)); + decls.push_back(witness_signal("reg", chunk.width, chunk.offset, "", idcounter, chunk.wire, smtoffset)); + smtoffset += chunk.width; + } makebits(stringf("%s#%d", get_id(module), idcounter), GetSize(cell->getPort(ID::Q)), log_signal(cell->getPort(ID::Q))); register_bv(cell->getPort(ID::Q), idcounter++); recursive_cells.erase(cell); @@ -1490,7 +1496,7 @@ struct Smt2Worker return path; } - std::string witness_signal(const char *type, int width, int offset, const std::string &smtname, int smtid, RTLIL::Wire *wire) + std::string witness_signal(const char *type, int width, int offset, const std::string &smtname, int smtid, RTLIL::Wire *wire, int smtoffset = 0) { std::vector<std::string> hiername; const char *wire_name = wire->name.c_str(); @@ -1508,6 +1514,7 @@ struct Smt2Worker { "offset", offset }, { "width", width }, { "smtname", smtname.empty() ? json11::Json(smtid) : json11::Json(smtname) }, + { "smtoffset", smtoffset }, { "path", witness_path(wire) }, }}).dump(line); line += "\n"; diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index 5f05287de..cb21eb3aa 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -55,6 +55,7 @@ noinit = False binarymode = False keep_going = False check_witness = False +detect_loops = False so = SmtOpts() @@ -175,6 +176,10 @@ def usage(): check that the used witness file contains sufficient constraints to force an assertion failure. + --detect-loops + check if states are unique in temporal induction counter examples + (this feature is experimental and incomplete) + """ + so.helpmsg()) sys.exit(1) @@ -183,7 +188,7 @@ try: opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:igcm:", so.longopts + ["final-only", "assume-skipped=", "smtc=", "cex=", "aig=", "aig-noheader", "yw=", "btorwit=", "presat", "dump-vcd=", "dump-yw=", "dump-vlogtb=", "vlogtb-top=", "dump-smtc=", "dump-all", "noinfo", "append=", - "smtc-init", "smtc-top=", "noinit", "binary", "keep-going", "check-witness"]) + "smtc-init", "smtc-top=", "noinit", "binary", "keep-going", "check-witness", "detect-loops"]) except: usage() @@ -264,6 +269,8 @@ for o, a in opts: keep_going = True elif o == "--check-witness": check_witness = True + elif o == "--detect-loops": + detect_loops = True elif so.handle(o, a): pass else: @@ -446,7 +453,6 @@ assert topmod in smt.modinfo if cexfile is not None: if not got_topt: - assume_skipped = 0 skip_steps = 0 num_steps = 0 @@ -492,7 +498,6 @@ if aimfile is not None: latch_map = dict() if not got_topt: - assume_skipped = 0 skip_steps = 0 num_steps = 0 @@ -626,7 +631,6 @@ if aimfile is not None: if inywfile is not None: if not got_topt: - assume_skipped = 0 skip_steps = 0 num_steps = 0 @@ -669,7 +673,7 @@ if inywfile is not None: if common_end <= common_offset: continue - smt_expr = smt.net_expr(topmod, f"s{t}", wire["smtpath"]) + smt_expr = smt.witness_net_expr(topmod, f"s{t}", wire) if not smt_bool: slice_high = common_end - offset - 1 @@ -969,6 +973,30 @@ def write_vcd_trace(steps_start, steps_stop, index): vcd.set_time(steps_stop) +def detect_state_loop(steps_start, steps_stop): + print_msg(f"Checking for loops in found induction counter example") + print_msg(f"This feature is experimental and incomplete") + + path_list = sorted(smt.hiernets(topmod, regs_only=True)) + + mem_trace_data = collect_mem_trace_data(steps_start, steps_stop) + + # Map state to index of step when it occurred + states = dict() + + for i in range(steps_start, steps_stop): + value_list = smt.get_net_bin_list(topmod, path_list, "s%d" % i) + mem_state = sorted( + [(tuple(path), addr, data) + for path, addr, data in mem_trace_data.get(i, [])]) + state = tuple(value_list), tuple(mem_state) + if state in states: + return (i, states[state]) + else: + states[state] = i + + return None + def char_ok_in_verilog(c,i): if ('A' <= c <= 'Z'): return True if ('a' <= c <= 'z'): return True @@ -1267,7 +1295,8 @@ def write_yw_trace(steps_start, steps_stop, index, allregs=False): sigs = seqs for sig in sigs: - step_values[sig["sig"]] = smt.bv2bin(smt.get(smt.net_expr(topmod, f"s{k}", sig["smtpath"]))) + value = smt.bv2bin(smt.get(smt.witness_net_expr(topmod, f"s{k}", sig))) + step_values[sig["sig"]] = value yw.step(step_values) yw.end_trace() @@ -1596,6 +1625,10 @@ if tempind: print_anyconsts(num_steps) print_failed_asserts(num_steps) write_trace(step, num_steps+1, '%', allregs=True) + if detect_loops: + loop = detect_state_loop(step, num_steps+1) + if loop: + print_msg(f"Loop detected, increasing induction depth will not help. Step {loop[0]} = step {loop[1]}") elif dumpall: print_anyconsts(num_steps) diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index 9af454cca..a73745896 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -701,7 +701,7 @@ class SmtIo: if witness["type"] == "mem": if allregs and not witness["rom"]: width, size = witness["width"], witness["size"] - witness = {**witness, "uninitialized": {"width": width * size, "offset": 0}} + witness = {**witness, "uninitialized": [{"width": width * size, "offset": 0}]} if not witness["uninitialized"]: continue @@ -958,6 +958,15 @@ class SmtIo: nextbase = "(|%s_h %s| %s)" % (mod, path[0], base) return self.net_expr(nextmod, nextbase, path[1:]) + def witness_net_expr(self, mod, base, witness): + net = self.net_expr(mod, base, witness["smtpath"]) + is_bool = self.net_width(mod, witness["smtpath"]) == 1 + if is_bool: + assert witness["width"] == 1 + assert witness["smtoffset"] == 0 + return net + return "((_ extract %d %d) %s)" % (witness["smtoffset"] + witness["width"] - 1, witness["smtoffset"], net) + def net_width(self, mod, net_path): for i in range(len(net_path)-1): assert mod in self.modinfo |