mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-11-04 13:29:12 +00:00
Code Activity

Merge pull request #3186 from nakengelhardt/smtbmc_sby_print_id

Browse source 
add argument for printing cell names in yosys-smtbmc
This commit is contained in:
Miodrag Milanović 2022-03-04 16:39:12 +01:00 • committed by GitHub
commit a95e5d505b
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
2 changed files with 12 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

6
backends/smt2/smt2.cc
View file

@ -985,8 +985,10 @@ struct Smt2Worker
string name_a = get_bool(cell->getPort(ID::A)); string name_a = get_bool(cell->getPort(ID::A));
string name_en = get_bool(cell->getPort(ID::EN)); 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); if (cell->name[0] == '$' && cell->attributes.count(ID::src))
decls.push_back(stringf("; yosys-smt2-%s %d %s\n", cell->type.c_str() + 1, id, infostr.c_str())); 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)) if (cell->type == ID($cover))
decls.push_back(stringf("(define-fun |%s_%c %d| ((state |%s_s|)) Bool (and %s %s)) ; %s\n", decls.push_back(stringf("(define-fun |%s_%c %d| ((state |%s_s|)) Bool (and %s %s)) ; %s\n",

6
backends/smt2/smtio.py
View file

@ -536,9 +536,15 @@ class SmtIo:
self.modinfo[self.curmod].clocks[fields[2]] = "event" self.modinfo[self.curmod].clocks[fields[2]] = "event"
if fields[1] == "yosys-smt2-assert": if fields[1] == "yosys-smt2-assert":
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] self.modinfo[self.curmod].asserts["%s_a %s" % (self.curmod, fields[2])] = fields[3]
if fields[1] == "yosys-smt2-cover": if fields[1] == "yosys-smt2-cover":
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] self.modinfo[self.curmod].covers["%s_c %s" % (self.curmod, fields[2])] = fields[3]
if fields[1] == "yosys-smt2-maximize": if fields[1] == "yosys-smt2-maximize":