aboutsummaryrefslogtreecommitdiffstats
path: root/tests/various/dynamic_part_select.ys
diff options
context:
space:
mode:
Diffstat (limited to 'tests/various/dynamic_part_select.ys')
-rw-r--r--tests/various/dynamic_part_select.ys76
1 files changed, 66 insertions, 10 deletions
diff --git a/tests/various/dynamic_part_select.ys b/tests/various/dynamic_part_select.ys
index abc1daad6..2dc061e89 100644
--- a/tests/various/dynamic_part_select.ys
+++ b/tests/various/dynamic_part_select.ys
@@ -21,18 +21,18 @@ 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
@@ -44,13 +44,13 @@ 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
@@ -62,13 +62,13 @@ 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
@@ -83,10 +83,10 @@ 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
@@ -101,6 +101,62 @@ 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