diff --git a/tests/staged_sim_and_verif/README.md b/tests/staged_sim_and_verif/README.md index 6cb81e8..e47f8a9 100644 --- a/tests/staged_sim_and_verif/README.md +++ b/tests/staged_sim_and_verif/README.md @@ -1,4 +1,7 @@ Staged simulation + verification example demonstrating staged verification using simulation and writeback via `sim -w` pass. + +This test mirrors what is described in , and should be kept up to date with that appnote. + - Stage 1: run cover to reach “req sent, ack pending”, producing `trace0.yw`. - Stage 2A (cover branch): replay the witness with `sim -w` to bake state, then run another cover that requires the ack. - Stage 2B (assert branch): replay the same baked state and assert there is at most one further ack after the second req. diff --git a/tests/staged_sim_and_verif/Req_Ack.sv b/tests/staged_sim_and_verif/Req_Ack.sv index e1fd0e0..145dd97 100644 --- a/tests/staged_sim_and_verif/Req_Ack.sv +++ b/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. - always @ (posedge clk) begin - phase2_shared_no_new_req: assume(!req); - end - - always @(posedge clk) begin - phase2a_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 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) ); - always @(posedge clk) begin - phase2b_assert_ack_stable: assert(acks_seen <= 2); + + + // In stage 3, assume that there's no more reqs. + always @ (posedge clk) begin + stage3_shared_no_new_req: assume(!req); end + // In stage 3a, cover the second ack arriving eventually. + always @(posedge clk) begin + stage3a_cover_ack: cover(ack); + end + + // 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:$] + ); `endif diff --git a/tests/staged_sim_and_verif/skip_staged_flow.sby b/tests/staged_sim_and_verif/skip_staged_flow.sby index 12a011e..da94b05 100644 --- a/tests/staged_sim_and_verif/skip_staged_flow.sby +++ b/tests/staged_sim_and_verif/skip_staged_flow.sby @@ -1,78 +1,106 @@ [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: + +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_rtlil stage_1_init.il + +select */c:stage* */c:stage1* %d delete -stage_2_init: -read_rtlil design_prep.il +stage_2: +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 + +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_init: -skip_staged_flow_stage_1_init/model/design_prep.il -skip_staged_flow_stage_1_cover/engine_0/trace0.yw +stage_2: +skip_staged_flow_stage_1/src/stage_1_init.il +skip_staged_flow_stage_1/engine_0/trace0.yw -stage_2a_cover: -skip_staged_flow_stage_2_init/model/design_prep.il +stage_3_init: +skip_staged_flow_stage_2/src/stage_2_init.il +skip_staged_flow_stage_2/engine_0/trace0.yw -stage_2b_assert: -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_3b_assert: +skip_staged_flow_stage_3_init/src/stage_3_init.il diff --git a/tests/staged_sim_and_verif/staged_sim_and_verif.sh b/tests/staged_sim_and_verif/staged_sim_and_verif.sh index a7426b8..720865b 100755 --- a/tests/staged_sim_and_verif/staged_sim_and_verif.sh +++ b/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