Merge pull request #5179 from YosysHQ/krys/assert2cover

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