diff options
| author | Jannis Harder <me@jix.one> | 2023-02-14 17:46:31 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2023-02-14 17:46:31 +0100 |
| commit | ec947036191bce7ef020c240fbdb8d6fdcf572b6 (patch) | |
| tree | 5cffe4f8a53459a0f617a33ba4839c67860c585b | |
| parent | 85f611fb23ea6f10505299a2f2329e2efedd1dbc (diff) | |
| parent | b636af9751993bd35f02f56e68e63a4ef715aa4e (diff) | |
| download | yosys-ec947036191bce7ef020c240fbdb8d6fdcf572b6.tar.gz yosys-ec947036191bce7ef020c240fbdb8d6fdcf572b6.tar.bz2 yosys-ec947036191bce7ef020c240fbdb8d6fdcf572b6.zip | |
Merge pull request #2995 from georgerennie/cover_precond
chformal: Add -coverenable option
| -rw-r--r-- | passes/cmds/chformal.cc | 19 | ||||
| -rw-r--r-- | tests/various/chformal_coverenable.ys | 25 |
2 files changed, 44 insertions, 0 deletions
diff --git a/passes/cmds/chformal.cc b/passes/cmds/chformal.cc index 66044b161..da97ff71d 100644 --- a/passes/cmds/chformal.cc +++ b/passes/cmds/chformal.cc @@ -55,6 +55,14 @@ struct ChformalPass : public Pass { log(" -skip <N>\n"); log(" ignore activation of the constraint in the first <N> clock cycles\n"); log("\n"); + log(" -coverenable\n"); + log(" add cover statements for the enable signals of the constraints\n"); + log("\n"); +#ifdef YOSYS_ENABLE_VERIFIC + log(" Note: For the Verific frontend it is currently not guaranteed that a\n"); + log(" reachable SVA statement corresponds to an active enable signal.\n"); + log("\n"); +#endif log(" -assert2assume\n"); log(" -assume2assert\n"); log(" -live2fair\n"); @@ -114,6 +122,10 @@ struct ChformalPass : public Pass { mode_arg = atoi(args[++argidx].c_str()); continue; } + if (mode == 0 && args[argidx] == "-coverenable") { + mode = 'p'; + continue; + } if ((mode == 0 || mode == 'c') && args[argidx] == "-assert2assume") { assert2assume = true; mode = 'c'; @@ -263,6 +275,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_SUFFIX("coverenable"), + cell->getPort(ID::EN), State::S1, cell->get_src_attribute()); + } + else if (mode == 'c') { for (auto cell : constr_cells) diff --git a/tests/various/chformal_coverenable.ys b/tests/various/chformal_coverenable.ys new file mode 100644 index 000000000..52b3ee6bf --- /dev/null +++ b/tests/various/chformal_coverenable.ys @@ -0,0 +1,25 @@ +read_verilog -formal <<EOT +module top(input a, b, c, d); + + always @* begin + if (a) assert (b == c); + if (!a) assert (b != c); + if (b) assume (c); + if (c) cover (d); + end + +endmodule +EOT + +prep -top top + +select -assert-count 1 t:$cover + +chformal -cover -coverenable +select -assert-count 2 t:$cover + +chformal -assert -coverenable +select -assert-count 4 t:$cover + +chformal -assume -coverenable +select -assert-count 5 t:$cover |