diff options
Diffstat (limited to 'tests')
28 files changed, 273 insertions, 231 deletions
diff --git a/tests/aiger/run-test.sh b/tests/aiger/run-test.sh index de7bc68cf..bcf2b964a 100755 --- a/tests/aiger/run-test.sh +++ b/tests/aiger/run-test.sh @@ -55,5 +55,5 @@ done for y in *.ys; do echo "Running $y." - ../../yosys $y -ql ${y%.*}.log + ../../yosys -ql ${y%.*}.log $y done 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/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/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/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/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/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/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/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.'" diff --git a/tests/gen-tests-makefile.sh b/tests/gen-tests-makefile.sh new file mode 100755 index 000000000..ab8fb7013 --- /dev/null +++ b/tests/gen-tests-makefile.sh @@ -0,0 +1,94 @@ +set -eu + +YOSYS_BASEDIR="$(cd "$(dirname "${BASH_SOURCE[0]}")"/../ >/dev/null 2>&1 && pwd)" + +# $ generate_target target_name test_command +generate_target() { + target_name=$1 + test_command=$2 + echo "all: $target_name" + echo ".PHONY: $target_name" + echo "$target_name:" + printf "\t@%s\n" "$test_command" + printf "\t@echo 'Passed %s'\n" "$target_name" +} + +# $ generate_ys_test ys_file [yosys_args] +generate_ys_test() { + ys_file=$1 + yosys_args=${2:-} + generate_target "$ys_file" "$YOSYS_BASEDIR/yosys -ql ${ys_file%.*}.log $yosys_args $ys_file" +} + +# $ generate_bash_test bash_file +generate_bash_test() { + bash_file=$1 + generate_target "$bash_file" "bash -v $bash_file >${bash_file%.*}.log 2>&1" +} + +# $ generate_tests [-y|--yosys-scripts] [-s|--prove-sv] [-b|--bash] [-a|--yosys-args yosys_args] +generate_tests() { + do_ys=false + do_sv=false + do_sh=false + yosys_args="" + + while [[ $# -gt 0 ]]; do + arg="$1" + case "$arg" in + -y|--yosys-scripts) + do_ys=true + shift + ;; + -s|--prove-sv) + do_sv=true + shift + ;; + -b|--bash) + do_sh=true + shift + ;; + -a|--yosys-args) + yosys_args+="$2" + shift + shift + ;; + *) + echo >&2 "Unknown argument: $1" + exit 1 + esac + done + + if [[ ! ( $do_ys = true || $do_sv = true || $do_sh = true ) ]]; then + echo >&2 "Error: No file types selected" + exit 1 + fi + + echo ".PHONY: all" + echo "all:" + + if [[ $do_ys = true ]]; then + for x in *.ys; do + generate_ys_test "$x" "$yosys_args" + done + fi; + if [[ $do_sv = true ]]; then + for x in *.sv; do + if [ ! -f "${x%.sv}.ys" ]; then + generate_ys_test "$x" "-p \"prep -top top; sat -verify -prove-asserts\" $yosys_args" + fi; + done + fi; + if [[ $do_sh == true ]]; then + for s in *.sh; do + if [ "$s" != "run-test.sh" ]; then + generate_bash_test "$s" + fi + done + fi +} + +run_tests() { + generate_tests "$@" > run-test.mk + exec ${MAKE:-make} -f run-test.mk +} diff --git a/tests/memories/run-test.sh b/tests/memories/run-test.sh index 8d1a8b413..376f5bf79 100755 --- a/tests/memories/run-test.sh +++ b/tests/memories/run-test.sh @@ -9,12 +9,12 @@ while getopts "A:S:" opt do case "$opt" in A) abcopt="-A $OPTARG" ;; - S) seed="-S $OPTARG" ;; + S) seed="$OPTARG" ;; esac done shift "$((OPTIND-1))" -bash ../tools/autotest.sh $abcopt $seed -G *.v +${MAKE:-make} -f ../tools/autotest.mk SEED="$seed" EXTRA_FLAGS="$abcopt" *.v for f in `egrep -l 'expect-(wr-ports|rd-ports|rd-clk)' *.v`; do echo -n "Testing expectations for $f .." diff --git a/tests/opt/.gitignore b/tests/opt/.gitignore index 397b4a762..8355de9dc 100644 --- a/tests/opt/.gitignore +++ b/tests/opt/.gitignore @@ -1 +1,2 @@ *.log +run-test.mk diff --git a/tests/opt/run-test.sh b/tests/opt/run-test.sh index 44ce7e674..2007cd6e4 100755 --- a/tests/opt/run-test.sh +++ b/tests/opt/run-test.sh @@ -1,6 +1,4 @@ #!/bin/bash -set -e -for x in *.ys; do - echo "Running $x.." - ../../yosys -ql ${x%.ys}.log $x -done +set -eu +source ../gen-tests-makefile.sh +run_tests --yosys-scripts diff --git a/tests/opt_share/run-test.sh b/tests/opt_share/run-test.sh index e01552646..e0008a259 100755 --- a/tests/opt_share/run-test.sh +++ b/tests/opt_share/run-test.sh @@ -22,12 +22,23 @@ mkdir -p temp echo "generating tests.." python3 generate.py -c $count $seed +{ + echo ".PHONY: all" + echo "all:" + + for i in $( ls temp/*.ys | sed 's,[^0-9],,g; s,^0*\(.\),\1,g;' ); do + idx=$( printf "%05d" $i ) + echo ".PHONY: test-$idx" + echo "all: test-$idx" + echo "test-$idx:" + printf "\t@%s\n" \ + "echo -n [$i]" \ + "../../yosys -ql temp/uut_${idx}.log temp/uut_${idx}.ys" + done +} > temp/makefile + echo "running tests.." -for i in $( ls temp/*.ys | sed 's,[^0-9],,g; s,^0*\(.\),\1,g;' ); do - echo -n "[$i]" - idx=$( printf "%05d" $i ) - ../../yosys -ql temp/uut_${idx}.log temp/uut_${idx}.ys -done +${MAKE:-make} -f temp/makefile echo failed_share=$( echo $( gawk '/^#job#/ { j=$2; db[j]=0; } /^Removing [246] cells/ { delete db[j]; } END { for (j in db) print(j); }' temp/all_share_log.txt ) ) diff --git a/tests/sat/.gitignore b/tests/sat/.gitignore index 397b4a762..8355de9dc 100644 --- a/tests/sat/.gitignore +++ b/tests/sat/.gitignore @@ -1 +1,2 @@ *.log +run-test.mk diff --git a/tests/sat/run-test.sh b/tests/sat/run-test.sh index 67e1beb23..74589dfeb 100755 --- a/tests/sat/run-test.sh +++ b/tests/sat/run-test.sh @@ -1,6 +1,4 @@ -#!/bin/bash -set -e -for x in *.ys; do - echo "Running $x.." - ../../yosys -ql ${x%.ys}.log $x -done +#!/usr/bin/env bash +set -eu +source ../gen-tests-makefile.sh +run_tests --yosys-scripts diff --git a/tests/simple/run-test.sh b/tests/simple/run-test.sh index f20fd0d30..47bcfd6da 100755 --- a/tests/simple/run-test.sh +++ b/tests/simple/run-test.sh @@ -17,5 +17,4 @@ if ! command -v iverilog > /dev/null ; then exit 1 fi -shopt -s nullglob exec ${MAKE:-make} -f ../tools/autotest.mk $seed *.{sv,v} diff --git a/tests/svtypes/multirange_array.sv b/tests/svtypes/multirange_array.sv new file mode 100644 index 000000000..be0d3dfc2 --- /dev/null +++ b/tests/svtypes/multirange_array.sv @@ -0,0 +1,16 @@ +// test for multirange arrays + +`define STRINGIFY(x) `"x`" +`define STATIC_ASSERT(x) if(!(x)) $error({"assert failed: ", `STRINGIFY(x)}) + +module top; + + logic a [3]; + logic b [3][5]; + logic c [3][5][7]; + + `STATIC_ASSERT($bits(a) == 3); + `STATIC_ASSERT($bits(b) == 15); + `STATIC_ASSERT($bits(c) == 105); + +endmodule diff --git a/tests/svtypes/multirange_subarray_access.ys b/tests/svtypes/multirange_subarray_access.ys new file mode 100644 index 000000000..de57d1423 --- /dev/null +++ b/tests/svtypes/multirange_subarray_access.ys @@ -0,0 +1,12 @@ +logger -expect error "Insufficient number of array indices for a." 1 +read_verilog -sv <<EOT +module foo; +logic a [6:0][4:0][1:0]; +logic b [1:0]; + +assign a[0][0][0] = 1'b0; +assign a[0][0][1] = 1'b1; +assign b = a[0][0]; + +endmodule +EOT diff --git a/tests/svtypes/run-test.sh b/tests/svtypes/run-test.sh index 09a30eed1..91ceae227 100755 --- a/tests/svtypes/run-test.sh +++ b/tests/svtypes/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 $x" -done -for x in *.sv; do - if [ ! -f "${x%.sv}.ys" ]; then - echo "all:: check-$x" - echo "check-$x:" - echo " @echo 'Checking $x..'" - echo " @../../yosys -ql ${x%.sv}.log -p \"prep -top top; sat -verify -prove-asserts\" $x" - fi -done -} > run-test.mk -exec ${MAKE:-make} -f run-test.mk +set -eu +source ../gen-tests-makefile.sh +run_tests --yosys-scripts --prove-sv diff --git a/tests/techmap/mem_simple_4x1_runtest.sh b/tests/techmap/mem_simple_4x1_runtest.sh index e2c6303da..9c41fa56a 100644 --- a/tests/techmap/mem_simple_4x1_runtest.sh +++ b/tests/techmap/mem_simple_4x1_runtest.sh @@ -1,6 +1,6 @@ #!/bin/bash -set -ev +set -e ../../yosys -b 'verilog -noattr' -o mem_simple_4x1_synth.v -p 'proc; opt; memory -nomap; techmap -map mem_simple_4x1_map.v;; techmap; opt; abc;; stat' mem_simple_4x1_uut.v diff --git a/tests/techmap/recursive_runtest.sh b/tests/techmap/recursive_runtest.sh index 30c79bf03..0725ccf40 100644 --- a/tests/techmap/recursive_runtest.sh +++ b/tests/techmap/recursive_runtest.sh @@ -1,3 +1,3 @@ -set -ev +set -e ../../yosys -p 'hierarchy -top top; techmap -map recursive_map.v -max_iter 1; select -assert-count 2 t:sub; select -assert-count 2 t:bar' recursive.v diff --git a/tests/techmap/run-test.sh b/tests/techmap/run-test.sh index c16f204d9..581847ab0 100755 --- a/tests/techmap/run-test.sh +++ b/tests/techmap/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 -e 'select out of bounds' $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 > ${s%.sh}.log 2>&1" - 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 "-e 'select out of bounds'" diff --git a/tests/various/run-test.sh b/tests/various/run-test.sh index ea56b70f0..2f91cf0fd 100755 --- a/tests/various/run-test.sh +++ b/tests/various/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 $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 diff --git a/tests/verilog/.gitignore b/tests/verilog/.gitignore index b48f808a1..34da23437 100644 --- a/tests/verilog/.gitignore +++ b/tests/verilog/.gitignore @@ -1,3 +1,5 @@ /*.log /*.out /run-test.mk +/const_arst.v +/const_sr.v diff --git a/tests/verilog/const_arst.ys b/tests/verilog/const_arst.ys new file mode 100644 index 000000000..df720575c --- /dev/null +++ b/tests/verilog/const_arst.ys @@ -0,0 +1,24 @@ +read_verilog <<EOT +module test ( + input clk, d, + output reg q +); +wire nop = 1'h0; +always @(posedge clk, posedge nop) begin + if (nop) q <= 1'b0; + else q <= d; +end +endmodule +EOT +prep -top test +write_verilog const_arst.v +design -stash gold +read_verilog const_arst.v +prep -top test +design -stash gate +design -copy-from gold -as gold A:top +design -copy-from gate -as gate A:top +miter -equiv -flatten -make_assert gold gate miter +prep -top miter +clk2fflogic +sat -set-init-zero -tempinduct -prove-asserts -verify diff --git a/tests/verilog/const_sr.ys b/tests/verilog/const_sr.ys new file mode 100644 index 000000000..c1406b0a0 --- /dev/null +++ b/tests/verilog/const_sr.ys @@ -0,0 +1,25 @@ +read_verilog <<EOT +module test ( + input clk, rst, d, + output reg q +); +wire nop = 1'h0; +always @(posedge clk, posedge nop, posedge rst) begin + if (rst) q <= 1'b0; + else if (nop) q <= 1'b1; + else q <= d; +end +endmodule +EOT +prep -top test +write_verilog const_sr.v +design -stash gold +read_verilog const_sr.v +prep -top test +design -stash gate +design -copy-from gold -as gold A:top +design -copy-from gate -as gate A:top +miter -equiv -flatten -make_assert gold gate miter +prep -top miter +clk2fflogic +sat -set-init-zero -tempinduct -prove-asserts -verify diff --git a/tests/verilog/run-test.sh b/tests/verilog/run-test.sh index ea56b70f0..2f91cf0fd 100755 --- a/tests/verilog/run-test.sh +++ b/tests/verilog/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 $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 |