diff options
| author | N. Engelhardt <nak@yosyshq.com> | 2022-02-04 18:23:12 +0100 |
|---|---|---|
| committer | N. Engelhardt <nak@yosyshq.com> | 2022-02-22 17:00:10 +0100 |
| commit | dc739362c7e0c0d7befe2a5dc2866aef31ca5a20 (patch) | |
| tree | b3c60a9f8c52f22e7c11f9916473a1c2e2ea0c3d | |
| parent | bf85dfee5e0cceaed8f6f6782afe2d1803039e6a (diff) | |
| download | yosys-dc739362c7e0c0d7befe2a5dc2866aef31ca5a20.tar.gz yosys-dc739362c7e0c0d7befe2a5dc2866aef31ca5a20.tar.bz2 yosys-dc739362c7e0c0d7befe2a5dc2866aef31ca5a20.zip | |
print cell name for properties in yosys-smtbmc
| -rw-r--r-- | backends/smt2/smt2.cc | 6 | ||||
| -rw-r--r-- | backends/smt2/smtio.py | 10 |
2 files changed, 12 insertions, 4 deletions
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index a928419a1..9bf0de03e 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -985,8 +985,10 @@ struct Smt2Worker string name_a = get_bool(cell->getPort(ID::A)); string name_en = get_bool(cell->getPort(ID::EN)); - string infostr = (cell->name[0] == '$' && cell->attributes.count(ID::src)) ? cell->attributes.at(ID::src).decode_string() : get_id(cell); - decls.push_back(stringf("; yosys-smt2-%s %d %s\n", cell->type.c_str() + 1, id, infostr.c_str())); + if (cell->name[0] == '$' && cell->attributes.count(ID::src)) + decls.push_back(stringf("; yosys-smt2-%s %d %s %s\n", cell->type.c_str() + 1, id, get_id(cell), cell->attributes.at(ID::src).decode_string().c_str())); + else + decls.push_back(stringf("; yosys-smt2-%s %d %s\n", cell->type.c_str() + 1, id, get_id(cell))); if (cell->type == ID($cover)) decls.push_back(stringf("(define-fun |%s_%c %d| ((state |%s_s|)) Bool (and %s %s)) ; %s\n", diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index d73a875ba..3d458e6cf 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -536,10 +536,16 @@ class SmtIo: self.modinfo[self.curmod].clocks[fields[2]] = "event" if fields[1] == "yosys-smt2-assert": - self.modinfo[self.curmod].asserts["%s_a %s" % (self.curmod, fields[2])] = fields[3] + if len(fields) > 4: + self.modinfo[self.curmod].asserts["%s_a %s" % (self.curmod, fields[2])] = f'{fields[4]} ({fields[3]})' + else: + self.modinfo[self.curmod].asserts["%s_a %s" % (self.curmod, fields[2])] = fields[3] if fields[1] == "yosys-smt2-cover": - self.modinfo[self.curmod].covers["%s_c %s" % (self.curmod, fields[2])] = fields[3] + if len(fields) > 4: + self.modinfo[self.curmod].covers["%s_c %s" % (self.curmod, fields[2])] = f'{fields[4]} ({fields[3]})' + else: + self.modinfo[self.curmod].covers["%s_c %s" % (self.curmod, fields[2])] = fields[3] if fields[1] == "yosys-smt2-maximize": self.modinfo[self.curmod].maximize.add(fields[2]) |