Revive an independent prep stage

tests/staged_sim_and_verif/skip_staged_flow.sby

@@ -1,4 +1,5 @@
 [tasks]
+prep
 stage_1
 stage_2
 stage_3_init
@@ -6,8 +7,12 @@ stage_3a_cover
 stage_3b_assert
 
 [options]
+prep:
+mode prep
+
 stage_1:
 mode cover
+skip_prep on
 
 stage_2:
 mode cover
@@ -30,17 +35,31 @@ skip_prep on
 [engines]
 smtbmc
 
+prep:
+none
+
 stage_3_init:
 none
 
 --
 
 [script]
-stage_1:
+
+# 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:
+read_rtlil design_prep.il
+
 # Write checkpoint file.
 write_rtlil stage_1_init.il
 
@@ -50,12 +69,15 @@ select */c:phase* */c:phase1* %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
-# Note that, in stage 2, we do not use -noinitstate, as this first simulation
-# begins at t=0. All future calls to sim should include -noinitstate.
 sim -a -w -scope DUT -r trace0.yw
-
 write_rtlil stage_2_init.il
+
 select */c:phase* */c:phase2* %d
 delete
 
@@ -82,9 +104,12 @@ delete
 
 [files]
 
-stage_1:
+prep:
 Req_Ack.sv
 
+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

tests/staged_sim_and_verif/staged_sim_and_verif.sh

@@ -7,6 +7,7 @@ run_task() {
     python3 "$SBY_MAIN" -f "$FLOW_FILE" "$1"
 }
 
+run_task prep
 run_task stage_1
 run_task stage_2
 run_task stage_3_init