From c659bd18786633c52d42b5966627d39d99ae89e3 Mon Sep 17 00:00:00 2001 From: George Rennie Date: Sat, 4 Sep 2021 22:40:51 +0100 Subject: chformal: Add -coverprecond option This inserts $cover cells to cover the enable signal (precondition) for the selected formal cells. --- passes/cmds/chformal.cc | 14 ++++++++++++++ 1 file changed, 14 insertions(+) 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"); log(" ignore activation of the constraint in the first 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) -- cgit v1.2.3 From e39c422734219bb0601827cb7c1d081f7ac7817b Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Tue, 31 May 2022 17:47:07 +0200 Subject: chformal: Test -coverprecond and reuse the src attribute --- passes/cmds/chformal.cc | 4 ++-- tests/various/chformal_coverprecond.ys | 25 +++++++++++++++++++++++++ 2 files changed, 27 insertions(+), 2 deletions(-) create mode 100644 tests/various/chformal_coverprecond.ys diff --git a/passes/cmds/chformal.cc b/passes/cmds/chformal.cc index 0131063b3..c4666f1f0 100644 --- a/passes/cmds/chformal.cc +++ b/passes/cmds/chformal.cc @@ -273,8 +273,8 @@ struct ChformalPass : public Pass { if (mode =='p') { for (auto cell : constr_cells) - module->addCover(NEW_ID, cell->getPort(ID::EN), State::S1, - "$auto$coverprecond$" + cell->get_src_attribute()); + module->addCover(NEW_ID_SUFFIX("coverprecond"), + cell->getPort(ID::EN), State::S1, cell->get_src_attribute()); } else if (mode == 'c') diff --git a/tests/various/chformal_coverprecond.ys b/tests/various/chformal_coverprecond.ys new file mode 100644 index 000000000..59e302a72 --- /dev/null +++ b/tests/various/chformal_coverprecond.ys @@ -0,0 +1,25 @@ +read_verilog -formal < Date: Sat, 18 Jun 2022 18:28:12 +0100 Subject: chformal: Rename -coverprecond to -coverenable --- passes/cmds/chformal.cc | 8 ++++---- tests/various/chformal_coverenable.ys | 25 +++++++++++++++++++++++++ tests/various/chformal_coverprecond.ys | 25 ------------------------- 3 files changed, 29 insertions(+), 29 deletions(-) create mode 100644 tests/various/chformal_coverenable.ys delete mode 100644 tests/various/chformal_coverprecond.ys diff --git a/passes/cmds/chformal.cc b/passes/cmds/chformal.cc index c4666f1f0..c3590855b 100644 --- a/passes/cmds/chformal.cc +++ b/passes/cmds/chformal.cc @@ -55,8 +55,8 @@ struct ChformalPass : public Pass { log(" -skip \n"); log(" ignore activation of the constraint in the first clock cycles\n"); log("\n"); - log(" -coverprecond\n"); - log(" add a cover statement for the precondition (enable signal) of the cells\n"); + log(" -coverenable\n"); + log(" add cover statements for the enable signals of the constraints\n"); log("\n"); log(" -assert2assume\n"); log(" -assume2assert\n"); @@ -117,7 +117,7 @@ struct ChformalPass : public Pass { mode_arg = atoi(args[++argidx].c_str()); continue; } - if (mode == 0 && args[argidx] == "-coverprecond") { + if (mode == 0 && args[argidx] == "-coverenable") { mode = 'p'; continue; } @@ -273,7 +273,7 @@ struct ChformalPass : public Pass { if (mode =='p') { for (auto cell : constr_cells) - module->addCover(NEW_ID_SUFFIX("coverprecond"), + module->addCover(NEW_ID_SUFFIX("coverenable"), cell->getPort(ID::EN), State::S1, cell->get_src_attribute()); } else 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 < Date: Tue, 14 Feb 2023 17:09:53 +0100 Subject: chformal: Note about using -coverenable with the Verific frontend --- passes/cmds/chformal.cc | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/passes/cmds/chformal.cc b/passes/cmds/chformal.cc index c3590855b..94da4cb26 100644 --- a/passes/cmds/chformal.cc +++ b/passes/cmds/chformal.cc @@ -58,6 +58,11 @@ struct ChformalPass : public Pass { 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"); -- cgit v1.2.3