mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-04-23 09:05:32 +00:00
Code Activity

rename -witness: Bug fix and rename formal cells

Browse source 
Rename formal cells in addition to witness signals. This is required to
reliably track individual property states for the non-smtbmc flows.

Also removes a misplced `break` which resulted in only partial witness
renaming.
This commit is contained in:
Jannis Harder 2024-02-27 19:56:47 +01:00
parent 6469d90293
commit d8cdc213a6
2 changed files with 26 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

15
passes/cmds/rename.cc
View file

@ -134,7 +134,6 @@ static bool rename_witness(RTLIL::Design *design, dict<RTLIL::Module *, int> &ca
cell->set_hdlname_attribute({ "_witness_", strstr(new_id.c_str(), ".") + 1 });
renames.emplace_back(cell, new_id);
}
break;
}
if (cell->type.in(ID($anyconst), ID($anyseq), ID($anyinit), ID($allconst), ID($allseq))) {
@ -165,6 +164,20 @@ static bool rename_witness(RTLIL::Design *design, dict<RTLIL::Module *, int> &ca
}
}
}
if (cell->type.in(ID($assert), ID($assume), ID($cover), ID($live), ID($fair), ID($check))) {
has_witness_signals = true;
if (cell->name.isPublic())
continue;
std::string name = stringf("%s_%s", cell->type.c_str() + 1, cell->name.c_str() + 1);
for (auto &c : name)
if ((c < 'a' || c > 'z') && (c < 'A' || c > 'Z') && (c < '0' || c > '9') && c != '_')
c = '_';
auto new_id = module->uniquify("\\_witness_." + name);
renames.emplace_back(cell, new_id);
cell->set_hdlname_attribute({ "_witness_", strstr(new_id.c_str(), ".") + 1 });
}
}
for (auto rename : renames) {
module->rename(rename.first, rename.second);