Additional tests for FV $check compatibility

tests/various/chformal_check.ys

@@ -0,0 +1,68 @@
+read_verilog -formal <<EOT
+
+module top(input clk, a, en);
+    wire a_q = '0;
+    wire 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:$check r:FLAVOR=assert %i
+
+chformal -assert2assume
+
+select -assert-count 1 t:$check r:FLAVOR=assume %i
+
+chformal -assume2assert
+
+select -assert-count 1 t:$check r:FLAVOR=assert %i
+
+async2sync
+
+chformal -lower
+select -assert-count 1 t:$assert
+
+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

tests/various/chformal_coverenable.ys

@@ -2,10 +2,10 @@ read_verilog -formal <<EOT
 module top(input a, b, c, d);
 
     always @* begin
-        if (a) assert (b == c);
+        if (a) c0: assert (b == c);
-        if (!a) assert (b != c);
+        if (!a) c1: assert (b != c);
-        if (b) assume (c);
+        if (b) c2: assume (c);
-        if (c) cover (d);
+        if (c) c3: cover (d);
     end
 
 endmodule
@@ -27,3 +27,36 @@ select -assert-count 4 t:$cover
 
 chformal -assume -coverenable
 select -assert-count 5 t:$cover
+
+autoname */t:$cover
+expose -evert */c? */c?_EN_$cover_*
+
+design -save a2s_first
+
+design -load prep
+select -assert-count 1 r:FLAVOR=cover
+
+chformal -cover -coverenable
+select -assert-count 2 r:FLAVOR=cover
+
+chformal -assert -coverenable
+select -assert-count 4 r:FLAVOR=cover
+
+chformal -assume -coverenable
+select -assert-count 5 r:FLAVOR=cover
+
+async2sync
+
+autoname */t:$cover
+expose -evert */c? */c?_EN_$cover_*
+
+design -save a2s_last
+
+design -reset
+
+design -copy-from a2s_first -as gold top
+design -copy-from a2s_last -as gate top
+
+miter -equiv -flatten -make_assert gold gate miter
+
+sat -verify -prove-asserts -tempinduct miter

tests/various/clk2fflogic_effects.sh

@@ -0,0 +1,27 @@
+#!/usr/bin/env bash
+set -ex
+
+../../yosys -p "
+read_verilog -formal -DFAST clk2fflogic_effects.sv
+hierarchy -top top; proc;;
+tee -o clk2fflogic_effects.sim.log sim -fst /tmp/sim.fst -q -n 16
+"
+
+../../yosys -p "
+read_verilog -formal -DFAST clk2fflogic_effects.sv
+hierarchy -top top; proc;;
+clk2fflogic;;
+
+tee -o clk2fflogic_effects.clk2fflogic.log sim -fst /tmp/sim.fst -q -n 16
+"
+
+iverilog -g2012 -o clk2fflogic_effects.iv.out clk2fflogic_effects.sv
+
+./clk2fflogic_effects.iv.out > clk2fflogic_effects.iv.log
+
+sort clk2fflogic_effects.iv.log > clk2fflogic_effects.iv.sorted.log
+tail +3 clk2fflogic_effects.sim.log | sort > clk2fflogic_effects.sim.sorted.log
+tail +3 clk2fflogic_effects.clk2fflogic.log | sort > clk2fflogic_effects.clk2fflogic.sorted.log
+
+cmp clk2fflogic_effects.iv.sorted.log clk2fflogic_effects.sim.sorted.log
+cmp clk2fflogic_effects.iv.sorted.log clk2fflogic_effects.clk2fflogic.sorted.log

tests/various/clk2fflogic_effects.sv

@@ -0,0 +1,82 @@
+module top;
+
+(* gclk *)
+reg gclk;
+
+reg clk = 0;
+always @(posedge gclk)
+    clk <= !clk;
+
+reg [4:0] counter = 0;
+
+reg eff_0_trg = '0;
+reg eff_0_en = '0;
+
+reg eff_1_trgA = '0;
+reg eff_1_trgB = '0;
+reg eff_1_en = '0;
+
+reg eff_2_trgA = '0;
+reg eff_2_trgB = '0;
+reg eff_2_en = '0;
+
+`ifdef FAST
+always @(posedge gclk) begin
+`else
+always @(posedge clk) begin
+`endif
+    counter <= counter + 1;
+
+    eff_0_trg = 32'b00000000000000110011001100101010 >> counter;
+    eff_0_en <= 32'b00000000000001100000110110110110 >> counter;
+
+    eff_1_trgA = 32'b00000000000000000011110000011110 >> counter;
+    eff_1_trgB = 32'b00000000000000001111000001111000 >> counter;
+    eff_1_en  <= 32'b00000000000000001010101010101010 >> counter;
+
+    eff_2_trgA = counter[0];
+    eff_2_trgB = !counter[0];
+    eff_2_en  <= 32'b00000000000000000000001111111100 >> counter;
+end
+
+always @(posedge eff_0_trg)
+    if (eff_0_en)
+        $display("%02d: eff0 +", counter);
+
+always @(negedge eff_0_trg)
+    if (eff_0_en)
+        $display("%02d: eff0 -", counter);
+
+always @(posedge eff_0_trg, negedge eff_0_trg)
+    if (eff_0_en)
+        $display("%02d: eff0 *", counter);
+
+always @(posedge eff_1_trgA, posedge eff_1_trgB)
+    if (eff_1_en)
+        $display("%02d: eff1 ++", counter);
+
+always @(posedge eff_1_trgA, negedge eff_1_trgB)
+    if (eff_1_en)
+        $display("%02d: eff1 +-", counter);
+
+always @(negedge eff_1_trgA, posedge eff_1_trgB)
+    if (eff_1_en)
+        $display("%02d: eff1 -+", counter);
+
+always @(negedge eff_1_trgA, negedge eff_1_trgB)
+    if (eff_1_en)
+        $display("%02d: eff1 --", counter);
+
+always @(posedge eff_2_trgA, posedge eff_2_trgB)
+    if (eff_2_en)
+        $display("repeated");
+
+`ifdef __ICARUS__
+initial gclk = 0;
+always @(gclk) gclk <= #5 !gclk;
+always @(posedge gclk)
+    if (counter == 31)
+        $finish(0);
+`endif
+
+endmodule