mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-08-14 23:05:28 +00:00
Code Activity

tests: Add equiv_induct to equiv_assume.ys

Browse source
This commit is contained in:
Krystine Sherwin 2025-08-06 15:13:04 +12:00
parent 93b39ad9b3
commit f9e8127e2b
No known key found for this signature in database
1 changed files with 25 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

25
tests/various/equiv_assume.ys
View file

@ -22,11 +22,18 @@ sat -set-assumes -prove-asserts -verify
# sat -prove-asserts -verify # sat -prove-asserts -verify
# so should $equiv # so should $equiv
## in equiv_simple
design -load input design -load input
equiv_make gold gate equiv equiv_make gold gate equiv
equiv_simple -set-assumes equiv equiv_simple -set-assumes equiv
equiv_status -assert equiv equiv_status -assert equiv
## and equiv_induct
delete equiv
equiv_make gold gate equiv
equiv_induct -set-assumes equiv
equiv_status -assert equiv
# and it works through cells # and it works through cells
design -reset design -reset
read_verilog -sv <<EOT read_verilog -sv <<EOT
@ -55,6 +62,11 @@ equiv_make gold gate equiv
equiv_simple -set-assumes equiv equiv_simple -set-assumes equiv
equiv_status -assert equiv equiv_status -assert equiv
delete equiv
equiv_make gold gate equiv
equiv_induct -set-assumes equiv
equiv_status -assert equiv
# and registers # and registers
design -reset design -reset
read_verilog -sv <<EOT read_verilog -sv <<EOT
@ -87,6 +99,11 @@ equiv_make gold gate equiv
equiv_simple -set-assumes equiv equiv_simple -set-assumes equiv
equiv_status -assert equiv equiv_status -assert equiv
delete equiv
equiv_make gold gate equiv
equiv_induct -set-assumes equiv
equiv_status -assert equiv
# so long as the assumption doesn't end up after the equiv # so long as the assumption doesn't end up after the equiv
design -reset design -reset
read_verilog -sv <<EOT read_verilog -sv <<EOT
@ -105,6 +122,9 @@ chformal -lower
async2sync async2sync
design -stash input4 design -stash input4
logger -expect log "model found: FAIL!" 1
logger -expect log "Found a total of 2 unproven .equiv cells." 2
design -load input4 design -load input4
equiv_make -make_assert gold gate equiv equiv_make -make_assert gold gate equiv
prep -top equiv prep -top equiv
@ -114,3 +134,8 @@ design -load input4
equiv_make gold gate equiv equiv_make gold gate equiv
equiv_simple -set-assumes equiv equiv_simple -set-assumes equiv
equiv_status equiv equiv_status equiv
delete equiv
equiv_make gold gate equiv
equiv_induct -set-assumes equiv
equiv_status equiv