3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-04-27 10:55:51 +00:00

quicklogic: Move pp3 tests one level down

This commit is contained in:
Martin Povišer 2023-10-09 13:13:42 +02:00
parent f84ab98055
commit 74296e3d92
11 changed files with 11 additions and 11 deletions

View file

@ -0,0 +1,11 @@
read_verilog ../../common/add_sub.v
hierarchy -top top
equiv_opt -assert -map +/quicklogic/pp3/cells_sim.v synth_quicklogic -family pp3 # 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:LUT2
select -assert-count 8 t:LUT3
select -assert-count 2 t:LUT4
select -assert-count 8 t:inpad
select -assert-count 8 t:outpad
select -assert-none t:LUT2 t:LUT3 t:LUT4 t:inpad t:outpad %% t:* %D

View file

@ -0,0 +1,67 @@
read_verilog ../../common/adffs.v
design -save read
hierarchy -top adff
proc
equiv_opt -async2sync -assert -map +/quicklogic/pp3/cells_sim.v -map +/quicklogic/common/cells_sim.v synth_quicklogic # 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:dffepc
select -assert-count 1 t:logic_0
select -assert-count 1 t:logic_1
select -assert-count 1 t:inpad
select -assert-count 1 t:outpad
select -assert-count 2 t:ckpad
select -assert-none t:dffepc t:logic_0 t:logic_1 t:inpad t:outpad t:ckpad %% t:* %D
design -load read
hierarchy -top adffn
proc
equiv_opt -async2sync -assert -map +/quicklogic/pp3/cells_sim.v -map +/quicklogic/common/cells_sim.v synth_quicklogic # 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:LUT1
select -assert-count 1 t:dffepc
select -assert-count 1 t:logic_0
select -assert-count 1 t:logic_1
select -assert-count 2 t:inpad
select -assert-count 1 t:outpad
select -assert-count 1 t:ckpad
select -assert-none t:LUT1 t:dffepc t:logic_0 t:logic_1 t:inpad t:outpad t:ckpad %% t:* %D
design -load read
hierarchy -top dffs
proc
equiv_opt -async2sync -assert -map +/quicklogic/pp3/cells_sim.v -map +/quicklogic/common/cells_sim.v synth_quicklogic # 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:LUT2
select -assert-count 1 t:dffepc
select -assert-count 1 t:logic_0
select -assert-count 1 t:logic_1
select -assert-count 3 t:inpad
select -assert-count 1 t:outpad
select -assert-count 1 t:ckpad
select -assert-none t:LUT2 t:dffepc t:logic_0 t:logic_1 t:inpad t:outpad t:ckpad %% t:* %D
design -load read
hierarchy -top ndffnr
proc
equiv_opt -async2sync -assert -map +/quicklogic/pp3/cells_sim.v -map +/quicklogic/common/cells_sim.v synth_quicklogic # 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:LUT1
select -assert-count 1 t:LUT2
select -assert-count 1 t:dffepc
select -assert-count 1 t:logic_0
select -assert-count 1 t:logic_1
select -assert-count 4 t:inpad
select -assert-count 1 t:outpad
select -assert-none t:LUT1 t:LUT2 t:dffepc t:logic_0 t:logic_1 t:inpad t:outpad %% t:* %D

View file

@ -0,0 +1,18 @@
read_verilog ../../common/counter.v
hierarchy -top top
proc
flatten
equiv_opt -assert -multiclock -map +/quicklogic/pp3/cells_sim.v -map +/quicklogic/common/cells_sim.v synth_quicklogic # 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:LUT1
select -assert-count 3 t:LUT2
select -assert-count 5 t:LUT3
select -assert-count 1 t:LUT4
select -assert-count 8 t:dffepc
select -assert-count 1 t:logic_0
select -assert-count 1 t:logic_1
select -assert-count 8 t:outpad
select -assert-count 2 t:ckpad
select -assert-none t:LUT1 t:LUT2 t:LUT3 t:LUT4 t:dffepc t:logic_0 t:logic_1 t:outpad t:ckpad %% t:* %D

View file

@ -0,0 +1,33 @@
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/pp3/cells_sim.v -map +/quicklogic/common/cells_sim.v synth_quicklogic # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd my_dff # Constrain all select calls below inside the top module
select -assert-count 1 t:ckpad
select -assert-count 1 t:dffepc
select -assert-count 1 t:inpad
select -assert-count 1 t:logic_0
select -assert-count 1 t:logic_1
select -assert-count 1 t:outpad
select -assert-none t:ckpad t:dffepc t:inpad t:logic_0 t:logic_1 t:outpad %% t:* %D
design -load read
hierarchy -top my_dffe
proc
equiv_opt -async2sync -assert -map +/quicklogic/pp3/cells_sim.v -map +/quicklogic/common/cells_sim.v synth_quicklogic # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd my_dffe # Constrain all select calls below inside the top module
select -assert-count 1 t:ckpad
select -assert-count 1 t:dffepc
select -assert-count 2 t:inpad
select -assert-count 1 t:logic_0
select -assert-count 1 t:outpad
select -assert-none t:ckpad t:dffepc t:inpad t:logic_0 t:outpad %% t:* %D

