aboutsummaryrefslogtreecommitdiffstats
path: root/tests/arch/xilinx/fsm.ys
diff options
context:
space:
mode:
authorN. Engelhardt <nak@symbioticeda.com>2020-01-03 12:28:48 +0100
committerN. Engelhardt <nak@symbioticeda.com>2020-01-03 12:28:48 +0100
commit341fd872b59e8f95aa14afd9f17225d2c03a4283 (patch)
tree21802e73ca767d124971d43d3f78d9f4cf7d62e2 /tests/arch/xilinx/fsm.ys
parentc8bc1793a4e8230c29fca4a34862414e8ab8722b (diff)
parentf8d5920a7e61f78873b7bf49dd7e8f3a83f7adf3 (diff)
downloadyosys-341fd872b59e8f95aa14afd9f17225d2c03a4283.tar.gz
yosys-341fd872b59e8f95aa14afd9f17225d2c03a4283.tar.bz2
yosys-341fd872b59e8f95aa14afd9f17225d2c03a4283.zip
Merge branch 'master' of https://github.com/YosysHQ/yosys into abc_scratchpad_script
Diffstat (limited to 'tests/arch/xilinx/fsm.ys')
-rw-r--r--tests/arch/xilinx/fsm.ys13
1 files changed, 7 insertions, 6 deletions
diff --git a/tests/arch/xilinx/fsm.ys b/tests/arch/xilinx/fsm.ys
index 2a72c34e8..3235d5af3 100644
--- a/tests/arch/xilinx/fsm.ys
+++ b/tests/arch/xilinx/fsm.ys
@@ -3,7 +3,7 @@ hierarchy -top fsm
proc
flatten
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
+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 -set-at 1 in_reset 1 -seq 20 -prove-skip 1 miter
@@ -11,8 +11,9 @@ design -load postopt # load the post-opt design (otherwise equiv_opt loads the p
cd fsm # Constrain all select calls below inside the top module
select -assert-count 1 t:BUFG
-select -assert-count 5 t:FDRE
-select -assert-count 1 t:LUT3
-select -assert-count 2 t:LUT4
-select -assert-count 4 t:LUT6
-select -assert-none t:BUFG t:FDRE t:LUT3 t:LUT4 t:LUT6 %% t:* %D
+select -assert-count 4 t:FDRE
+select -assert-count 1 t:FDSE
+select -assert-count 1 t:LUT2
+select -assert-count 3 t:LUT5
+select -assert-count 1 t:LUT6
+select -assert-none t:BUFG t:FDRE t:FDSE t:LUT2 t:LUT5 t:LUT6 %% t:* %D