Merge pull request #2995 from georgerennie/cover_precond

chformal: Add -coverenable option

1 files changed, 19 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)