mirror of
https://github.com/YosysHQ/sby.git
synced 2026-01-21 19:44:45 +00:00
Update sby file
This commit is contained in:
parent
5abce0c9ee
commit
531e328c3d
1 changed files with 28 additions and 11 deletions
|
|
@ -1,23 +1,30 @@
|
|||
[tasks]
|
||||
stage_1_init init
|
||||
stage_1_fv fv
|
||||
stage_1_cover cover
|
||||
stage_2_init init
|
||||
stage_2_fv fv
|
||||
stage_2a_cover cover
|
||||
stage_2b_assert assert
|
||||
|
||||
[options]
|
||||
init:
|
||||
mode prep
|
||||
|
||||
fv:
|
||||
cover:
|
||||
mode cover
|
||||
depth 40
|
||||
skip_prep on
|
||||
|
||||
assert:
|
||||
mode prove
|
||||
depth 40
|
||||
skip_prep on
|
||||
|
||||
--
|
||||
|
||||
[engines]
|
||||
init: none
|
||||
fv: smtbmc
|
||||
cover: smtbmc
|
||||
assert: smtbmc
|
||||
|
||||
[script]
|
||||
stage_1_init:
|
||||
|
|
@ -25,7 +32,7 @@ verific -formal Req_Ack.sv
|
|||
hierarchy -top DUT
|
||||
prep
|
||||
|
||||
stage_1_fv:
|
||||
stage_1_cover:
|
||||
read_rtlil design_prep.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.
|
||||
|
|
@ -36,11 +43,18 @@ stage_2_init:
|
|||
read_rtlil design_prep.il
|
||||
sim -a -w -scope DUT -r trace0.yw
|
||||
|
||||
stage_2_fv:
|
||||
stage_2a_cover:
|
||||
read_rtlil design_prep.il
|
||||
# This selection computes (all phase-labeled things) - (all phase-2-labeled
|
||||
# things) to remove all phase-tagged SVA constructs not intended for phase 2.
|
||||
select */c:phase* */c:phase2_* %d
|
||||
# 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
|
||||
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
|
||||
delete
|
||||
|
||||
--
|
||||
|
|
@ -50,12 +64,15 @@ delete
|
|||
stage_1_init:
|
||||
Req_Ack.sv
|
||||
|
||||
stage_1_fv:
|
||||
stage_1_cover:
|
||||
skip_staged_flow_stage_1_init/model/design_prep.il
|
||||
|
||||
stage_2_init:
|
||||
skip_staged_flow_stage_1_init/model/design_prep.il
|
||||
skip_staged_flow_stage_1_fv/engine_0/trace0.yw
|
||||
|
||||
stage_2_fv:
|
||||
stage_2a_cover:
|
||||
skip_staged_flow_stage_2_init/model/design_prep.il
|
||||
|
||||
stage_2b_assert:
|
||||
skip_staged_flow_stage_2_init/model/design_prep.il
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue