diff options
Diffstat (limited to 'backends')
| -rw-r--r-- | backends/btor/btor.cc | 4 | ||||
| -rw-r--r-- | backends/json/json.cc | 19 | ||||
| -rw-r--r-- | backends/smt2/smt2.cc | 6 | ||||
| -rw-r--r-- | backends/smt2/smtio.py | 10 |
4 files changed, 32 insertions, 7 deletions
diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc index d62cc4c3d..73e88c049 100644 --- a/backends/btor/btor.cc +++ b/backends/btor/btor.cc @@ -678,7 +678,7 @@ struct BtorWorker int sid = get_bv_sid(GetSize(sig_y)); int nid = next_nid++; - btorf("%d state %d\n", nid, sid); + btorf("%d state %d%s\n", nid, sid, getinfo(cell).c_str()); if (cell->type == ID($anyconst)) { int nid2 = next_nid++; @@ -699,7 +699,7 @@ struct BtorWorker int one_nid = get_sig_nid(State::S1); int zero_nid = get_sig_nid(State::S0); initstate_nid = next_nid++; - btorf("%d state %d\n", initstate_nid, sid); + btorf("%d state %d%s\n", initstate_nid, sid, getinfo(cell).c_str()); btorf("%d init %d %d %d\n", next_nid++, sid, initstate_nid, one_nid); btorf("%d next %d %d %d\n", next_nid++, sid, initstate_nid, zero_nid); } diff --git a/backends/json/json.cc b/backends/json/json.cc index 4aa8046d6..270d762ee 100644 --- a/backends/json/json.cc +++ b/backends/json/json.cc @@ -52,8 +52,23 @@ struct JsonWriter string newstr = "\""; for (char c : str) { if (c == '\\') + newstr += "\\\\"; + else if (c == '"') + newstr += "\\\""; + else if (c == '\b') + newstr += "\\b"; + else if (c == '\f') + newstr += "\\f"; + else if (c == '\n') + newstr += "\\n"; + else if (c == '\r') + newstr += "\\r"; + else if (c == '\t') + newstr += "\\t"; + else if (c < 0x20) + newstr += stringf("\\u%04X", c); + else newstr += c; - newstr += c; } return newstr + "\""; } @@ -379,6 +394,7 @@ struct JsonBackend : public Backend { log(" \"bits\": <bit_vector>\n"); log(" \"offset\": <the lowest bit index in use, if non-0>\n"); log(" \"upto\": <1 if the port bit indexing is MSB-first>\n"); + log(" \"signed\": <1 if the port is signed>\n"); log(" }\n"); log("\n"); log("The \"offset\" and \"upto\" fields are skipped if their value would be 0."); @@ -428,6 +444,7 @@ struct JsonBackend : public Backend { log(" \"bits\": <bit_vector>\n"); log(" \"offset\": <the lowest bit index in use, if non-0>\n"); log(" \"upto\": <1 if the port bit indexing is MSB-first>\n"); + log(" \"signed\": <1 if the port is signed>\n"); log(" }\n"); log("\n"); log("The \"hide_name\" fields are set to 1 when the name of this cell or net is\n"); 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]) |