Merge pull request #5179 from YosysHQ/krys/assert2cover

Author: nakengelhardt

passes/cmds/chformal.cc

@@ -115,6 +115,7 @@ struct ChformalPass : public Pass {
 		log("\n");
 #endif
 		log("    -assert2assume\n");
+		log("    -assert2cover\n");
 		log("    -assume2assert\n");
 		log("    -live2fair\n");
 		log("    -fair2live\n");
@@ -129,6 +130,7 @@ struct ChformalPass : public Pass {
 	void execute(std::vector<std::string> args, RTLIL::Design *design) override
 	{
 		bool assert2assume = false;
+		bool assert2cover = false;
 		bool assume2assert = false;
 		bool live2fair = false;
 		bool fair2live = false;
@@ -187,6 +189,11 @@ struct ChformalPass : public Pass {
 				mode = 'c';
 				continue;
 			}
+			if ((mode == 0 || mode == 'c') && args[argidx] == "-assert2cover") {
+				assert2cover = true;
+				mode = 'c';
+				continue;
+			}
 			if ((mode == 0 || mode == 'c') && args[argidx] == "-assume2assert") {
 				assume2assert = true;
 				mode = 'c';
@@ -218,6 +225,10 @@ struct ChformalPass : public Pass {
 			constr_types.insert(ID($cover));
 		}
 
+		if (assert2assume && assert2cover) {
+			log_cmd_error("Cannot use both -assert2assume and -assert2cover.\n");
+		}
+
 		if (mode == 0)
 			log_cmd_error("Mode option is missing.\n");
 
@@ -381,6 +392,8 @@ struct ChformalPass : public Pass {
 					IdString flavor = formal_flavor(cell);
 					if (assert2assume && flavor == ID($assert))
 						set_formal_flavor(cell, ID($assume));
+					if (assert2cover && flavor == ID($assert))
+						set_formal_flavor(cell, ID($cover));
 					else if (assume2assert && flavor == ID($assume))
 						set_formal_flavor(cell, ID($assert));
 					else if (live2fair && flavor == ID($live))

tests/various/chformal_check.ys

@@ -36,6 +36,12 @@ select -assert-count 1 t:$assert
 
 design -load prep
 
+chformal -assert2cover
+
+select -assert-count 1 t:$check r:FLAVOR=cover %i
+
+design -load prep
+
 chformal -assert2assume
 async2sync
 chformal -lower
@@ -66,3 +72,8 @@ design -copy-from gate -as gate top
 miter -equiv -flatten -make_assert gold gate miter
 
 sat -verify -prove-asserts -tempinduct miter
+
+design -load prep
+
+logger -expect error "Cannot use both" 1
+chformal -assert2assume -assert2cover

tests/verific/chformal.ys

@@ -0,0 +1,74 @@
+verific -formal <<EOT
+
+module top(input clk, a, en);
+    reg a_q = '0;
+    reg en_q = '0;
+
+    always @(posedge clk) begin
+        a_q <= a;
+        en_q <= en;
+    end
+
+    always @(posedge clk)
+        if (en_q)
+            assert(a_q);
+endmodule
+EOT
+
+prep
+
+design -save prep
+
+select -assert-count 1 t:$assert
+
+chformal -assert2assume
+
+select -assert-count 1 t:$assume
+
+chformal -assume2assert
+
+select -assert-count 1 t:$assert
+
+async2sync
+
+chformal -lower
+select -assert-count 1 t:$assert
+
+design -load prep
+
+chformal -assert2cover
+
+select -assert-count 1 t:$cover
+
+design -load prep
+
+chformal -assert2assume
+async2sync
+chformal -lower
+chformal -assume -early
+
+rename -enumerate -pattern assume_% t:$assume
+expose -evert t:$assume
+
+design -save gold
+
+design -load prep
+
+chformal -assert2assume
+chformal -assume -early
+async2sync
+chformal -lower
+
+rename -enumerate -pattern assume_% t:$assume
+expose -evert t:$assume
+
+design -save gate
+
+design -reset
+
+design -copy-from gold -as gold top
+design -copy-from gate -as gate top
+
+miter -equiv -flatten -make_assert gold gate miter
+
+sat -verify -prove-asserts -tempinduct miter