diff options
Diffstat (limited to 'backends')
| -rw-r--r-- | backends/smt2/smt2.cc | 4 | ||||
| -rw-r--r-- | backends/smt2/smtbmc.py | 20 | ||||
| -rw-r--r-- | backends/smt2/smtio.py | 4 |
3 files changed, 27 insertions, 1 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()): |