mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2026-02-22 03:07:38 +00:00
Code Activity

Remove comments and point to appnote

Browse source 
Instead of duplicating editorial comments in the test, we should just
point to the appnote where the comments are already made in a more
substantive way.
This commit is contained in:
Gus Smith 2026-02-18 08:20:51 -08:00
parent e89f71b3cb
commit 551d8df2a9
2 changed files with 3 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

3
tests/staged_sim_and_verif/README.md
View file

@ -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 <https://yosyshq.readthedocs.io/projects/ap130/en/latest/>, 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.

16
tests/staged_sim_and_verif/skip_staged_flow.sby
View file

@ -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