diff --git a/Makefile b/Makefile index f467330c8..c3d3f57ea 100644 --- a/Makefile +++ b/Makefile @@ -881,6 +881,7 @@ endif +cd tests/arch/intel_alm && bash run-test.sh $(SEEDOPT) +cd tests/arch/nexus && bash run-test.sh $(SEEDOPT) +cd tests/arch/quicklogic/pp3 && bash run-test.sh $(SEEDOPT) + +cd tests/arch/quicklogic/qlf_k6n10f && bash run-test.sh $(SEEDOPT) +cd tests/arch/gatemate && bash run-test.sh $(SEEDOPT) +cd tests/rpc && bash run-test.sh +cd tests/memfile && bash run-test.sh diff --git a/tests/arch/quicklogic/qlf_k6n10f/add_sub.ys b/tests/arch/quicklogic/qlf_k6n10f/add_sub.ys new file mode 100644 index 000000000..30d9bbc9d --- /dev/null +++ b/tests/arch/quicklogic/qlf_k6n10f/add_sub.ys @@ -0,0 +1,8 @@ +read_verilog ../../common/add_sub.v +hierarchy -top top +equiv_opt -assert -map +/quicklogic/qlf_k6n10f/cells_sim.v synth_quicklogic -family qlf_k6n10f # 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 9 t:$lut # OOT flow has 8 +select -assert-count 8 t:adder_carry +select -assert-none t:$lut t:adder_carry %% t:* %D diff --git a/tests/arch/quicklogic/qlf_k6n10f/adffs.ys b/tests/arch/quicklogic/qlf_k6n10f/adffs.ys new file mode 100644 index 000000000..475355d2b --- /dev/null +++ b/tests/arch/quicklogic/qlf_k6n10f/adffs.ys @@ -0,0 +1,48 @@ +read_verilog ../../common/adffs.v +design -save read + +hierarchy -top adff +proc +equiv_opt -async2sync -assert -map +/quicklogic/qlf_k6n10f/cells_sim.v -map +/quicklogic/common/cells_sim.v synth_quicklogic -family qlf_k6n10f # 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:$lut r:WIDTH=1 %i +select -assert-none r:WIDTH>1 +select -assert-count 1 t:dffsre + +select -assert-none t:$lut t:dffsre %% t:* %D + + +design -load read +hierarchy -top adffn +proc +equiv_opt -async2sync -assert -map +/quicklogic/qlf_k6n10f/cells_sim.v -map +/quicklogic/common/cells_sim.v synth_quicklogic -family qlf_k6n10f # 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:dffsre + +select -assert-none t:dffsre %% t:* %D + + +design -load read +hierarchy -top dffs +proc +equiv_opt -async2sync -assert -map +/quicklogic/qlf_k6n10f/cells_sim.v -map +/quicklogic/common/cells_sim.v synth_quicklogic -family qlf_k6n10f # 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:$lut r:WIDTH=1 %i +select -assert-none r:WIDTH>1 +select -assert-count 1 t:sdffsre + +select -assert-none t:$lut t:sdffsre %% t:* %D + + +design -load read +hierarchy -top ndffnr +proc +equiv_opt -async2sync -assert -map +/quicklogic/qlf_k6n10f/cells_sim.v -map +/quicklogic/common/cells_sim.v synth_quicklogic -family qlf_k6n10f # 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:sdffnsre + +select -assert-none t:sdffnsre %% t:* %D diff --git a/tests/arch/quicklogic/qlf_k6n10f/counter.ys b/tests/arch/quicklogic/qlf_k6n10f/counter.ys new file mode 100644 index 000000000..ebb6ce243 --- /dev/null +++ b/tests/arch/quicklogic/qlf_k6n10f/counter.ys @@ -0,0 +1,12 @@ +read_verilog ../../common/counter.v +hierarchy -top top +proc +flatten +equiv_opt -assert -multiclock -map +/quicklogic/qlf_k6n10f/cells_sim.v -map +/quicklogic/common/cells_sim.v synth_quicklogic -family qlf_k6n10f # 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 4 t:$lut +select -assert-count 8 t:adder_carry +select -assert-count 8 t:dffsre + +select -assert-none t:$lut t:adder_carry t:dffsre %% t:* %D diff --git a/tests/arch/quicklogic/qlf_k6n10f/dffs.ys b/tests/arch/quicklogic/qlf_k6n10f/dffs.ys new file mode 100644 index 000000000..a4a159f1b --- /dev/null +++ b/tests/arch/quicklogic/qlf_k6n10f/dffs.ys @@ -0,0 +1,21 @@ +read_verilog ../../common/dffs.v +rename dff my_dff # Work around conflicting module names between test and vendor cells +rename dffe my_dffe +design -save read + +hierarchy -top my_dff +proc +equiv_opt -async2sync -assert -map +/quicklogic/qlf_k6n10f/cells_sim.v -map +/quicklogic/common/cells_sim.v synth_quicklogic -family qlf_k6n10f # 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:sdffsre +select -assert-none t:sdffsre %% t:* %D + +design -load read +hierarchy -top my_dffe +proc +equiv_opt -async2sync -assert -map +/quicklogic/qlf_k6n10f/cells_sim.v -map +/quicklogic/common/cells_sim.v synth_quicklogic -family qlf_k6n10f # 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:sdffsre +select -assert-none t:sdffsre %% t:* %D diff --git a/tests/arch/quicklogic/qlf_k6n10f/fsm.ys b/tests/arch/quicklogic/qlf_k6n10f/fsm.ys new file mode 100644 index 000000000..e7a9d962d --- /dev/null +++ b/tests/arch/quicklogic/qlf_k6n10f/fsm.ys @@ -0,0 +1,17 @@ +read_verilog ../../common/fsm.v +hierarchy -top fsm +proc +flatten + +equiv_opt -run :prove -map +/quicklogic/qlf_k6n10f/cells_sim.v -map +/quicklogic/common/cells_sim.v synth_quicklogic -family qlf_k6n10f +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 9 t:$lut +select -assert-count 6 t:sdffsre + +select -assert-none t:$lut t:sdffsre %% t:* %D diff --git a/tests/arch/quicklogic/qlf_k6n10f/latches.ys b/tests/arch/quicklogic/qlf_k6n10f/latches.ys new file mode 100644 index 000000000..59574a1fb --- /dev/null +++ b/tests/arch/quicklogic/qlf_k6n10f/latches.ys @@ -0,0 +1,29 @@ +read_verilog ../../common/latches.v +design -save read + +hierarchy -top latchp +proc +equiv_opt -assert -async2sync -map +/quicklogic/qlf_k6n10f/cells_sim.v synth_quicklogic -family qlf_k6n10f +design -load postopt +cd latchp +select -assert-count 1 t:latchsre +select -assert-none t:latchsre %% t:* %D + +design -load read +hierarchy -top latchn +proc +equiv_opt -assert -async2sync -map +/quicklogic/qlf_k6n10f/cells_sim.v synth_quicklogic -family qlf_k6n10f +design -load postopt +cd latchn +select -assert-count 1 t:latchnsre +select -assert-none t:latchnsre %% t:* %D + +design -load read +hierarchy -top latchsr +proc +equiv_opt -assert -async2sync -map +/quicklogic/qlf_k6n10f/cells_sim.v synth_quicklogic -family qlf_k6n10f +design -load postopt +cd latchsr +select -assert-count 2 t:$lut +select -assert-count 1 t:latchnsre +select -assert-none t:$lut t:latchnsre %% t:* %D diff --git a/tests/arch/quicklogic/qlf_k6n10f/logic.ys b/tests/arch/quicklogic/qlf_k6n10f/logic.ys new file mode 100644 index 000000000..a24d5a479 --- /dev/null +++ b/tests/arch/quicklogic/qlf_k6n10f/logic.ys @@ -0,0 +1,10 @@ +read_verilog ../../common/logic.v +hierarchy -top top +proc +equiv_opt -assert -map +/quicklogic/qlf_k6n10f/cells_sim.v -map +/quicklogic/common/cells_sim.v synth_quicklogic -family qlf_k6n10f # 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 9 t:$lut + +select -assert-none t:$lut %% t:* %D diff --git a/tests/arch/quicklogic/qlf_k6n10f/mux.ys b/tests/arch/quicklogic/qlf_k6n10f/mux.ys new file mode 100644 index 000000000..633b5fc86 --- /dev/null +++ b/tests/arch/quicklogic/qlf_k6n10f/mux.ys @@ -0,0 +1,40 @@ +read_verilog ../../common/mux.v +design -save read + +hierarchy -top mux2 +proc +equiv_opt -assert -map +/quicklogic/qlf_k6n10f/cells_sim.v -map +/quicklogic/common/cells_sim.v synth_quicklogic -family qlf_k6n10f # 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:$lut r:WIDTH=3 %i +select -assert-none t:$lut r:WIDTH=3 %i %% t:* %D + +design -load read +hierarchy -top mux4 +proc +equiv_opt -assert -map +/quicklogic/qlf_k6n10f/cells_sim.v -map +/quicklogic/common/cells_sim.v synth_quicklogic -family qlf_k6n10f # 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:$lut r:WIDTH=6 %i +select -assert-none t:$lut r:WIDTH=6 %i %% t:* %D + +design -load read +hierarchy -top mux8 +proc +equiv_opt -assert -map +/quicklogic/qlf_k6n10f/cells_sim.v -map +/quicklogic/common/cells_sim.v synth_quicklogic -family qlf_k6n10f # 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 2 t:$lut r:WIDTH=6 %i +select -assert-count 1 t:$lut r:WIDTH=3 %i +select -assert-none t:$lut r:WIDTH=6 r:WIDTH=3 %u %i %% t:* %D + +design -load read +hierarchy -top mux16 +proc +equiv_opt -assert -map +/quicklogic/qlf_k6n10f/cells_sim.v -map +/quicklogic/common/cells_sim.v synth_quicklogic -family qlf_k6n10f # 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-max 5 t:$lut r:WIDTH=6 %i # OOT flow does 2 +select -assert-max 1 t:$lut r:WIDTH=3 %i # and here 1 +select -assert-max 1 t:$lut r:WIDTH=4 r:WIDTH=5 %u %i +select -assert-none t:$lut r:WIDTH>2 %i %% t:* %D diff --git a/tests/arch/quicklogic/qlf_k6n10f/run-test.sh b/tests/arch/quicklogic/qlf_k6n10f/run-test.sh new file mode 100755 index 000000000..36689edde --- /dev/null +++ b/tests/arch/quicklogic/qlf_k6n10f/run-test.sh @@ -0,0 +1,4 @@ +#!/usr/bin/env bash +set -eu +source ../../../gen-tests-makefile.sh +run_tests --yosys-scripts --bash