mirror of https://github.com/YosysHQ/yosys.git
181 lines
4.7 KiB
Plaintext
181 lines
4.7 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 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 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 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 equiv
|
|
|
|
### For-loop select, one dynamic input, (* nowrshmsk *)
|
|
design -reset
|
|
read_verilog ./dynamic_part_select/forloop_select_nowrshmsk.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 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 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 equiv
|
|
|
|
### Latches
|
|
## Issue 1990
|
|
design -reset
|
|
read_verilog ./dynamic_part_select/latch_1990.v
|
|
hierarchy -top latch_1990; prep; async2sync
|
|
rename -top gold
|
|
design -stash gold
|
|
|
|
read_verilog ./dynamic_part_select/latch_1990_gate.v
|
|
hierarchy -top latch_1990_gate; prep
|
|
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 -show-public -verify -set-init-zero equiv
|
|
|
|
###
|
|
## Part select with obvious latch, expected to fail due comparison with old shift&mask AST transformation
|
|
design -reset
|
|
read_verilog ./dynamic_part_select/latch_002.v
|
|
hierarchy -top latch_002; prep; async2sync
|
|
rename -top gold
|
|
design -stash gold
|
|
|
|
read_verilog ./dynamic_part_select/latch_002_gate.v
|
|
hierarchy -top latch_002_gate; prep; async2sync
|
|
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 -falsify -set-init-zero equiv
|
|
|
|
## Part select + latch, with no shift&mask
|
|
design -reset
|
|
read_verilog ./dynamic_part_select/latch_002.v
|
|
hierarchy -top latch_002; prep; async2sync
|
|
rename -top gold
|
|
design -stash gold
|
|
|
|
read_verilog ./dynamic_part_select/latch_002_gate_good.v
|
|
hierarchy -top latch_002_gate; prep; async2sync
|
|
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 equiv
|