From: N. Engelhardt <nak@yosyshq.com>
Date: Fri, 4 Feb 2022 17:23:12 +0000 (+0100)
Subject: print cell name for properties in yosys-smtbmc
X-Git-Tag: yosys-0.16~57^2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=dc739362c7e0c0d7befe2a5dc2866aef31ca5a20;p=yosys.git

print cell name for properties in yosys-smtbmc
---

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])