Update sby file for new stages

tests/staged_sim_and_verif/skip_staged_flow.sby

@@ -1,78 +1,100 @@
 [tasks]
-stage_1_init init
-stage_1_cover cover
-stage_2_init init
-stage_2a_cover cover
-stage_2b_assert assert
+stage_1
+stage_2
+stage_3_init
+stage_3a_cover
+stage_3b_assert
 
 [options]
-init:
-mode prep
-
-cover:
+stage_1:
+mode cover
+
+stage_2:
 mode cover
-depth 40
 skip_prep on
 
-assert:
+stage_3_init:
+mode prep
+skip_prep on
+
+stage_3a_cover:
+mode cover
+skip_prep on
+
+stage_3b_assert:
 mode prove
-depth 40
 skip_prep on
 
 --
 
 [engines]
-init: none
-cover: smtbmc
-assert: smtbmc
+smtbmc
+
+stage_3_init:
+none
+
+--
 
 [script]
-stage_1_init:
+stage_1:
 verific -formal Req_Ack.sv
 hierarchy -top DUT
 prep
 
-stage_1_cover:
-read_rtlil design_prep.il
+# Write checkpoint file.
+write_rtlil stage_1_init.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
+select */c:phase* */c:phase1* %d
 delete
 
-stage_2_init:
-read_rtlil design_prep.il
+stage_2:
+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
 
-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
+write_rtlil stage_2_init.il
+select */c:phase* */c:phase2* %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:phase* */c:phase3_shared* */c:phase3a* %u %d
 delete
 
+stage_3b_assert:
+read_rtlil stage_3_init.il
+select */c:phase* */c:phase3_shared_* */c:phase3b* %u %d
+delete
+
+
 --
 
 [files]
 
-stage_1_init:
+stage_1:
 Req_Ack.sv
 
-stage_1_cover:
-skip_staged_flow_stage_1_init/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