aboutsummaryrefslogtreecommitdiffstats
path: root/backends
diff options
context:
space:
mode:
authorMiodrag Milanović <mmicko@gmail.com>2022-03-04 16:39:12 +0100
committerGitHub <noreply@github.com>2022-03-04 16:39:12 +0100
commita95e5d505b8e5dd841ba6eb8b6d1e9cfe75aa776 (patch)
treef3640bdd4d521efefa4f54e008bde2ac34d3ac0a /backends
parent13655ddccf861de13f7b7faced793fdd2799dce4 (diff)
parentdc739362c7e0c0d7befe2a5dc2866aef31ca5a20 (diff)
downloadyosys-a95e5d505b8e5dd841ba6eb8b6d1e9cfe75aa776.tar.gz
yosys-a95e5d505b8e5dd841ba6eb8b6d1e9cfe75aa776.tar.bz2
yosys-a95e5d505b8e5dd841ba6eb8b6d1e9cfe75aa776.zip
Merge pull request #3186 from nakengelhardt/smtbmc_sby_print_id
add argument for printing cell names in yosys-smtbmc
Diffstat (limited to 'backends')
-rw-r--r--backends/smt2/smt2.cc6
-rw-r--r--backends/smt2/smtio.py10
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])