Skip to content

Commit

Permalink
cutpoint t:$mul
Browse files Browse the repository at this point in the history
Use `cutpoint t:$mul` instead of specifying the multiplier.  Added to veer and cv32.  In cv32 it also caught multiplier cells in some of the assertions (which probably need to have a `chformal -remove` done to them).
  • Loading branch information
KrystalDelusion committed Feb 22, 2024
1 parent 5fb771f commit ae7976f
Show file tree
Hide file tree
Showing 2 changed files with 5 additions and 4 deletions.
5 changes: 2 additions & 3 deletions cv32e40x/cv32e40x.sby
Original file line number Diff line number Diff line change
Expand Up @@ -53,9 +53,8 @@ verific -formal formal_setup.sv
## import from verific to yosys
hierarchy -top uvmt_cv32e40x_tb
## cut mult
### ex_stage name includes parameters:
### e.g. cv32e40x_ex_stage(B_EXT=B_NONE_cv32e40x_pkg,M_EXT=M_cv32e40x_pkg)_0
cutpoint cv32e40x_ex_stage*_0/mul.mult_i
### should match cv32e40x_ex_stage(B_EXT=B_NONE_cv32e40x_pkg,M_EXT=M_cv32e40x_pkg)_0/mul.mult_i
cutpoint t:$mul
## this flatten is needed to work around an issue with SV interfaces
flatten
## prepare design
Expand Down
4 changes: 3 additions & 1 deletion veer/veer_benchmark.sby
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,7 @@ fail: expect fail

[engines]
bmc: smtbmc
pdr: abc pdr
pdr: abc --keep-going pdr
cover: smtbmc

[script]
Expand All @@ -37,6 +37,8 @@ verific -import -extnets veer_wrapper

tee -o ../hierarchy.log hierarchy -top veer_wrapper

cutpoint t:$mul

prep -flatten

# dma_axi requires axi to be setup
Expand Down

0 comments on commit ae7976f

Please sign in to comment.