From 5dfad5101d92edb484da2e5306cde58b8d958e7d Mon Sep 17 00:00:00 2001
From: George Rennie <georgerennie@gmail.com>
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>\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("    -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 <<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
diff --git a/tests/various/chformal_coverprecond.ys b/tests/various/chformal_coverprecond.ys
deleted file mode 100644
index 59e302a72..000000000
--- a/tests/various/chformal_coverprecond.ys
+++ /dev/null
@@ -1,25 +0,0 @@
-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 -coverprecond
-select -assert-count 2 t:$cover
-
-chformal -assert -coverprecond
-select -assert-count 4 t:$cover
-
-chformal -assume -coverprecond
-select -assert-count 5 t:$cover
-- 
cgit v1.2.3