aboutsummaryrefslogtreecommitdiffstats
path: root/backends/smt2/smtio.py
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2016-08-17 20:10:02 +0200
committerClifford Wolf <clifford@clifford.at>2016-08-17 20:10:02 +0200
commitdfcd30ea869f43af520aef033aa1311457112904 (patch)
tree6d066b6dc33fbc15499333c281becea6bc6d9cea /backends/smt2/smtio.py
parent42a971226bd1972c3c21d386c02c1bc2ac850129 (diff)
downloadyosys-dfcd30ea869f43af520aef033aa1311457112904.tar.gz
yosys-dfcd30ea869f43af520aef033aa1311457112904.tar.bz2
yosys-dfcd30ea869f43af520aef033aa1311457112904.zip
Added printing of code loc of failed asserts to yosys-smtbmc
Diffstat (limited to 'backends/smt2/smtio.py')
-rw-r--r--backends/smt2/smtio.py4
1 files changed, 4 insertions, 0 deletions
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index 5f93a2fed..53d2ec57b 100644
--- a/backends/smt2/smtio.py
+++ b/backends/smt2/smtio.py
@@ -30,6 +30,7 @@ class smtmodinfo:
self.wires = set()
self.wsize = dict()
self.cells = dict()
+ self.asserts = dict()
class smtio:
def __init__(self, solver=None, debug_print=None, debug_file=None, timeinfo=None, opts=None):
@@ -129,6 +130,9 @@ class smtio:
self.modinfo[self.curmod].wires.add(fields[2])
self.modinfo[self.curmod].wsize[fields[2]] = int(fields[3])
+ if fields[1] == "yosys-smt2-assert":
+ self.modinfo[self.curmod].asserts[fields[2]] = fields[3]
+
def hiernets(self, top):
def hiernets_worker(nets, mod, cursor):
for netname in sorted(self.modinfo[mod].wsize.keys()):