mirror of
https://github.com/YosysHQ/yosys
synced 2025-04-14 12:58:45 +00:00
60 lines
2.1 KiB
Plaintext
60 lines
2.1 KiB
Plaintext
#### Original testcase ###
|
|
read_verilog ../common/dynamic_part_select/original.v
|
|
hierarchy -top original
|
|
prep -flatten -top original
|
|
design -save gold
|
|
|
|
equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad
|
|
miter -equiv -make_assert -flatten gold gate miter
|
|
sat -verify -prove-asserts -show-public -seq 10 -prove-skip 1 miter
|
|
|
|
### Multiple blocking assingments ###
|
|
read_verilog ../common/dynamic_part_select/multiple_blocking.v
|
|
hierarchy -top multiple_blocking
|
|
prep -flatten -top multiple_blocking
|
|
design -save gold
|
|
|
|
equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad
|
|
miter -equiv -make_assert -flatten gold gate miter
|
|
sat -verify -prove-asserts -show-public -seq 10 -prove-skip 1 miter
|
|
|
|
### Non-blocking to the same output register ###
|
|
read_verilog ../common/dynamic_part_select/nonblocking.v
|
|
hierarchy -top nonblocking
|
|
prep -flatten -top nonblocking
|
|
design -save gold
|
|
|
|
equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad
|
|
miter -equiv -make_assert -flatten gold gate miter
|
|
sat -verify -prove-asserts -show-public -seq 10 -prove-skip 1 miter
|
|
|
|
### For-loop select, one dynamic input
|
|
read_verilog ../common/dynamic_part_select/forloop_select.v
|
|
hierarchy -top forloop_select
|
|
prep -flatten -top forloop_select
|
|
design -save gold
|
|
|
|
equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad
|
|
miter -equiv -make_assert -flatten gold gate miter
|
|
sat -verify -prove-asserts -show-public -seq 5 -prove-skip 1 miter
|
|
|
|
### Double loop (part-select, reset) ###
|
|
read_verilog ../common/dynamic_part_select/reset_test.v
|
|
hierarchy -top reset_test
|
|
prep -flatten -top reset_test
|
|
design -save gold
|
|
|
|
equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad
|
|
miter -equiv -make_assert -flatten gold gate miter
|
|
sat -verify -prove-asserts -show-public -seq 10 -prove-skip 1 miter
|
|
|
|
### Reversed part-select case ###
|
|
read_verilog ../common/dynamic_part_select/reversed.v
|
|
hierarchy -top reversed
|
|
prep -flatten -top reversed
|
|
design -save gold
|
|
|
|
equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad
|
|
miter -equiv -make_assert -flatten gold gate miter
|
|
sat -verify -prove-asserts -show-public -seq 20 -prove-skip 1 miter
|