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/skip_staged_flow.sby b/tests/staged_sim_and_verif/skip_staged_flow.sby index 41b575a..da94b05 100644 --- a/tests/staged_sim_and_verif/skip_staged_flow.sby +++ b/tests/staged_sim_and_verif/skip_staged_flow.sby @@ -42,13 +42,6 @@ smtbmc [script] -# 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 @@ -57,20 +50,12 @@ prep stage_1: read_rtlil design_prep.il -# 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: -# 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 @@ -81,7 +66,6 @@ delete 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