Use SVA label in smt export if available

Signed-off-by: Clifford Wolf <clifford@clifford.at>
This commit is contained in:
Clifford Wolf 2019-03-07 11:31:46 -08:00
parent 22ff60850e
commit 5dfc7becca
1 changed files with 2 additions and 2 deletions

View File

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