diff options
Diffstat (limited to 'tests/arch')
51 files changed, 792 insertions, 206 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/anlogic/latches.ys b/tests/arch/anlogic/latches.ys index 8d66f77b3..34a3b14d0 100644 --- a/tests/arch/anlogic/latches.ys +++ b/tests/arch/anlogic/latches.ys @@ -3,31 +3,33 @@ design -save read hierarchy -top latchp proc -# Can't run any sort of equivalence check because latches are blown to LUTs -synth_anlogic +equiv_opt -assert -multiclock -map +/anlogic/cells_sim.v synth_anlogic +design -load postopt cd latchp # Constrain all select calls below inside the top module -select -assert-count 1 t:AL_MAP_LUT3 -select -assert-none t:AL_MAP_LUT3 %% t:* %D +select -assert-count 1 t:AL_MAP_SEQ +select -assert-count 1 t:AL_MAP_LUT1 +select -assert-none t:AL_MAP_SEQ t:AL_MAP_LUT1 %% t:* %D design -load read hierarchy -top latchn proc -# Can't run any sort of equivalence check because latches are blown to LUTs -synth_anlogic +equiv_opt -assert -multiclock -map +/anlogic/cells_sim.v synth_anlogic +design -load postopt cd latchn # Constrain all select calls below inside the top module -select -assert-count 1 t:AL_MAP_LUT3 -select -assert-none t:AL_MAP_LUT3 %% t:* %D +select -assert-count 1 t:AL_MAP_SEQ +select -assert-none t:AL_MAP_SEQ %% t:* %D design -load read hierarchy -top latchsr proc -# Can't run any sort of equivalence check because latches are blown to LUTs -synth_anlogic +equiv_opt -assert -multiclock -map +/anlogic/cells_sim.v synth_anlogic +design -load postopt cd latchsr # Constrain all select calls below inside the top module -select -assert-count 1 t:AL_MAP_LUT5 -select -assert-none t:AL_MAP_LUT5 %% t:* %D +select -assert-count 1 t:AL_MAP_SEQ +select -assert-count 2 t:AL_MAP_LUT3 +select -assert-none t:AL_MAP_SEQ t:AL_MAP_LUT3 %% t:* %D diff --git a/tests/arch/anlogic/run-test.sh b/tests/arch/anlogic/run-test.sh index bf19b887d..4be4b70ae 100755 --- a/tests/arch/anlogic/run-test.sh +++ b/tests/arch/anlogic/run-test.sh @@ -1,20 +1,4 @@ #!/usr/bin/env bash -set -e -{ -echo "all::" -for x in *.ys; do - echo "all:: run-$x" - echo "run-$x:" - echo " @echo 'Running $x..'" - echo " @../../../yosys -ql ${x%.ys}.log -w 'Yosys has only limited support for tri-state logic at the moment.' $x" -done -for s in *.sh; do - if [ "$s" != "run-test.sh" ]; then - echo "all:: run-$s" - echo "run-$s:" - echo " @echo 'Running $s..'" - echo " @bash $s" - fi -done -} > run-test.mk -exec ${MAKE:-make} -f run-test.mk +set -eu +source ../../gen-tests-makefile.sh +run_tests --yosys-scripts --bash --yosys-args "-w 'Yosys has only limited support for tri-state logic at the moment.'" diff --git a/tests/arch/common/mul.v b/tests/arch/common/mul.v index 437a91cfc..baed64fcd 100644 --- a/tests/arch/common/mul.v +++ b/tests/arch/common/mul.v @@ -1,9 +1,10 @@ module top +#(parameter X_WIDTH=6, Y_WIDTH=6, A_WIDTH=12) ( - input [5:0] x, - input [5:0] y, + input [X_WIDTH-1:0] x, + input [Y_WIDTH-1:0] y, - output [11:0] A, + output [A_WIDTH-1:0] A, ); assign A = x * y; endmodule diff --git a/tests/arch/ecp5/bug2409.ys b/tests/arch/ecp5/bug2409.ys new file mode 100644 index 000000000..5ba9cec17 --- /dev/null +++ b/tests/arch/ecp5/bug2409.ys @@ -0,0 +1,24 @@ +read_verilog <<EOT +module t (...); + +input CLK; +input [10:0] A; +input WE; +input C; +input [7:0] DI; +output reg [7:0] DO; + +reg [7:0] mem[2047:0]; + +always @(posedge CLK) begin + if (C) + if (WE) + mem[A] <= DI; + DO <= mem[A]; +end + +endmodule +EOT + +synth_ecp5 +select -assert-count 1 t:DP16KD 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/ecp5/run-test.sh b/tests/arch/ecp5/run-test.sh index bf19b887d..4be4b70ae 100755 --- a/tests/arch/ecp5/run-test.sh +++ b/tests/arch/ecp5/run-test.sh @@ -1,20 +1,4 @@ #!/usr/bin/env bash -set -e -{ -echo "all::" -for x in *.ys; do - echo "all:: run-$x" - echo "run-$x:" - echo " @echo 'Running $x..'" - echo " @../../../yosys -ql ${x%.ys}.log -w 'Yosys has only limited support for tri-state logic at the moment.' $x" -done -for s in *.sh; do - if [ "$s" != "run-test.sh" ]; then - echo "all:: run-$s" - echo "run-$s:" - echo " @echo 'Running $s..'" - echo " @bash $s" - fi -done -} > run-test.mk -exec ${MAKE:-make} -f run-test.mk +set -eu +source ../../gen-tests-makefile.sh +run_tests --yosys-scripts --bash --yosys-args "-w 'Yosys has only limited support for tri-state logic at the moment.'" 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/efinix/run-test.sh b/tests/arch/efinix/run-test.sh index bf19b887d..4be4b70ae 100755 --- a/tests/arch/efinix/run-test.sh +++ b/tests/arch/efinix/run-test.sh @@ -1,20 +1,4 @@ #!/usr/bin/env bash -set -e -{ -echo "all::" -for x in *.ys; do - echo "all:: run-$x" - echo "run-$x:" - echo " @echo 'Running $x..'" - echo " @../../../yosys -ql ${x%.ys}.log -w 'Yosys has only limited support for tri-state logic at the moment.' $x" -done -for s in *.sh; do - if [ "$s" != "run-test.sh" ]; then - echo "all:: run-$s" - echo "run-$s:" - echo " @echo 'Running $s..'" - echo " @bash $s" - fi -done -} > run-test.mk -exec ${MAKE:-make} -f run-test.mk +set -eu +source ../../gen-tests-makefile.sh +run_tests --yosys-scripts --bash --yosys-args "-w 'Yosys has only limited support for tri-state logic at the moment.'" diff --git a/tests/arch/gowin/init-error.ys b/tests/arch/gowin/init-error.ys new file mode 100644 index 000000000..de3813d6f --- /dev/null +++ b/tests/arch/gowin/init-error.ys @@ -0,0 +1,5 @@ +read_verilog init.v +chparam -set INIT 0 myDFF*P* +hierarchy -top myDFFP +logger -expect error "unsupported initial value and async reset value combination" 1 +synth_gowin diff --git a/tests/arch/gowin/init.ys b/tests/arch/gowin/init.ys index ddc0e4757..fba7c2fa5 100644 --- a/tests/arch/gowin/init.ys +++ b/tests/arch/gowin/init.ys @@ -30,45 +30,40 @@ select -assert-count 1 t:DFFRE select -assert-count 1 t:DFFS select -assert-count 1 t:DFFSE -delete design -load read # these should synth to a flop with reset chparam -set INIT 1 myDFF myDFFN myDFFE myDFFNE -# async should give a warning +# async would give an error # sync should synth to a mux -chparam -set INIT 0 myDFF*S* myDFF*P* -chparam -set INIT 1 myDFF*R* myDFF*C* +chparam -set INIT 0 myDFF*S* +chparam -set INIT 1 myDFF*R* proc 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 - -# check the expected leftover init values -# this would happen if your reset value is not the initial value -# which would be weird -select -assert-count 8 a:init +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/gowin/run-test.sh b/tests/arch/gowin/run-test.sh index bf19b887d..4be4b70ae 100755 --- a/tests/arch/gowin/run-test.sh +++ b/tests/arch/gowin/run-test.sh @@ -1,20 +1,4 @@ #!/usr/bin/env bash -set -e -{ -echo "all::" -for x in *.ys; do - echo "all:: run-$x" - echo "run-$x:" - echo " @echo 'Running $x..'" - echo " @../../../yosys -ql ${x%.ys}.log -w 'Yosys has only limited support for tri-state logic at the moment.' $x" -done -for s in *.sh; do - if [ "$s" != "run-test.sh" ]; then - echo "all:: run-$s" - echo "run-$s:" - echo " @echo 'Running $s..'" - echo " @bash $s" - fi -done -} > run-test.mk -exec ${MAKE:-make} -f run-test.mk +set -eu +source ../../gen-tests-makefile.sh +run_tests --yosys-scripts --bash --yosys-args "-w 'Yosys has only limited support for tri-state logic at the moment.'" 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/ice40/run-test.sh b/tests/arch/ice40/run-test.sh index bf19b887d..4be4b70ae 100755 --- a/tests/arch/ice40/run-test.sh +++ b/tests/arch/ice40/run-test.sh @@ -1,20 +1,4 @@ #!/usr/bin/env bash -set -e -{ -echo "all::" -for x in *.ys; do - echo "all:: run-$x" - echo "run-$x:" - echo " @echo 'Running $x..'" - echo " @../../../yosys -ql ${x%.ys}.log -w 'Yosys has only limited support for tri-state logic at the moment.' $x" -done -for s in *.sh; do - if [ "$s" != "run-test.sh" ]; then - echo "all:: run-$s" - echo "run-$s:" - echo " @echo 'Running $s..'" - echo " @bash $s" - fi -done -} > run-test.mk -exec ${MAKE:-make} -f run-test.mk +set -eu +source ../../gen-tests-makefile.sh +run_tests --yosys-scripts --bash --yosys-args "-w 'Yosys has only limited support for tri-state logic at the moment.'" diff --git a/tests/arch/intel_alm/add_sub.ys b/tests/arch/intel_alm/add_sub.ys index 4cb2c2e0d..0f552a27c 100644 --- a/tests/arch/intel_alm/add_sub.ys +++ b/tests/arch/intel_alm/add_sub.ys @@ -6,3 +6,13 @@ cd top # Constrain all select calls below inside the top module stat select -assert-count 8 t:MISTRAL_ALUT_ARITH select -assert-none t:MISTRAL_ALUT_ARITH %% t:* %D + +design -reset +read_verilog ../common/add_sub.v +hierarchy -top top +equiv_opt -assert -map +/intel_alm/common/alm_sim.v synth_intel_alm -family cyclone10gx # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd top # Constrain all select calls below inside the top module +stat +select -assert-count 8 t:MISTRAL_ALUT_ARITH +select -assert-none t:MISTRAL_ALUT_ARITH %% t:* %D diff --git a/tests/arch/intel_alm/adffs.ys b/tests/arch/intel_alm/adffs.ys index 5d8d3a220..4565dcc64 100644 --- a/tests/arch/intel_alm/adffs.ys +++ b/tests/arch/intel_alm/adffs.ys @@ -13,6 +13,18 @@ select -assert-none t:MISTRAL_FF t:MISTRAL_NOT %% t:* %D design -load read +hierarchy -top adff +proc +equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclone10gx # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd adff # 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-none t:MISTRAL_FF t:MISTRAL_NOT %% t:* %D + + +design -load read hierarchy -top adffn proc equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclonev # equivalency check @@ -24,6 +36,17 @@ select -assert-none t:MISTRAL_FF %% t:* %D design -load read +hierarchy -top adffn +proc +equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclone10gx # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd adffn # Constrain all select calls below inside the top module +select -assert-count 1 t:MISTRAL_FF + +select -assert-none t:MISTRAL_FF %% t:* %D + + +design -load read hierarchy -top dffs proc equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclonev # equivalency check @@ -36,13 +59,36 @@ select -assert-none t:MISTRAL_FF t:MISTRAL_ALUT2 %% t:* %D design -load read +hierarchy -top dffs +proc +equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclone10gx # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd dffs # Constrain all select calls below inside the top module +select -assert-count 1 t:MISTRAL_FF +select -assert-count 1 t:MISTRAL_ALUT2 + +select -assert-none t:MISTRAL_FF t:MISTRAL_ALUT2 %% t:* %D + + +design -load read hierarchy -top ndffnr proc equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclonev # equivalency check 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 +hierarchy -top ndffnr +proc +equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclone10gx # equivalency check +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 2 t:MISTRAL_NOT + +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/counter.ys b/tests/arch/intel_alm/counter.ys index 945c318d8..50103fefc 100644 --- a/tests/arch/intel_alm/counter.ys +++ b/tests/arch/intel_alm/counter.ys @@ -9,5 +9,19 @@ cd top # Constrain all select calls below inside the top module select -assert-count 2 t:MISTRAL_NOT select -assert-count 8 t:MISTRAL_ALUT_ARITH select -assert-count 8 t:MISTRAL_FF +select -assert-none t:MISTRAL_NOT t:MISTRAL_ALUT_ARITH t:MISTRAL_FF %% t:* %D + + +design -reset +read_verilog ../common/counter.v +hierarchy -top top +proc +flatten +equiv_opt -async2sync -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclone10gx # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd top # Constrain all select calls below inside the top module +select -assert-count 2 t:MISTRAL_NOT +select -assert-count 8 t:MISTRAL_ALUT_ARITH +select -assert-count 8 t:MISTRAL_FF select -assert-none t:MISTRAL_NOT t:MISTRAL_ALUT_ARITH t:MISTRAL_FF %% t:* %D diff --git a/tests/arch/intel_alm/dffs.ys b/tests/arch/intel_alm/dffs.ys index cf29ad8e0..9ae6c637a 100644 --- a/tests/arch/intel_alm/dffs.ys +++ b/tests/arch/intel_alm/dffs.ys @@ -11,12 +11,33 @@ select -assert-count 1 t:MISTRAL_FF select -assert-none t:MISTRAL_FF %% t:* %D design -load read +hierarchy -top dff +proc +equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclone10gx # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd dff # Constrain all select calls below inside the top module +select -assert-count 1 t:MISTRAL_FF + +select -assert-none t:MISTRAL_FF %% t:* %D + + +design -load read hierarchy -top dffe proc equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclonev # 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:MISTRAL_FF -select -assert-count 1 t:MISTRAL_ALUT3 -select -assert-none t:MISTRAL_FF t:MISTRAL_ALUT3 %% t:* %D +select -assert-none t:MISTRAL_FF %% t:* %D + + +design -load read +hierarchy -top dffe +proc +equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclone10gx # 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:MISTRAL_FF + +select -assert-none t:MISTRAL_FF %% t:* %D diff --git a/tests/arch/intel_alm/fsm.ys b/tests/arch/intel_alm/fsm.ys index 8bb0ebab2..e54b5c21e 100644 --- a/tests/arch/intel_alm/fsm.ys +++ b/tests/arch/intel_alm/fsm.ys @@ -12,7 +12,33 @@ 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 5 t:MISTRAL_ALUT5 -select -assert-count 1 t:MISTRAL_ALUT6 -select -assert-none t:MISTRAL_FF t:MISTRAL_ALUT2 t:MISTRAL_ALUT5 t:MISTRAL_ALUT6 %% t:* %D +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_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 +hierarchy -top fsm +proc +flatten + +equiv_opt -run :prove -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclone10gx +async2sync +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 + +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 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 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_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/logic.ys b/tests/arch/intel_alm/logic.ys index fad45db74..e8b26a524 100644 --- a/tests/arch/intel_alm/logic.ys +++ b/tests/arch/intel_alm/logic.ys @@ -9,3 +9,17 @@ select -assert-count 1 t:MISTRAL_NOT select -assert-count 6 t:MISTRAL_ALUT2 select -assert-count 2 t:MISTRAL_ALUT4 select -assert-none t:MISTRAL_NOT t:MISTRAL_ALUT2 t:MISTRAL_ALUT4 %% t:* %D + + +design -reset +read_verilog ../common/logic.v +hierarchy -top top +proc +equiv_opt -assert -map +/intel_alm/common/alm_sim.v synth_intel_alm -family cyclone10gx # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd top # Constrain all select calls below inside the top module + +select -assert-count 1 t:MISTRAL_NOT +select -assert-count 6 t:MISTRAL_ALUT2 +select -assert-count 2 t:MISTRAL_ALUT4 +select -assert-none t:MISTRAL_NOT t:MISTRAL_ALUT2 t:MISTRAL_ALUT4 %% t:* %D
\ No newline at end of file diff --git a/tests/arch/intel_alm/lutram.ys b/tests/arch/intel_alm/lutram.ys index 6f997b67b..66f8a1536 100644 --- a/tests/arch/intel_alm/lutram.ys +++ b/tests/arch/intel_alm/lutram.ys @@ -7,7 +7,7 @@ memory opt -full miter -equiv -flatten -make_assert -make_outputs gold gate miter -sat -verify -prove-asserts -seq 5 -set-init-zero -show-inputs -show-outputs miter +sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter design -load postopt cd lutram_1w1r @@ -18,3 +18,24 @@ select -assert-count 8 t:MISTRAL_ALUT3 select -assert-count 17 t:MISTRAL_FF select -assert-none t:MISTRAL_NOT t:MISTRAL_ALUT2 t:MISTRAL_ALUT3 t:MISTRAL_FF t:MISTRAL_MLAB %% t:* %D + +design -reset +read_verilog ../common/lutram.v +hierarchy -top lutram_1w1r +proc +memory -nomap +equiv_opt -run :prove -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v -map +/intel_alm/common/mem_sim.v synth_intel_alm -family cyclonev -nobram +memory +opt -full + +miter -equiv -flatten -make_assert -make_outputs gold gate miter +sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter + +design -load postopt +cd lutram_1w1r +select -assert-count 16 t:MISTRAL_MLAB +select -assert-count 1 t:MISTRAL_NOT +select -assert-count 2 t:MISTRAL_ALUT2 +select -assert-count 8 t:MISTRAL_ALUT3 +select -assert-count 17 t:MISTRAL_FF +select -assert-none t:MISTRAL_NOT t:MISTRAL_ALUT2 t:MISTRAL_ALUT3 t:MISTRAL_FF t:MISTRAL_MLAB %% t:* %D diff --git a/tests/arch/intel_alm/mul.ys b/tests/arch/intel_alm/mul.ys new file mode 100644 index 000000000..49934740f --- /dev/null +++ b/tests/arch/intel_alm/mul.ys @@ -0,0 +1,60 @@ +read_verilog ../common/mul.v +chparam -set X_WIDTH 8 -set Y_WIDTH 8 -set A_WIDTH 16 +hierarchy -top top +proc +equiv_opt -assert -map +/intel_alm/common/dsp_sim.v synth_intel_alm -family cyclonev # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd top # Constrain all select calls below inside the top module + +select -assert-count 1 t:MISTRAL_MUL9X9 +select -assert-none t:MISTRAL_MUL9X9 %% t:* %D + +# Cyclone 10 GX does not have 9x9 multipliers. + +design -reset +read_verilog ../common/mul.v +chparam -set X_WIDTH 17 -set Y_WIDTH 17 -set A_WIDTH 34 +hierarchy -top top +proc +equiv_opt -assert -map +/intel_alm/common/dsp_sim.v synth_intel_alm -family cyclonev # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd top # Constrain all select calls below inside the top module + +select -assert-count 1 t:MISTRAL_MUL18X18 +select -assert-none t:MISTRAL_MUL18X18 %% t:* %D + +design -reset +read_verilog ../common/mul.v +chparam -set X_WIDTH 17 -set Y_WIDTH 17 -set A_WIDTH 34 +hierarchy -top top +proc +equiv_opt -assert -map +/intel_alm/common/dsp_sim.v synth_intel_alm -family cyclone10gx # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd top # Constrain all select calls below inside the top module + +select -assert-count 1 t:MISTRAL_MUL18X18 +select -assert-none t:MISTRAL_MUL18X18 %% t:* %D + +design -reset +read_verilog ../common/mul.v +chparam -set X_WIDTH 26 -set Y_WIDTH 26 -set A_WIDTH 52 +hierarchy -top top +proc +equiv_opt -assert -map +/intel_alm/common/dsp_sim.v synth_intel_alm -family cyclonev # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd top # Constrain all select calls below inside the top module + +select -assert-count 1 t:MISTRAL_MUL27X27 +select -assert-none t:MISTRAL_MUL27X27 %% t:* %D + +design -reset +read_verilog ../common/mul.v +chparam -set X_WIDTH 26 -set Y_WIDTH 26 -set A_WIDTH 52 +hierarchy -top top +proc +equiv_opt -assert -map +/intel_alm/common/dsp_sim.v synth_intel_alm -family cyclone10gx # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd top # Constrain all select calls below inside the top module + +select -assert-count 1 t:MISTRAL_MUL27X27 +select -assert-none t:MISTRAL_MUL27X27 %% t:* %D diff --git a/tests/arch/intel_alm/mux.ys b/tests/arch/intel_alm/mux.ys index 308e45268..ac3b9b08f 100644 --- a/tests/arch/intel_alm/mux.ys +++ b/tests/arch/intel_alm/mux.ys @@ -1,15 +1,26 @@ read_verilog ../common/mux.v design -save read + hierarchy -top mux2 proc equiv_opt -assert -map +/intel_alm/common/alm_sim.v synth_intel_alm -family cyclonev # equivalency check design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) cd mux2 # Constrain all select calls below inside the top module select -assert-count 1 t:MISTRAL_ALUT3 +select -assert-none t:MISTRAL_ALUT3 %% t:* %D + +design -load read +hierarchy -top mux2 +proc +equiv_opt -assert -map +/intel_alm/common/alm_sim.v synth_intel_alm -family cyclone10gx # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd mux2 # Constrain all select calls below inside the top module +select -assert-count 1 t:MISTRAL_ALUT3 select -assert-none t:MISTRAL_ALUT3 %% t:* %D + design -load read hierarchy -top mux4 proc @@ -17,9 +28,19 @@ 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 mux4 # Constrain all select calls below inside the top module select -assert-count 1 t:MISTRAL_ALUT6 +select -assert-none t:MISTRAL_ALUT6 %% t:* %D + +design -load read +hierarchy -top mux4 +proc +equiv_opt -assert -map +/intel_alm/common/alm_sim.v synth_intel_alm -family cyclone10gx # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd mux4 # Constrain all select calls below inside the top module +select -assert-count 1 t:MISTRAL_ALUT6 select -assert-none t:MISTRAL_ALUT6 %% t:* %D + design -load read hierarchy -top mux8 proc @@ -27,10 +48,20 @@ 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_ALUT6 %% t:* %D + + +design -load read +hierarchy -top mux8 +proc +equiv_opt -assert -map +/intel_alm/common/alm_sim.v synth_intel_alm -family cyclone10gx # equivalency check +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 2 t:MISTRAL_ALUT6 +select -assert-none t:MISTRAL_ALUT3 t:MISTRAL_ALUT6 %% t:* %D -select -assert-none t:MISTRAL_ALUT3 t:MISTRAL_ALUT5 t:MISTRAL_ALUT6 %% t:* %D design -load read hierarchy -top mux16 @@ -39,6 +70,18 @@ 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-max 2 t:MISTRAL_ALUT5 +select -assert-max 5 t:MISTRAL_ALUT6 +select -assert-none t:MISTRAL_ALUT3 t:MISTRAL_ALUT5 t:MISTRAL_ALUT6 %% t:* %D + + +design -load read +hierarchy -top mux16 +proc +equiv_opt -assert -map +/intel_alm/common/alm_sim.v synth_intel_alm -family cyclone10gx # equivalency check +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 diff --git a/tests/arch/intel_alm/quartus_ice.ys b/tests/arch/intel_alm/quartus_ice.ys index 4b9b54d10..a88226e13 100644 --- a/tests/arch/intel_alm/quartus_ice.ys +++ b/tests/arch/intel_alm/quartus_ice.ys @@ -10,3 +10,17 @@ EOT synth_intel_alm -family cyclonev -quartus select -assert-none w:*[* w:*]* + +design -reset +read_verilog <<EOT +// Verilog has syntax for raw identifiers, where you start it with \ and end it with a space. +// This test crashes Quartus due to it parsing \a[10] as a wire slice and not a raw identifier. +module top(); + (* keep *) wire [31:0] \a[10] ; + (* keep *) wire b; + assign b = \a[10] [31]; +endmodule +EOT + +synth_intel_alm -family cyclone10gx -quartus +select -assert-none w:*[* w:*]* diff --git a/tests/arch/intel_alm/run-test.sh b/tests/arch/intel_alm/run-test.sh index bf19b887d..4be4b70ae 100755 --- a/tests/arch/intel_alm/run-test.sh +++ b/tests/arch/intel_alm/run-test.sh @@ -1,20 +1,4 @@ #!/usr/bin/env bash -set -e -{ -echo "all::" -for x in *.ys; do - echo "all:: run-$x" - echo "run-$x:" - echo " @echo 'Running $x..'" - echo " @../../../yosys -ql ${x%.ys}.log -w 'Yosys has only limited support for tri-state logic at the moment.' $x" -done -for s in *.sh; do - if [ "$s" != "run-test.sh" ]; then - echo "all:: run-$s" - echo "run-$s:" - echo " @echo 'Running $s..'" - echo " @bash $s" - fi -done -} > run-test.mk -exec ${MAKE:-make} -f run-test.mk +set -eu +source ../../gen-tests-makefile.sh +run_tests --yosys-scripts --bash --yosys-args "-w 'Yosys has only limited support for tri-state logic at the moment.'" diff --git a/tests/arch/intel_alm/shifter.ys b/tests/arch/intel_alm/shifter.ys index 014dbd1a8..e307b5486 100644 --- a/tests/arch/intel_alm/shifter.ys +++ b/tests/arch/intel_alm/shifter.ys @@ -6,5 +6,16 @@ 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 top # Constrain all select calls below inside the top module select -assert-count 8 t:MISTRAL_FF +select -assert-none t:MISTRAL_FF %% t:* %D + +design -reset +read_verilog ../common/shifter.v +hierarchy -top top +proc +flatten +equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclone10gx # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd top # Constrain all select calls below inside the top module +select -assert-count 8 t:MISTRAL_FF select -assert-none t:MISTRAL_FF %% t:* %D diff --git a/tests/arch/intel_alm/tribuf.ys b/tests/arch/intel_alm/tribuf.ys index 71b05a747..7f3b38493 100644 --- a/tests/arch/intel_alm/tribuf.ys +++ b/tests/arch/intel_alm/tribuf.ys @@ -9,5 +9,19 @@ design -load postopt # load the post-opt design (otherwise equiv_opt loads the p cd tristate # Constrain all select calls below inside the top module #Internal cell type used. Need support it. select -assert-count 1 t:$_TBUF_ +select -assert-none t:$_TBUF_ %% t:* %D + +design -reset +read_verilog ../common/tribuf.v +hierarchy -top tristate +proc +tribuf +flatten +synth +equiv_opt -assert -map +/simcells.v synth_intel_alm -family cyclone10gx # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd tristate # Constrain all select calls below inside the top module +#Internal cell type used. Need support it. +select -assert-count 1 t:$_TBUF_ select -assert-none t:$_TBUF_ %% t:* %D diff --git a/tests/arch/nexus/.gitignore b/tests/arch/nexus/.gitignore new file mode 100644 index 000000000..ba42e1ee6 --- /dev/null +++ b/tests/arch/nexus/.gitignore @@ -0,0 +1,2 @@ +/*.log +/run-test.mk diff --git a/tests/arch/nexus/add_sub.ys b/tests/arch/nexus/add_sub.ys new file mode 100644 index 000000000..4317bab81 --- /dev/null +++ b/tests/arch/nexus/add_sub.ys @@ -0,0 +1,21 @@ +read_verilog ../common/add_sub.v +hierarchy -top top +proc +design -save orig + +equiv_opt -assert -map +/nexus/cells_sim.v synth_nexus # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd top # Constrain all select calls below inside the top module +stat +select -assert-count 10 t:LUT4 +select -assert-none t:IB t:OB t:VLO t:LUT4 %% t:* %D + +design -load orig + +equiv_opt -assert -map +/nexus/cells_sim.v synth_nexus -abc9 # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd top # Constrain all select calls below inside the top module +stat +select -assert-count 6 t:LUT4 +select -assert-count 4 t:WIDEFN9 +select -assert-none t:IB t:OB t:VLO t:LUT4 t:WIDEFN9 %% t:* %D diff --git a/tests/arch/nexus/adffs.ys b/tests/arch/nexus/adffs.ys new file mode 100644 index 000000000..f8796425c --- /dev/null +++ b/tests/arch/nexus/adffs.ys @@ -0,0 +1,44 @@ +read_verilog ../common/adffs.v +design -save read + +hierarchy -top adff +proc +equiv_opt -async2sync -assert -map +/nexus/cells_sim.v synth_nexus # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd adff # Constrain all select calls below inside the top module +stat +select -assert-count 1 t:FD1P3DX +select -assert-none t:FD1P3DX t:IB t:OB t:VLO t:VHI %% t:* %D + +design -load read +hierarchy -top adffn +proc +equiv_opt -async2sync -assert -map +/nexus/cells_sim.v synth_nexus # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd adffn # Constrain all select calls below inside the top module +stat +select -assert-count 1 t:FD1P3DX +select -assert-count 1 t:INV +select -assert-none t:FD1P3DX t:INV t:LUT4 t:IB t:OB t:VLO t:VHI %% t:* %D + +design -load read +hierarchy -top dffs +proc +equiv_opt -async2sync -assert -map +/nexus/cells_sim.v synth_nexus # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd dffs # Constrain all select calls below inside the top module +stat +select -assert-count 1 t:FD1P3IX +select -assert-count 1 t:LUT4 +select -assert-none t:FD1P3IX t:LUT4 t:IB t:OB t:VLO t:VHI %% t:* %D + +design -load read +hierarchy -top ndffnr +proc +equiv_opt -async2sync -assert -map +/nexus/cells_sim.v synth_nexus # equivalency check +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 +stat +select -assert-count 1 t:FD1P3IX +select -assert-count 2 t:INV +select -assert-none t:FD1P3IX t:INV t:LUT4 t:IB t:OB t:VLO t:VHI %% t:* %D diff --git a/tests/arch/nexus/blockram.ys b/tests/arch/nexus/blockram.ys new file mode 100644 index 000000000..9540136d5 --- /dev/null +++ b/tests/arch/nexus/blockram.ys @@ -0,0 +1,18 @@ +read_verilog ../common/blockram.v +design -save read + +# Check that we use the right dual and single clock variants + +chparam -set ADDRESS_WIDTH 10 -set DATA_WIDTH 18 sync_ram_sdp +synth_nexus -top sync_ram_sdp +cd sync_ram_sdp +select -assert-count 1 t:PDPSC16K +select -assert-none t:PDPSC16K t:INV t:IB t:OB t:VLO t:VHI %% t:* %D + +design -reset +read_verilog blockram_dc.v +chparam -set ADDRESS_WIDTH 10 -set DATA_WIDTH 18 sync_ram_sdp_dc +synth_nexus -top sync_ram_sdp_dc +cd sync_ram_sdp_dc +select -assert-count 1 t:PDP16K +select -assert-none t:PDP16K t:INV t:IB t:OB t:VLO t:VHI %% t:* %D diff --git a/tests/arch/nexus/blockram_dc.v b/tests/arch/nexus/blockram_dc.v new file mode 100644 index 000000000..4f5d4f5a6 --- /dev/null +++ b/tests/arch/nexus/blockram_dc.v @@ -0,0 +1,25 @@ + +`default_nettype none +module sync_ram_sdp_dc #(parameter DATA_WIDTH=8, ADDRESS_WIDTH=10) + (input wire clkw, clkr, write_enable, + input wire [DATA_WIDTH-1:0] data_in, + input wire [ADDRESS_WIDTH-1:0] address_in_r, address_in_w, + output wire [DATA_WIDTH-1:0] data_out); + + localparam WORD = (DATA_WIDTH-1); + localparam DEPTH = (2**ADDRESS_WIDTH-1); + + reg [WORD:0] data_out_r; + reg [WORD:0] memory [0:DEPTH]; + + always @(posedge clkw) begin + if (write_enable) + memory[address_in_w] <= data_in; + end + always @(posedge clkr) begin + data_out_r <= memory[address_in_r]; + end + + assign data_out = data_out_r; + +endmodule // sync_ram_sdp_dc diff --git a/tests/arch/nexus/counter.ys b/tests/arch/nexus/counter.ys new file mode 100644 index 000000000..44421e377 --- /dev/null +++ b/tests/arch/nexus/counter.ys @@ -0,0 +1,11 @@ +read_verilog ../common/counter.v +hierarchy -top top +proc +flatten +equiv_opt -assert -multiclock -map +/nexus/cells_sim.v synth_nexus # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd top # Constrain all select calls below inside the top module +stat +select -assert-count 5 t:CCU2 +select -assert-count 8 t:FD1P3DX +select -assert-none t:CCU2 t:FD1P3DX t:IB t:OB t:VLO t:VHI %% t:* %D diff --git a/tests/arch/nexus/dffs.ys b/tests/arch/nexus/dffs.ys new file mode 100644 index 000000000..9ebf68bf4 --- /dev/null +++ b/tests/arch/nexus/dffs.ys @@ -0,0 +1,19 @@ +read_verilog ../common/dffs.v +design -save read + +hierarchy -top dff +proc +equiv_opt -assert -map +/nexus/cells_sim.v synth_nexus # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd dff # Constrain all select calls below inside the top module +select -assert-count 1 t:FD1P3IX +select -assert-none t:FD1P3IX t:IB t:OB t:VHI t:VLO %% t:* %D + +design -load read +hierarchy -top dffe +proc +equiv_opt -assert -map +/nexus/cells_sim.v synth_nexus # 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:FD1P3IX +select -assert-none t:FD1P3IX t:IB t:OB t:VHI t:VLO %% t:* %D diff --git a/tests/arch/nexus/fsm.ys b/tests/arch/nexus/fsm.ys new file mode 100644 index 000000000..24ad8fe5b --- /dev/null +++ b/tests/arch/nexus/fsm.ys @@ -0,0 +1,19 @@ +read_verilog ../common/fsm.v +hierarchy -top fsm +proc +flatten + +equiv_opt -run :prove -map +/nexus/cells_sim.v synth_nexus +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 + +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 + +stat + +select -assert-max 1 t:INV +select -assert-max 2 t:LUT4 +select -assert-max 6 t:WIDEFN9 +select -assert-count 6 t:FD1P3IX +select -assert-none t:LUT4 t:FD1P3IX t:WIDEFN9 t:INV t:IB t:OB t:VLO t:VHI %% t:* %D diff --git a/tests/arch/nexus/logic.ys b/tests/arch/nexus/logic.ys new file mode 100644 index 000000000..cff61b509 --- /dev/null +++ b/tests/arch/nexus/logic.ys @@ -0,0 +1,8 @@ +read_verilog ../common/logic.v +hierarchy -top top +proc +equiv_opt -assert -map +/nexus/cells_sim.v synth_nexus # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd top # Constrain all select calls below inside the top module +select -assert-count 8 t:LUT4 +select -assert-none t:LUT4 t:INV t:IB t:OB t:VLO t:VHI %% t:* %D diff --git a/tests/arch/nexus/lutram.ys b/tests/arch/nexus/lutram.ys new file mode 100644 index 000000000..cd645f717 --- /dev/null +++ b/tests/arch/nexus/lutram.ys @@ -0,0 +1,19 @@ +read_verilog ../common/lutram.v +hierarchy -top lutram_1w1r +proc +memory -nomap +equiv_opt -run :prove -map +/nexus/cells_sim.v synth_nexus +memory +opt -full + +miter -equiv -flatten -make_assert -make_outputs gold gate miter +sat -verify -prove-asserts -seq 5 -set-init-zero -show-inputs -show-outputs miter + +design -load postopt +cd lutram_1w1r +stat +select -assert-count 8 t:WIDEFN9 +select -assert-count 16 t:LUT4 +select -assert-count 8 t:DPR16X4 +select -assert-count 36 t:FD1P3IX +select -assert-none t:DPR16X4 t:FD1P3IX t:WIDEFN9 t:LUT4 t:INV t:IB t:OB t:VLO t:VHI %% t:* %D diff --git a/tests/arch/nexus/mul.ys b/tests/arch/nexus/mul.ys new file mode 100644 index 000000000..65a2fd8c3 --- /dev/null +++ b/tests/arch/nexus/mul.ys @@ -0,0 +1,50 @@ +read_verilog ../common/mul.v +chparam -set X_WIDTH 8 -set Y_WIDTH 8 -set A_WIDTH 16 +hierarchy -top top +proc + +design -save read + +equiv_opt -assert -map +/nexus/cells_sim.v synth_nexus +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd top # Constrain all select calls below inside the top module +select -assert-count 1 t:MULT9X9 + +select -assert-none t:IB t:OB t:VLO t:VHI t:MULT9X9 %% t:* %D + + +design -reset +read_verilog ../common/mul.v +chparam -set X_WIDTH 16 -set Y_WIDTH 16 -set A_WIDTH 32 +hierarchy -top top +proc +# equivalence checking is too slow here +synth_nexus +cd top # Constrain all select calls below inside the top module +select -assert-count 1 t:MULT18X18 +select -assert-none t:IB t:OB t:VLO t:VHI t:MULT18X18 %% t:* %D + + +design -reset +read_verilog ../common/mul.v +chparam -set X_WIDTH 32 -set Y_WIDTH 16 -set A_WIDTH 48 +hierarchy -top top +proc +# equivalence checking is too slow here +synth_nexus +cd top # Constrain all select calls below inside the top module +select -assert-count 1 t:MULT18X36 +select -assert-none t:IB t:OB t:VLO t:VHI t:MULT18X36 %% t:* %D + + +design -reset +read_verilog ../common/mul.v +chparam -set X_WIDTH 32 -set Y_WIDTH 32 -set A_WIDTH 64 +hierarchy -top top +proc +# equivalence checking is too slow here +synth_nexus +cd top # Constrain all select calls below inside the top module +select -assert-count 1 t:MULT36X36 + +select -assert-none t:IB t:OB t:VLO t:VHI t:MULT36X36 %% t:* %D diff --git a/tests/arch/nexus/mux.ys b/tests/arch/nexus/mux.ys new file mode 100644 index 000000000..0e12d674a --- /dev/null +++ b/tests/arch/nexus/mux.ys @@ -0,0 +1,43 @@ +read_verilog ../common/mux.v +design -save read + +hierarchy -top mux2 +proc +equiv_opt -assert -map +/nexus/cells_sim.v synth_nexus # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd mux2 # Constrain all select calls below inside the top module +select -assert-count 1 t:LUT4 +select -assert-none t:IB t:OB t:VLO t:VHI t:LUT4 t:WIDEFN9 %% t:* %D + +design -load read +hierarchy -top mux4 +proc +equiv_opt -assert -map +/nexus/cells_sim.v synth_nexus # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd mux4 # Constrain all select calls below inside the top module +select -assert-count 1 t:WIDEFN9 + +select -assert-none t:IB t:OB t:VLO t:VHI t:LUT4 t:WIDEFN9 %% t:* %D + +design -load read +hierarchy -top mux8 +proc +equiv_opt -assert -map +/nexus/cells_sim.v synth_nexus # equivalency check +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 4 t:LUT4 +select -assert-count 1 t:WIDEFN9 + +select -assert-none t:IB t:OB t:VLO t:VHI t:LUT4 t:WIDEFN9 %% t:* %D + +design -load read +hierarchy -top mux16 +proc +equiv_opt -assert -map +/nexus/cells_sim.v synth_nexus # equivalency check +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-min 11 t:LUT4 +select -assert-max 12 t:LUT4 +select -assert-count 1 t:WIDEFN9 + +select -assert-none t:IB t:OB t:VLO t:VHI t:LUT4 t:WIDEFN9 %% t:* %D diff --git a/tests/arch/nexus/run-test.sh b/tests/arch/nexus/run-test.sh new file mode 100644 index 000000000..4be4b70ae --- /dev/null +++ b/tests/arch/nexus/run-test.sh @@ -0,0 +1,4 @@ +#!/usr/bin/env bash +set -eu +source ../../gen-tests-makefile.sh +run_tests --yosys-scripts --bash --yosys-args "-w 'Yosys has only limited support for tri-state logic at the moment.'" diff --git a/tests/arch/nexus/shifter.ys b/tests/arch/nexus/shifter.ys new file mode 100644 index 000000000..a8e34b0f9 --- /dev/null +++ b/tests/arch/nexus/shifter.ys @@ -0,0 +1,9 @@ +read_verilog ../common/shifter.v +hierarchy -top top +proc +flatten +equiv_opt -assert -map +/nexus/cells_sim.v synth_nexus # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd top # Constrain all select calls below inside the top module +select -assert-count 8 t:FD1P3IX +select -assert-none t:FD1P3IX t:WIDEFN9 t:INV t:IB t:OB t:VLO t:VHI %% t:* %D diff --git a/tests/arch/nexus/tribuf.ys b/tests/arch/nexus/tribuf.ys new file mode 100644 index 000000000..70fb7cb5f --- /dev/null +++ b/tests/arch/nexus/tribuf.ys @@ -0,0 +1,12 @@ +read_verilog ../common/tribuf.v +hierarchy -top tristate +proc +tribuf +flatten +synth +equiv_opt -assert -map +/nexus/cells_sim.v -map +/simcells.v synth_nexus # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd tristate # Constrain all select calls below inside the top module +select -assert-count 1 t:OBZ +select -assert-count 1 t:INV +select -assert-none t:OBZ t:INV t:IB t:OB t:VLO t:VHI %% t:* %D diff --git a/tests/arch/xilinx/attributes_test.ys b/tests/arch/xilinx/attributes_test.ys index 7bdd94a63..58552d8fb 100644 --- a/tests/arch/xilinx/attributes_test.ys +++ b/tests/arch/xilinx/attributes_test.ys @@ -16,8 +16,7 @@ select -assert-count 8 t:RAM32X1D # Set ram_style distributed to blockram memory; will be implemented as distributed design -reset read_verilog ../common/memory_attributes/attributes_test.v -prep -setattr -mod -set ram_style "distributed" block_ram +setattr -set ram_style "distributed" block_ram/m:* synth_xilinx -top block_ram -noiopad cd block_ram # Constrain all select calls below inside the top module select -assert-count 32 t:RAM128X1D @@ -25,8 +24,7 @@ select -assert-count 32 t:RAM128X1D # Set synthesis, logic_block to blockram memory; will be implemented as distributed design -reset read_verilog ../common/memory_attributes/attributes_test.v -prep -setattr -mod -set logic_block 1 block_ram +setattr -set logic_block 1 block_ram/m:* synth_xilinx -top block_ram -noiopad cd block_ram # Constrain all select calls below inside the top module select -assert-count 0 t:RAMB18E1 diff --git a/tests/arch/xilinx/dsp_abc9.ys b/tests/arch/xilinx/dsp_abc9.ys new file mode 100644 index 000000000..909e54149 --- /dev/null +++ b/tests/arch/xilinx/dsp_abc9.ys @@ -0,0 +1,37 @@ +read_verilog <<EOT +module top(input [24:0] A, input [17:0] B, output [47:0] P); +DSP48E1 #(.PREG(0)) dsp(.A(A), .B(B), .P(P)); +endmodule +EOT +techmap -autoproc -wb -map +/xilinx/cells_sim.v +opt +scc -expect 0 + + +design -reset +read_verilog <<EOT +module top(input signed [24:0] A, input signed [17:0] B, output [47:0] P); +assign P = A * B; +endmodule +EOT +synth_xilinx -abc9 +techmap -autoproc -wb -map +/xilinx/cells_sim.v +opt -full -fine +select -assert-count 1 t:$mul +select -assert-count 0 t:* t:$mul %D + + +design -reset +read_verilog -icells -formal <<EOT +module top(output [42:0] P); +\$__MUL25X18 mul (.A(42), .B(42), .Y(P)); +assert property (P == 42*42); +endmodule +EOT +techmap -map +/xilinx/xc7_dsp_map.v +verilog_defaults -add -D ALLOW_WHITEBOX_DSP48E1 +synth_xilinx -abc9 +techmap -autoproc -wb -map +/xilinx/cells_sim.v +opt -full -fine +select -assert-count 0 t:* t:$assert %d +sat -verify -prove-asserts 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/nosrl.ys b/tests/arch/xilinx/nosrl.ys new file mode 100644 index 000000000..31bd5d377 --- /dev/null +++ b/tests/arch/xilinx/nosrl.ys @@ -0,0 +1,41 @@ +read_verilog <<EOT + +module xilinx_srl_static_test(input i, clk, output [1:0] q); +reg head = 1'b0; +reg [3:0] shift1 = 4'b0000; +reg [3:0] shift2 = 4'b0000; + +always @(posedge clk) begin + head <= i; + shift1 <= {shift1[2:0], head}; + shift2 <= {shift2[2:0], head}; +end + +assign q = {shift2[3], shift1[3]}; +endmodule + +EOT + +design -save read + +hierarchy -top xilinx_srl_static_test +proc +#equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check +equiv_opt -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd xilinx_srl_static_test # Constrain all select calls below inside the top module +stat +select -assert-count 1 t:BUFG +select -assert-count 1 t:SRL16E +select -assert-none t:BUFG t:SRL16E %% t:* %D + +design -load read +hierarchy -top xilinx_srl_static_test +proc +equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -nosrl -noiopad # equivalency check +design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +cd xilinx_srl_static_test # Constrain all select calls below inside the top module +stat +select -assert-count 1 t:BUFG +select -assert-count 5 t:FDRE +select -assert-none t:BUFG t:FDRE %% t:* %D 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 diff --git a/tests/arch/xilinx/run-test.sh b/tests/arch/xilinx/run-test.sh index bf19b887d..4be4b70ae 100755 --- a/tests/arch/xilinx/run-test.sh +++ b/tests/arch/xilinx/run-test.sh @@ -1,20 +1,4 @@ #!/usr/bin/env bash -set -e -{ -echo "all::" -for x in *.ys; do - echo "all:: run-$x" - echo "run-$x:" - echo " @echo 'Running $x..'" - echo " @../../../yosys -ql ${x%.ys}.log -w 'Yosys has only limited support for tri-state logic at the moment.' $x" -done -for s in *.sh; do - if [ "$s" != "run-test.sh" ]; then - echo "all:: run-$s" - echo "run-$s:" - echo " @echo 'Running $s..'" - echo " @bash $s" - fi -done -} > run-test.mk -exec ${MAKE:-make} -f run-test.mk +set -eu +source ../../gen-tests-makefile.sh +run_tests --yosys-scripts --bash --yosys-args "-w 'Yosys has only limited support for tri-state logic at the moment.'" |