aboutsummaryrefslogtreecommitdiffstats
path: root/tests/arch
diff options
context:
space:
mode:
Diffstat (limited to 'tests/arch')
-rw-r--r--tests/arch/anlogic/dffs.ys3
-rw-r--r--tests/arch/ecp5/fsm.ys6
-rw-r--r--tests/arch/efinix/adffs.ys6
-rw-r--r--tests/arch/efinix/dffs.ys3
-rw-r--r--tests/arch/gowin/init.ys19
-rw-r--r--tests/arch/ice40/fsm.ys2
-rw-r--r--tests/arch/intel_alm/adffs.ys10
-rw-r--r--tests/arch/intel_alm/blockram.ys6
-rw-r--r--tests/arch/intel_alm/fsm.ys12
-rw-r--r--tests/arch/intel_alm/mux.ys8
-rw-r--r--tests/arch/xilinx/fsm.ys16
-rw-r--r--tests/arch/xilinx/latches.ys3
-rw-r--r--tests/arch/xilinx/pmgen_xilinx_srl.ys2
13 files changed, 46 insertions, 50 deletions
diff --git a/tests/arch/anlogic/dffs.ys b/tests/arch/anlogic/dffs.ys
index d3281ab89..deb90e051 100644
--- a/tests/arch/anlogic/dffs.ys
+++ b/tests/arch/anlogic/dffs.ys
@@ -15,6 +15,5 @@ proc
equiv_opt -assert -map +/anlogic/cells_sim.v synth_anlogic # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dffe # Constrain all select calls below inside the top module
-select -assert-count 1 t:AL_MAP_LUT3
select -assert-count 1 t:AL_MAP_SEQ
-select -assert-none t:AL_MAP_LUT3 t:AL_MAP_SEQ %% t:* %D
+select -assert-none t:AL_MAP_SEQ %% t:* %D
diff --git a/tests/arch/ecp5/fsm.ys b/tests/arch/ecp5/fsm.ys
index ba91e5fc0..a77986bbc 100644
--- a/tests/arch/ecp5/fsm.ys
+++ b/tests/arch/ecp5/fsm.ys
@@ -10,8 +10,8 @@ sat -verify -prove-asserts -show-public -set-at 1 in_reset 1 -seq 20 -prove-skip
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd fsm # Constrain all select calls below inside the top module
-select -assert-count 1 t:L6MUX21
-select -assert-count 15 t:LUT4
-select -assert-count 6 t:PFUMX
+select -assert-max 1 t:L6MUX21
+select -assert-max 16 t:LUT4
+select -assert-max 7 t:PFUMX
select -assert-count 6 t:TRELLIS_FF
select -assert-none t:L6MUX21 t:LUT4 t:PFUMX t:TRELLIS_FF %% t:* %D
diff --git a/tests/arch/efinix/adffs.ys b/tests/arch/efinix/adffs.ys
index 49dc7f256..86d446439 100644
--- a/tests/arch/efinix/adffs.ys
+++ b/tests/arch/efinix/adffs.ys
@@ -32,9 +32,8 @@ design -load postopt # load the post-opt design (otherwise equiv_opt loads the p
cd dffs # Constrain all select calls below inside the top module
select -assert-count 1 t:EFX_FF
select -assert-count 1 t:EFX_GBUFCE
-select -assert-count 1 t:EFX_LUT4
-select -assert-none t:EFX_FF t:EFX_GBUFCE t:EFX_LUT4 %% t:* %D
+select -assert-none t:EFX_FF t:EFX_GBUFCE %% t:* %D
design -load read
@@ -45,6 +44,5 @@ design -load postopt # load the post-opt design (otherwise equiv_opt loads the p
cd ndffnr # Constrain all select calls below inside the top module
select -assert-count 1 t:EFX_FF
select -assert-count 1 t:EFX_GBUFCE
-select -assert-count 1 t:EFX_LUT4
-select -assert-none t:EFX_FF t:EFX_GBUFCE t:EFX_LUT4 %% t:* %D
+select -assert-none t:EFX_FF t:EFX_GBUFCE %% t:* %D
diff --git a/tests/arch/efinix/dffs.ys b/tests/arch/efinix/dffs.ys
index af787ab67..f9111873c 100644
--- a/tests/arch/efinix/dffs.ys
+++ b/tests/arch/efinix/dffs.ys
@@ -19,6 +19,5 @@ design -load postopt # load the post-opt design (otherwise equiv_opt loads the p
cd dffe # Constrain all select calls below inside the top module
select -assert-count 1 t:EFX_FF
select -assert-count 1 t:EFX_GBUFCE
-select -assert-count 1 t:EFX_LUT4
-select -assert-none t:EFX_FF t:EFX_GBUFCE t:EFX_LUT4 %% t:* %D
+select -assert-none t:EFX_FF t:EFX_GBUFCE %% t:* %D
diff --git a/tests/arch/gowin/init.ys b/tests/arch/gowin/init.ys
index 88e88c15a..fba7c2fa5 100644
--- a/tests/arch/gowin/init.ys
+++ b/tests/arch/gowin/init.ys
@@ -45,24 +45,25 @@ flatten
synth_gowin -run coarse:
# check the flops mapped as expected
-select -assert-count 1 t:DFF
+select -assert-count 2 t:DFF
select -assert-count 1 t:DFFC
select -assert-count 1 t:DFFCE
-select -assert-count 1 t:DFFE
-select -assert-count 1 t:DFFN
+select -assert-count 0 t:DFFE
+select -assert-count 2 t:DFFN
select -assert-count 1 t:DFFNC
select -assert-count 1 t:DFFNCE
-select -assert-count 1 t:DFFNE
+select -assert-count 0 t:DFFNE
select -assert-count 1 t:DFFNP
select -assert-count 1 t:DFFNPE
select -assert-count 0 t:DFFNR
select -assert-count 0 t:DFFNRE
-select -assert-count 2 t:DFFNS
-select -assert-count 2 t:DFFNSE
+select -assert-count 3 t:DFFNS
+select -assert-count 1 t:DFFNSE
select -assert-count 1 t:DFFP
select -assert-count 1 t:DFFPE
select -assert-count 0 t:DFFR
select -assert-count 0 t:DFFRE
-select -assert-count 2 t:DFFS
-select -assert-count 2 t:DFFSE
-select -assert-count 12 t:LUT2
+select -assert-count 3 t:DFFS
+select -assert-count 1 t:DFFSE
+select -assert-count 4 t:LUT2
+select -assert-count 4 t:LUT4
diff --git a/tests/arch/ice40/fsm.ys b/tests/arch/ice40/fsm.ys
index 223ba070e..e3b746202 100644
--- a/tests/arch/ice40/fsm.ys
+++ b/tests/arch/ice40/fsm.ys
@@ -12,5 +12,5 @@ cd fsm # Constrain all select calls below inside the top module
select -assert-count 4 t:SB_DFF
select -assert-count 2 t:SB_DFFESR
-select -assert-count 15 t:SB_LUT4
+select -assert-max 15 t:SB_LUT4
select -assert-none t:SB_DFFESR t:SB_DFF t:SB_LUT4 %% t:* %D
diff --git a/tests/arch/intel_alm/adffs.ys b/tests/arch/intel_alm/adffs.ys
index 04fa2ad24..4565dcc64 100644
--- a/tests/arch/intel_alm/adffs.ys
+++ b/tests/arch/intel_alm/adffs.ys
@@ -77,10 +77,9 @@ equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd ndffnr # Constrain all select calls below inside the top module
select -assert-count 1 t:MISTRAL_FF
-select -assert-count 1 t:MISTRAL_NOT
-select -assert-count 1 t:MISTRAL_ALUT2
+select -assert-count 2 t:MISTRAL_NOT
-select -assert-none t:MISTRAL_FF t:MISTRAL_NOT t:MISTRAL_ALUT2 %% t:* %D
+select -assert-none t:MISTRAL_FF t:MISTRAL_NOT %% t:* %D
design -load read
@@ -90,7 +89,6 @@ equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd ndffnr # Constrain all select calls below inside the top module
select -assert-count 1 t:MISTRAL_FF
-select -assert-count 1 t:MISTRAL_NOT
-select -assert-count 1 t:MISTRAL_ALUT2
+select -assert-count 2 t:MISTRAL_NOT
-select -assert-none t:MISTRAL_FF t:MISTRAL_NOT t:MISTRAL_ALUT2 %% t:* %D
+select -assert-none t:MISTRAL_FF t:MISTRAL_NOT %% t:* %D
diff --git a/tests/arch/intel_alm/blockram.ys b/tests/arch/intel_alm/blockram.ys
new file mode 100644
index 000000000..610ae1ffd
--- /dev/null
+++ b/tests/arch/intel_alm/blockram.ys
@@ -0,0 +1,6 @@
+read_verilog ../common/blockram.v
+chparam -set ADDRESS_WIDTH 10 -set DATA_WIDTH 10 sync_ram_sdp
+synth_intel_alm -family cyclonev
+cd sync_ram_sdp
+select -assert-count 1 t:MISTRAL_M10K
+select -assert-none t:MISTRAL_M10K %% t:* %D
diff --git a/tests/arch/intel_alm/fsm.ys b/tests/arch/intel_alm/fsm.ys
index 6491b2e08..e54b5c21e 100644
--- a/tests/arch/intel_alm/fsm.ys
+++ b/tests/arch/intel_alm/fsm.ys
@@ -12,12 +12,13 @@ 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 6 t:MISTRAL_FF
+select -assert-max 1 t:MISTRAL_NOT
select -assert-max 2 t:MISTRAL_ALUT2 # Clang returns 2, GCC returns 1
-select -assert-count 1 t:MISTRAL_ALUT3
-select -assert-max 1 t:MISTRAL_ALUT4 # Clang returns 0, GCC returns 1
+select -assert-max 1 t:MISTRAL_ALUT3
+select -assert-max 2 t:MISTRAL_ALUT4 # Clang returns 0, GCC returns 1
select -assert-max 6 t:MISTRAL_ALUT5 # Clang returns 5, GCC returns 4
select -assert-max 2 t:MISTRAL_ALUT6 # Clang returns 1, GCC returns 2
-select -assert-none t:MISTRAL_FF t:MISTRAL_ALUT2 t:MISTRAL_ALUT3 t:MISTRAL_ALUT4 t:MISTRAL_ALUT5 t:MISTRAL_ALUT6 %% t:* %D
+select -assert-none t:MISTRAL_FF t:MISTRAL_NOT t:MISTRAL_ALUT2 t:MISTRAL_ALUT3 t:MISTRAL_ALUT4 t:MISTRAL_ALUT5 t:MISTRAL_ALUT6 %% t:* %D
design -reset
read_verilog ../common/fsm.v
@@ -34,9 +35,10 @@ 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 6 t:MISTRAL_FF
+select -assert-max 1 t:MISTRAL_NOT
select -assert-max 2 t:MISTRAL_ALUT2 # Clang returns 2, GCC returns 1
select -assert-max 2 t:MISTRAL_ALUT3 # Clang returns 2, GCC returns 1
-select -assert-max 1 t:MISTRAL_ALUT4 # Clang returns 0, GCC returns 1
+select -assert-max 2 t:MISTRAL_ALUT4 # Clang returns 0, GCC returns 1
select -assert-max 6 t:MISTRAL_ALUT5 # Clang returns 5, GCC returns 4
select -assert-max 2 t:MISTRAL_ALUT6 # Clang returns 1, GCC returns 2
-select -assert-none t:MISTRAL_FF t:MISTRAL_ALUT2 t:MISTRAL_ALUT3 t:MISTRAL_ALUT4 t:MISTRAL_ALUT5 t:MISTRAL_ALUT6 %% t:* %D
+select -assert-none t:MISTRAL_FF t:MISTRAL_NOT t:MISTRAL_ALUT2 t:MISTRAL_ALUT3 t:MISTRAL_ALUT4 t:MISTRAL_ALUT5 t:MISTRAL_ALUT6 %% t:* %D
diff --git a/tests/arch/intel_alm/mux.ys b/tests/arch/intel_alm/mux.ys
index d109257bd..01cc78e1b 100644
--- a/tests/arch/intel_alm/mux.ys
+++ b/tests/arch/intel_alm/mux.ys
@@ -48,9 +48,8 @@ equiv_opt -assert -map +/intel_alm/common/alm_sim.v synth_intel_alm -family cycl
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd mux8 # Constrain all select calls below inside the top module
select -assert-count 1 t:MISTRAL_ALUT3
-select -assert-count 1 t:MISTRAL_ALUT5
select -assert-count 2 t:MISTRAL_ALUT6
-select -assert-none t:MISTRAL_ALUT3 t:MISTRAL_ALUT5 t:MISTRAL_ALUT6 %% t:* %D
+select -assert-none t:MISTRAL_ALUT3 t:MISTRAL_ALUT6 %% t:* %D
design -load read
@@ -71,9 +70,8 @@ equiv_opt -assert -map +/intel_alm/common/alm_sim.v synth_intel_alm -family cycl
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd mux16 # Constrain all select calls below inside the top module
select -assert-count 1 t:MISTRAL_ALUT3
-select -assert-count 2 t:MISTRAL_ALUT5
-select -assert-count 4 t:MISTRAL_ALUT6
-select -assert-none t:MISTRAL_ALUT3 t:MISTRAL_ALUT5 t:MISTRAL_ALUT6 %% t:* %D
+select -assert-count 5 t:MISTRAL_ALUT6
+select -assert-none t:MISTRAL_ALUT3 t:MISTRAL_ALUT6 %% t:* %D
design -load read
diff --git a/tests/arch/xilinx/fsm.ys b/tests/arch/xilinx/fsm.ys
index fec4c6082..ace646af4 100644
--- a/tests/arch/xilinx/fsm.ys
+++ b/tests/arch/xilinx/fsm.ys
@@ -13,12 +13,11 @@ 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
stat
select -assert-count 1 t:BUFG
-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 6 t:FDRE
+select -assert-count 1 t:LUT4
+select -assert-count 4 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
+select -assert-none t:BUFG t:FDRE t:LUT4 t:LUT5 t:LUT6 %% t:* %D
design -load orig
@@ -32,7 +31,6 @@ stat
select -assert-count 1 t:BUFG
select -assert-count 6 t:FDRE
select -assert-count 1 t:LUT1
-select -assert-count 3 t:LUT3
-select -assert-count 6 t:LUT4
-select -assert-count 6 t:MUXF5
-select -assert-none t:BUFG t:FDRE t:LUT1 t:LUT3 t:LUT4 t:MUXF5 %% t:* %D
+select -assert-count 8 t:LUT4
+select -assert-count 5 t:MUXF5
+select -assert-none t:BUFG t:FDRE t:LUT1 t:LUT4 t:MUXF5 %% t:* %D
diff --git a/tests/arch/xilinx/latches.ys b/tests/arch/xilinx/latches.ys
index e226c2ec8..ee87fee21 100644
--- a/tests/arch/xilinx/latches.ys
+++ b/tests/arch/xilinx/latches.ys
@@ -18,9 +18,8 @@ equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad #
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd latchn # Constrain all select calls below inside the top module
select -assert-count 1 t:LDCE
-select -assert-count 1 t:INV
-select -assert-none t:LDCE t:INV %% t:* %D
+select -assert-none t:LDCE %% t:* %D
design -load read
diff --git a/tests/arch/xilinx/pmgen_xilinx_srl.ys b/tests/arch/xilinx/pmgen_xilinx_srl.ys
index e76fb20ab..9a5e70ea9 100644
--- a/tests/arch/xilinx/pmgen_xilinx_srl.ys
+++ b/tests/arch/xilinx/pmgen_xilinx_srl.ys
@@ -35,7 +35,6 @@ design -stash gate
design -copy-from gold -as gold pmtest_xilinx_srl_pm_fixed
design -copy-from gate -as gate pmtest_xilinx_srl_pm_fixed
-dff2dffe -unmap # sat does not support flops-with-enable yet
miter -equiv -flatten -make_assert gold gate miter
sat -set-init-zero -seq 5 -verify -prove-asserts miter
@@ -52,6 +51,5 @@ design -stash gate
design -copy-from gold -as gold pmtest_xilinx_srl_pm_variable
design -copy-from gate -as gate pmtest_xilinx_srl_pm_variable
-dff2dffe -unmap # sat does not support flops-with-enable yet
miter -equiv -flatten -make_assert gold gate miter
sat -set-init-zero -seq 5 -verify -prove-asserts miter
generated by cgit v1.2.3 (git 2.25.1) at 2025-09-10 03:22:38 +0000