Update staged verification test

tests/staged_sim_and_verif/Req_Ack.sv

@@ -6,14 +6,14 @@ module DUT (
 
 `ifdef FORMAL
 
-        logic [1:0] reqs_seen;
-        logic [1:0] acks_seen;
+        logic [31:0] reqs_seen;
+        logic [31:0] acks_seen;
         logic [31:0] cycle_count;
 
         // Deterministic initial state
         initial begin
-                reqs_seen = 2'b0;
-                acks_seen = 2'b0;
+                reqs_seen = 32'b0;
+                acks_seen = 32'b0;
                 cycle_count = 32'b0;
         end
 
@@ -47,29 +47,30 @@ module DUT (
         // occurs. This leaves us in a state where we're waiting for the second
         // ack.
         always @(posedge clk) begin
-                phase1_reqs_seen: cover(reqs_seen == 2);
+                stage1_reqs_seen: cover(reqs_seen == 2);
         end
 
-        // In phase 2, assume that there's no more reqs; cover that an ack will
-        // eventually come for the second req, and separately prove bounded
-        // counts for reqs/acks.
+        // In stage 2, cover that the first ack arrives within a bounded window
+        // after the first req + another req arrives.
+        stage2_cover_ack_and_new_req: cover property (@(posedge clk)
+                $rose(ack) ##[1:$] (reqs_seen == 3)
+        );
+
+
+        // In stage 3, assume that there's no more reqs.
         always @ (posedge clk) begin
-                phase2_shared_no_new_req: assume(!req);
+                stage3_shared_no_new_req: assume(!req);
         end
 
+        // In stage 3a, cover the second ack arriving eventually.
         always @(posedge clk) begin
-                phase2a_cover_ack: cover(ack);
+                stage3a_cover_ack: cover(ack);
         end
 
-        // Assert the second ack arrives within a bounded window after the second
-        // request, and also that ack count never exceeds the expected two.
-        phase2b_assert_ack_reaches_two: assert property (@(posedge clk)
-                $rose(reqs_seen == 2) |-> ##[1:8] acks_seen == 2
+        // In stage 3b, assert that once we've seen 3 acks, we stay at 3 acks.
+        stage3b_acks_remains_3: assert property (
+                @(posedge clk) $rose(acks_seen == 3) |-> (acks_seen == 3)[*1:$]
         );
-        always @(posedge clk) begin
-                phase2b_assert_ack_stable: assert(acks_seen <= 2);
-        end
-
 
 `endif
 

tests/staged_sim_and_verif/skip_staged_flow.sby

@@ -1,78 +1,122 @@
 [tasks]
-stage_1_init init
-stage_1_cover cover
-stage_2_init init
-stage_2a_cover cover
-stage_2b_assert assert
+prep
+stage_1 cover
+stage_2 cover
+stage_3_init
+stage_3a_cover cover
+stage_3b_assert
 
 [options]
-init:
+prep:
 mode prep
 
 cover:
 mode cover
-depth 40
 skip_prep on
 
-assert:
+stage_3_init:
+mode prep
+skip_prep on
+
+stage_3b_assert:
 mode prove
-depth 40
 skip_prep on
 
 --
 
 [engines]
-init: none
-cover: smtbmc
-assert: smtbmc
+
+prep:
+none
+
+cover:
+smtbmc
+
+stage_3_init:
+none
+
+stage_3b_assert:
+smtbmc
+
+--
 
 [script]
-stage_1_init:
+
+# This separate prep step generates model_prep.il, which is our ground-truth
+# design file from which all other checkpoints are derived. It is essential
+# to have at least one prep step in `mode prep`, as we must produce a .il file
+# which has had the SBY-internal prep routine run on it. Any file written
+# in the user-provided script below will represent the state of the design 
+# *before* the SBY prep routine. (Note that the `prep` pass below is *not*
+# the SBY prep routine, but just the Yosys synthesis pass.)
+prep:
 verific -formal Req_Ack.sv
 hierarchy -top DUT
 prep
 
-stage_1_cover:
+stage_1:
 read_rtlil design_prep.il
-# This selection computes (all phase-labeled things) - (all phase-1-labeled
-# things) to remove all phase-tagged SVA constructs not intended for phase 1.
-select */c:phase* */c:phase1_* %d
+
+# Write checkpoint file.
+write_rtlil stage_1_init.il
+
+# This selection computes (all stage-labeled things) - (all stage-1-labeled
+# things) to remove all stage-tagged SVA constructs not intended for stage 1.
+select */c:stage* */c:stage1* %d
 delete
 
-stage_2_init:
-read_rtlil design_prep.il
+stage_2:
+# Read the stage 1 checkpoint, and then use the stage 1 trace to simulate up
+# to the end of stage 1.
+# Note that, in stage 2, we do not use -noinitstate on sim, as this first 
+# simulation begins at t=0 and thus $initstate cells should be active. All 
+# future calls to sim should include -noinitstate.
+read_rtlil stage_1_init.il
 sim -a -w -scope DUT -r trace0.yw
+write_rtlil stage_2_init.il
 
-stage_2a_cover:
-read_rtlil design_prep.il
-# This selection computes (all phase-labeled things) - (phase2 shared + phase2a)
-# to remove all phase-tagged SVA constructs not intended for this branch.
-select */c:phase* */c:phase2_shared_* */c:phase2a_* %u %d
+select */c:stage* */c:stage2* %d
 delete
 
-stage_2b_assert:
-read_rtlil design_prep.il
-# This selection computes (all phase-labeled things) - (phase2 shared + phase2b)
-# to remove all phase-tagged SVA constructs not intended for this branch.
-select */c:phase* */c:phase2_shared_* */c:phase2b_* %u %d
+stage_3_init:
+read_rtlil stage_2_init.il
+
+# Use -noinitstate, as this simulation does not begin at t=0.
+sim -a -w -scope DUT -r trace0.yw -noinitstate
+
+write_rtlil stage_3_init.il
+
+stage_3a_cover:
+read_rtlil stage_3_init.il
+select */c:stage* */c:stage3_shared* */c:stage3a* %u %d
+delete
+
+stage_3b_assert:
+read_rtlil stage_3_init.il
+select */c:stage* */c:stage3_shared* */c:stage3b* %u %d
 delete
 
+
 --
 
 [files]
 
-stage_1_init:
+prep:
 Req_Ack.sv
 
-stage_1_cover:
-skip_staged_flow_stage_1_init/model/design_prep.il
+stage_1:
+skip_staged_flow_prep/model/design_prep.il
+
+stage_2:
+skip_staged_flow_stage_1/src/stage_1_init.il
+skip_staged_flow_stage_1/engine_0/trace0.yw
 
-stage_2_init:
-skip_staged_flow_stage_1_init/model/design_prep.il
-skip_staged_flow_stage_1_cover/engine_0/trace0.yw
+stage_3_init:
+skip_staged_flow_stage_2/src/stage_2_init.il
+skip_staged_flow_stage_2/engine_0/trace0.yw
 
-stage_2a_cover:
-skip_staged_flow_stage_2_init/model/design_prep.il
+stage_3a_cover:
+skip_staged_flow_stage_3_init/src/stage_3_init.il
 
-stage_2b_assert:
-skip_staged_flow_stage_2_init/model/design_prep.il
+stage_3b_assert:
+skip_staged_flow_stage_3_init/src/stage_3_init.il

tests/staged_sim_and_verif/staged_sim_and_verif.sh

@@ -7,8 +7,9 @@ run_task() {
     python3 "$SBY_MAIN" -f "$FLOW_FILE" "$1"
 }
 
-run_task stage_1_init
-run_task stage_1_cover
-run_task stage_2_init
-run_task stage_2a_cover
-run_task stage_2b_assert
+run_task prep
+run_task stage_1
+run_task stage_2
+run_task stage_3_init
+run_task stage_3a_cover
+run_task stage_3b_assert