View file

@ -0,0 +1,23 @@
read_verilog ../../common/fsm.v
hierarchy -top fsm
proc
flatten
equiv_opt -run :prove -map +/quicklogic/pp3/cells_sim.v -map +/quicklogic/common/cells_sim.v synth_quicklogic
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 1 t:LUT2
select -assert-count 9 t:LUT3
select -assert-count 4 t:dffepc
select -assert-count 1 t:logic_0
select -assert-count 1 t:logic_1
select -assert-count 3 t:inpad
select -assert-count 2 t:outpad
select -assert-count 1 t:ckpad
select -assert-none t:LUT2 t:LUT3 t:dffepc t:logic_0 t:logic_1 t:inpad t:outpad t:ckpad %% t:* %D

View file

@ -0,0 +1,40 @@
read_verilog ../../common/latches.v
design -save read
hierarchy -top latchp
proc
# Can't run any sort of equivalence check because latches are blown to LUTs
synth_quicklogic
cd latchp # Constrain all select calls below inside the top module
select -assert-count 1 t:LUT3
select -assert-count 3 t:inpad
select -assert-count 1 t:outpad
select -assert-none t:LUT3 t:inpad t:outpad %% t:* %D
design -load read
hierarchy -top latchn
proc
# Can't run any sort of equivalence check because latches are blown to LUTs
synth_quicklogic
cd latchn # Constrain all select calls below inside the top module
select -assert-count 1 t:LUT3
select -assert-count 3 t:inpad
select -assert-count 1 t:outpad
select -assert-none t:LUT3 t:inpad t:outpad %% t:* %D
design -load read
hierarchy -top latchsr
proc
# Can't run any sort of equivalence check because latches are blown to LUTs
synth_quicklogic
cd latchsr # Constrain all select calls below inside the top module
select -assert-count 1 t:LUT2
select -assert-count 1 t:LUT4
select -assert-count 5 t:inpad
select -assert-count 1 t:outpad
select -assert-none t:LUT2 t:LUT4 t:inpad t:outpad %% t:* %D

View file

@ -0,0 +1,14 @@
read_verilog ../../common/logic.v
hierarchy -top top
proc
equiv_opt -assert -map +/quicklogic/pp3/cells_sim.v -map +/quicklogic/common/cells_sim.v synth_quicklogic # 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:LUT1
select -assert-count 6 t:LUT2
select -assert-count 2 t:LUT3
select -assert-count 8 t:inpad
select -assert-count 10 t:outpad
select -assert-none t:LUT1 t:LUT2 t:LUT3 t:inpad t:outpad %% t:* %D

View file

@ -0,0 +1,52 @@
read_verilog ../../common/mux.v
design -save read
hierarchy -top mux2
proc
equiv_opt -assert -map +/quicklogic/pp3/cells_sim.v -map +/quicklogic/common/cells_sim.v synth_quicklogic # 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:LUT3
select -assert-count 3 t:inpad
select -assert-count 1 t:outpad
select -assert-none t:LUT3 t:inpad t:outpad %% t:* %D
design -load read
hierarchy -top mux4
proc
equiv_opt -assert -map +/quicklogic/pp3/cells_sim.v -map +/quicklogic/common/cells_sim.v synth_quicklogic # 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 3 t:LUT3
select -assert-count 6 t:inpad
select -assert-count 1 t:outpad
select -assert-none t:LUT3 t:inpad t:outpad %% t:* %D
design -load read
hierarchy -top mux8
proc
equiv_opt -assert -map +/quicklogic/pp3/cells_sim.v -map +/quicklogic/common/cells_sim.v synth_quicklogic # 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:LUT1
select -assert-count 1 t:LUT3
select -assert-count 2 t:mux4x0
select -assert-count 11 t:inpad
select -assert-count 1 t:outpad
select -assert-none t:LUT1 t:LUT3 t:mux4x0 t:inpad t:outpad %% t:* %D
design -load read
hierarchy -top mux16
proc
equiv_opt -assert -map +/quicklogic/pp3/cells_sim.v -map +/quicklogic/common/cells_sim.v synth_quicklogic # 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:LUT3
select -assert-count 2 t:mux8x0
select -assert-count 20 t:inpad
select -assert-count 1 t:outpad
select -assert-none t:LUT3 t:mux8x0 t:inpad t:outpad %% t:* %D

View file

@ -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.'"

View file

@ -0,0 +1,13 @@
read_verilog ../../common/tribuf.v
hierarchy -top tristate
proc
tribuf
flatten
synth
equiv_opt -assert -map +/quicklogic/pp3/cells_sim.v -map +/quicklogic/common/cells_sim.v -map +/simcells.v synth_quicklogic # 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 2 t:inpad
select -assert-count 1 t:outpad
select -assert-count 1 t:$_TBUF_
select -assert-none t:inpad t:outpad t:$_TBUF_ %% t:* %D