mirror of
https://github.com/YosysHQ/yosys
synced 2025-04-14 04:48:46 +00:00
107 lines
2.8 KiB
Plaintext
107 lines
2.8 KiB
Plaintext
### Original testcase ###
|
|
read_verilog ./dynamic_part_select/original.v
|
|
proc
|
|
rename -top gold
|
|
design -stash gold
|
|
|
|
read_verilog ./dynamic_part_select/original_gate.v
|
|
proc
|
|
rename -top gate
|
|
design -stash gate
|
|
|
|
design -copy-from gold -as gold gold
|
|
design -copy-from gate -as gate gate
|
|
|
|
miter -equiv -make_assert -make_outcmp -flatten gold gate equiv
|
|
sat -prove-asserts -seq 10 -show-public -verify -set-init-zero -ignore_unknown_cells equiv
|
|
|
|
### Multiple blocking assingments ###
|
|
design -reset
|
|
read_verilog ./dynamic_part_select/multiple_blocking.v
|
|
proc
|
|
rename -top gold
|
|
design -stash gold
|
|
|
|
read_verilog ./dynamic_part_select/multiple_blocking_gate.v
|
|
proc
|
|
rename -top gate
|
|
design -stash gate
|
|
|
|
design -copy-from gold -as gold gold
|
|
design -copy-from gate -as gate gate
|
|
|
|
miter -equiv -make_assert -make_outcmp -flatten gold gate equiv
|
|
sat -prove-asserts -seq 10 -show-public -verify -set-init-zero -ignore_unknown_cells equiv
|
|
|
|
### Non-blocking to the same output register ###
|
|
design -reset
|
|
read_verilog ./dynamic_part_select/nonblocking.v
|
|
proc
|
|
rename -top gold
|
|
design -stash gold
|
|
|
|
read_verilog ./dynamic_part_select/nonblocking_gate.v
|
|
proc
|
|
rename -top gate
|
|
design -stash gate
|
|
|
|
design -copy-from gold -as gold gold
|
|
design -copy-from gate -as gate gate
|
|
|
|
miter -equiv -make_assert -make_outcmp -flatten gold gate equiv
|
|
sat -prove-asserts -seq 10 -show-public -verify -set-init-zero -ignore_unknown_cells equiv
|
|
|
|
### For-loop select, one dynamic input
|
|
design -reset
|
|
read_verilog ./dynamic_part_select/forloop_select.v
|
|
proc
|
|
rename -top gold
|
|
design -stash gold
|
|
|
|
read_verilog ./dynamic_part_select/forloop_select_gate.v
|
|
proc
|
|
rename -top gate
|
|
design -stash gate
|
|
|
|
design -copy-from gold -as gold gold
|
|
design -copy-from gate -as gate gate
|
|
|
|
miter -equiv -make_assert -make_outcmp -flatten gold gate equiv
|
|
sat -prove-asserts -seq 10 -show-public -verify -set-init-zero -ignore_unknown_cells equiv
|
|
|
|
#### Double loop (part-select, reset) ###
|
|
design -reset
|
|
read_verilog ./dynamic_part_select/reset_test.v
|
|
proc
|
|
rename -top gold
|
|
design -stash gold
|
|
|
|
read_verilog ./dynamic_part_select/reset_test_gate.v
|
|
proc
|
|
rename -top gate
|
|
design -stash gate
|
|
|
|
design -copy-from gold -as gold gold
|
|
design -copy-from gate -as gate gate
|
|
|
|
miter -equiv -make_assert -make_outcmp -flatten gold gate equiv
|
|
sat -prove-asserts -seq 10 -show-public -verify -set-init-zero -ignore_unknown_cells equiv
|
|
|
|
### Reversed part-select case ###
|
|
design -reset
|
|
read_verilog ./dynamic_part_select/reversed.v
|
|
proc
|
|
rename -top gold
|
|
design -stash gold
|
|
|
|
read_verilog ./dynamic_part_select/reversed_gate.v
|
|
proc
|
|
rename -top gate
|
|
design -stash gate
|
|
|
|
design -copy-from gold -as gold gold
|
|
design -copy-from gate -as gate gate
|
|
|
|
miter -equiv -make_assert -make_outcmp -flatten gold gate equiv
|
|
sat -prove-asserts -seq 10 -show-public -verify -set-init-zero -ignore_unknown_cells equiv
|