3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-12-28 15:56:38 +00:00

Simplify script by relying on sby's prep routine

This commit is contained in:
Gus Smith 2025-12-15 12:41:47 -08:00
parent 1ee552a502
commit 9779436d0b

View file

@ -22,25 +22,20 @@ fv: smtbmc
stage_1_init:
verific -formal Req_Ack.sv
hierarchy -top DUT
setattr -set keep 1 w:\\*
prep -top DUT
flatten
write_rtlil stage_1_init.il
stage_1_fv:
read_rtlil stage_1_init.il
read_rtlil design_prep.il
# This selection computes (all things with phase)-(all things with phase=1)
# to remove all phased SVA constructs not intended for phase 1.
select */a:phase */a:phase=1 %d
delete
stage_2_init:
read_rtlil stage_1_init.il
read_rtlil design_prep.il
sim -a -w -scope DUT -r trace0.yw
write_rtlil stage_2_init.il
stage_2_fv:
read_rtlil stage_2_init.il
read_rtlil design_prep.il
# This selection computes (all things with phase)-(all things with phase=2)
# to remove all phased SVA constructs not intended for phase 2.
select */a:phase */a:phase=2 %d
@ -54,11 +49,11 @@ stage_1_init:
Req_Ack.sv
stage_1_fv:
skip_staged_flow_stage_1_init/src/stage_1_init.il
skip_staged_flow_stage_1_init/model/design_prep.il
stage_2_init:
skip_staged_flow_stage_1_init/src/stage_1_init.il
skip_staged_flow_stage_1_init/model/design_prep.il
skip_staged_flow_stage_1_fv/engine_0/trace0.yw
stage_2_fv:
skip_staged_flow_stage_2_init/src/stage_2_init.il
skip_staged_flow_stage_2_init/model/design_prep.il