diff options
Diffstat (limited to 'passes/cmds/chformal.cc')
| -rw-r--r-- | passes/cmds/chformal.cc | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/passes/cmds/chformal.cc b/passes/cmds/chformal.cc index d813a449c..0131063b3 100644 --- a/passes/cmds/chformal.cc +++ b/passes/cmds/chformal.cc @@ -55,6 +55,9 @@ struct ChformalPass : public Pass { log(" -skip <N>\n"); log(" ignore activation of the constraint in the first <N> clock cycles\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(" -assume2assert\n"); log(" -live2fair\n"); @@ -114,6 +117,10 @@ struct ChformalPass : public Pass { mode_arg = atoi(args[++argidx].c_str()); continue; } + if (mode == 0 && args[argidx] == "-coverprecond") { + mode = 'p'; + continue; + } if ((mode == 0 || mode == 'c') && args[argidx] == "-assert2assume") { assert2assume = true; mode = 'c'; @@ -263,6 +270,13 @@ struct ChformalPass : public Pass { cell->setPort(ID::EN, module->LogicAnd(NEW_ID, en, cell->getPort(ID::EN))); } 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') { for (auto cell : constr_cells) |