quicklogic: Add basic k6n10f tests

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

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

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

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

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 

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

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

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

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

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