riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

chformal: Add -coverprecond option 

This inserts $cover cells to cover the enable signal (precondition)
for the selected formal cells.
This commit is contained in:
George Rennie 2021-09-04 22:40:51 +01:00
parent 90147f5fbf
commit c659bd1878
1 changed files with 14 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
passes/cmds/chformal.cc
View File

@ -55,6 +55,9 @@ struct ChformalPass : public Pass {
log(" -skip <N>\n"); log(" -skip <N>\n");
log(" ignore activation of the constraint in the first <N> clock cycles\n"); log(" ignore activation of the constraint in the first <N> clock cycles\n");
log("\n"); log("\n");
log(" -coverprecond\n");
log(" add a cover statement for the precondition (enable signal) of the cells\n");
log("\n");
log(" -assert2assume\n"); log(" -assert2assume\n");
log(" -assume2assert\n"); log(" -assume2assert\n");
log(" -live2fair\n"); log(" -live2fair\n");
@ -114,6 +117,10 @@ struct ChformalPass : public Pass {
mode_arg = atoi(args[++argidx].c_str()); mode_arg = atoi(args[++argidx].c_str());
continue; continue;
} }
if (mode == 0 && args[argidx] == "-coverprecond") {
mode = 'p';
continue;
}
if ((mode == 0 || mode == 'c') && args[argidx] == "-assert2assume") { if ((mode == 0 || mode == 'c') && args[argidx] == "-assert2assume") {
assert2assume = true; assert2assume = true;
mode = 'c'; mode = 'c';
@ -263,6 +270,13 @@ struct ChformalPass : public Pass {
cell->setPort(ID::EN, module->LogicAnd(NEW_ID, en, cell->getPort(ID::EN))); cell->setPort(ID::EN, module->LogicAnd(NEW_ID, en, cell->getPort(ID::EN)));
} }
else else
if (mode =='p')
{
for (auto cell : constr_cells)
module->addCover(NEW_ID, cell->getPort(ID::EN), State::S1,
"$auto$coverprecond$" + cell->get_src_attribute());
}
else
if (mode == 'c') if (mode == 'c')
{ {
for (auto cell : constr_cells) for (auto cell : constr_cells)