mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-11-04 13:29:12 +00:00
Code Activity

Make test without iopads

Browse source
This commit is contained in:
Miodrag Milanovic 2019-12-28 16:22:24 +01:00
parent 509da7ed1a
commit a82c701668
17 changed files with 51 additions and 51 deletions
Download patch file Download diff file Expand all files Collapse all files

2
tests/arch/xilinx/add_sub.ys
View file

@ -1,7 +1,7 @@
read_verilog ../common/add_sub.v read_verilog ../common/add_sub.v
hierarchy -top top hierarchy -top top
proc proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check equiv_opt -assert -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) 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 cd top # Constrain all select calls below inside the top module
select -assert-count 14 t:LUT2 select -assert-count 14 t:LUT2

8
tests/arch/xilinx/adffs.ys
View file

@ -3,7 +3,7 @@ design -save read
hierarchy -top adff hierarchy -top adff
proc proc
equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check equiv_opt -async2sync -assert -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) 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 cd adff # Constrain all select calls below inside the top module
select -assert-count 1 t:BUFG select -assert-count 1 t:BUFG
@ -15,7 +15,7 @@ select -assert-none t:BUFG t:FDCE %% t:* %D
design -load read design -load read
hierarchy -top adffn hierarchy -top adffn
proc proc
equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check equiv_opt -async2sync -assert -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) 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 cd adffn # Constrain all select calls below inside the top module
select -assert-count 1 t:BUFG select -assert-count 1 t:BUFG
@ -28,7 +28,7 @@ select -assert-none t:BUFG t:FDCE t:INV %% t:* %D
design -load read design -load read
hierarchy -top dffs hierarchy -top dffs
proc proc
equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check equiv_opt -async2sync -assert -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) 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 cd dffs # Constrain all select calls below inside the top module
select -assert-count 1 t:BUFG select -assert-count 1 t:BUFG
@ -40,7 +40,7 @@ select -assert-none t:BUFG t:FDSE %% t:* %D
design -load read design -load read
hierarchy -top ndffnr hierarchy -top ndffnr
proc proc
equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check equiv_opt -async2sync -assert -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) 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 cd ndffnr # Constrain all select calls below inside the top module
select -assert-count 1 t:BUFG select -assert-count 1 t:BUFG

12
tests/arch/xilinx/attributes_test.ys
View file

@ -1,7 +1,7 @@
# Check that blockram memory without parameters is not modified # Check that blockram memory without parameters is not modified
read_verilog ../common/memory_attributes/attributes_test.v read_verilog ../common/memory_attributes/attributes_test.v
hierarchy -top block_ram hierarchy -top block_ram
synth_xilinx -top block_ram synth_xilinx -top block_ram -noiopad
cd block_ram # Constrain all select calls below inside the top module cd block_ram # Constrain all select calls below inside the top module
select -assert-count 1 t:RAMB18E1 select -assert-count 1 t:RAMB18E1
@ -9,7 +9,7 @@ select -assert-count 1 t:RAMB18E1
design -reset design -reset
read_verilog ../common/memory_attributes/attributes_test.v read_verilog ../common/memory_attributes/attributes_test.v
hierarchy -top distributed_ram hierarchy -top distributed_ram
synth_xilinx -top distributed_ram synth_xilinx -top distributed_ram -noiopad
cd distributed_ram # Constrain all select calls below inside the top module cd distributed_ram # Constrain all select calls below inside the top module
select -assert-count 8 t:RAM32X1D select -assert-count 8 t:RAM32X1D
@ -18,7 +18,7 @@ design -reset
read_verilog ../common/memory_attributes/attributes_test.v read_verilog ../common/memory_attributes/attributes_test.v
prep prep
setattr -mod -set ram_style "distributed" block_ram setattr -mod -set ram_style "distributed" block_ram
synth_xilinx -top block_ram synth_xilinx -top block_ram -noiopad
cd block_ram # Constrain all select calls below inside the top module cd block_ram # Constrain all select calls below inside the top module
select -assert-count 32 t:RAM128X1D select -assert-count 32 t:RAM128X1D
@ -27,7 +27,7 @@ design -reset
read_verilog ../common/memory_attributes/attributes_test.v read_verilog ../common/memory_attributes/attributes_test.v
prep prep
setattr -mod -set logic_block 1 block_ram setattr -mod -set logic_block 1 block_ram
synth_xilinx -top block_ram synth_xilinx -top block_ram -noiopad
cd block_ram # Constrain all select calls below inside the top module cd block_ram # Constrain all select calls below inside the top module
select -assert-count 0 t:RAMB18E1 select -assert-count 0 t:RAMB18E1
select -assert-count 32 t:RAM128X1D select -assert-count 32 t:RAM128X1D
@ -35,13 +35,13 @@ select -assert-count 32 t:RAM128X1D
# Set ram_style block to a distributed memory; will be implemented as blockram # Set ram_style block to a distributed memory; will be implemented as blockram
design -reset design -reset
read_verilog ../common/memory_attributes/attributes_test.v read_verilog ../common/memory_attributes/attributes_test.v
synth_xilinx -top distributed_ram_manual synth_xilinx -top distributed_ram_manual -noiopad
cd distributed_ram_manual # Constrain all select calls below inside the top module cd distributed_ram_manual # Constrain all select calls below inside the top module
select -assert-count 1 t:RAMB18E1 select -assert-count 1 t:RAMB18E1
# Set synthesis, ram_block block to a distributed memory; will be implemented as blockram # Set synthesis, ram_block block to a distributed memory; will be implemented as blockram
design -reset design -reset
read_verilog ../common/memory_attributes/attributes_test.v read_verilog ../common/memory_attributes/attributes_test.v
synth_xilinx -top distributed_ram_manual_syn synth_xilinx -top distributed_ram_manual_syn -noiopad
cd distributed_ram_manual_syn # Constrain all select calls below inside the top module cd distributed_ram_manual_syn # Constrain all select calls below inside the top module
select -assert-count 1 t:RAMB18E1 select -assert-count 1 t:RAMB18E1

24
tests/arch/xilinx/blockram.ys
View file

@ -3,28 +3,28 @@
# Memory bits <= 18K; Data width <= 36; Address width <= 14: -> RAMB18E1 # Memory bits <= 18K; Data width <= 36; Address width <= 14: -> RAMB18E1
read_verilog ../common/blockram.v read_verilog ../common/blockram.v
chparam -set ADDRESS_WIDTH 10 -set DATA_WIDTH 1 sync_ram_sdp chparam -set ADDRESS_WIDTH 10 -set DATA_WIDTH 1 sync_ram_sdp
synth_xilinx -top sync_ram_sdp synth_xilinx -top sync_ram_sdp -noiopad
cd sync_ram_sdp cd sync_ram_sdp
select -assert-count 1 t:RAMB18E1 select -assert-count 1 t:RAMB18E1
design -reset design -reset
read_verilog ../common/blockram.v read_verilog ../common/blockram.v
chparam -set ADDRESS_WIDTH 8 -set DATA_WIDTH 18 sync_ram_sdp chparam -set ADDRESS_WIDTH 8 -set DATA_WIDTH 18 sync_ram_sdp
synth_xilinx -top sync_ram_sdp synth_xilinx -top sync_ram_sdp -noiopad
cd sync_ram_sdp cd sync_ram_sdp
select -assert-count 1 t:RAMB18E1 select -assert-count 1 t:RAMB18E1
design -reset design -reset
read_verilog ../common/blockram.v read_verilog ../common/blockram.v
chparam -set ADDRESS_WIDTH 14 -set DATA_WIDTH 1 sync_ram_sdp chparam -set ADDRESS_WIDTH 14 -set DATA_WIDTH 1 sync_ram_sdp
synth_xilinx -top sync_ram_sdp synth_xilinx -top sync_ram_sdp -noiopad
cd sync_ram_sdp cd sync_ram_sdp
select -assert-count 1 t:RAMB18E1 select -assert-count 1 t:RAMB18E1
design -reset design -reset
read_verilog ../common/blockram.v read_verilog ../common/blockram.v
chparam -set ADDRESS_WIDTH 9 -set DATA_WIDTH 36 sync_ram_sdp chparam -set ADDRESS_WIDTH 9 -set DATA_WIDTH 36 sync_ram_sdp
synth_xilinx -top sync_ram_sdp synth_xilinx -top sync_ram_sdp -noiopad
cd sync_ram_sdp cd sync_ram_sdp
select -assert-count 1 t:RAMB18E1 select -assert-count 1 t:RAMB18E1
@ -32,7 +32,7 @@ select -assert-count 1 t:RAMB18E1
design -reset design -reset
read_verilog ../common/blockram.v read_verilog ../common/blockram.v
chparam -set ADDRESS_WIDTH 8 -set DATA_WIDTH 2 sync_ram_sdp chparam -set ADDRESS_WIDTH 8 -set DATA_WIDTH 2 sync_ram_sdp
synth_xilinx -top sync_ram_sdp synth_xilinx -top sync_ram_sdp -noiopad
cd sync_ram_sdp cd sync_ram_sdp
select -assert-count 0 t:RAMB18E1 select -assert-count 0 t:RAMB18E1
select -assert-count 4 t:RAM128X1D select -assert-count 4 t:RAM128X1D
@ -41,7 +41,7 @@ select -assert-count 4 t:RAM128X1D
design -reset design -reset
read_verilog ../common/blockram.v read_verilog ../common/blockram.v
chparam -set ADDRESS_WIDTH 10 -set DATA_WIDTH 36 sync_ram_sdp chparam -set ADDRESS_WIDTH 10 -set DATA_WIDTH 36 sync_ram_sdp
synth_xilinx -top sync_ram_sdp synth_xilinx -top sync_ram_sdp -noiopad
cd sync_ram_sdp cd sync_ram_sdp
select -assert-count 1 t:RAMB36E1 select -assert-count 1 t:RAMB36E1
@ -52,7 +52,7 @@ design -reset
read_verilog ../common/blockram.v read_verilog ../common/blockram.v
hierarchy -top sync_ram_sdp -chparam ADDRESS_WIDTH 10 -chparam DATA_WIDTH 1 hierarchy -top sync_ram_sdp -chparam ADDRESS_WIDTH 10 -chparam DATA_WIDTH 1
setattr -set ram_style "block" m:memory setattr -set ram_style "block" m:memory
synth_xilinx -top sync_ram_sdp synth_xilinx -top sync_ram_sdp -noiopad
cd sync_ram_sdp cd sync_ram_sdp
select -assert-count 1 t:RAMB18E1 select -assert-count 1 t:RAMB18E1
@ -60,7 +60,7 @@ design -reset
read_verilog ../common/blockram.v read_verilog ../common/blockram.v
hierarchy -top sync_ram_sdp -chparam ADDRESS_WIDTH 10 -chparam DATA_WIDTH 1 hierarchy -top sync_ram_sdp -chparam ADDRESS_WIDTH 10 -chparam DATA_WIDTH 1
setattr -set ram_block 1 m:memory setattr -set ram_block 1 m:memory
synth_xilinx -top sync_ram_sdp synth_xilinx -top sync_ram_sdp -noiopad
cd sync_ram_sdp cd sync_ram_sdp
select -assert-count 1 t:RAMB18E1 select -assert-count 1 t:RAMB18E1
@ -68,7 +68,7 @@ design -reset
read_verilog ../common/blockram.v read_verilog ../common/blockram.v
hierarchy -top sync_ram_sdp -chparam ADDRESS_WIDTH 10 -chparam DATA_WIDTH 1 hierarchy -top sync_ram_sdp -chparam ADDRESS_WIDTH 10 -chparam DATA_WIDTH 1
setattr -set ram_style "dont_infer_a_ram_pretty_please" m:memory setattr -set ram_style "dont_infer_a_ram_pretty_please" m:memory
synth_xilinx -top sync_ram_sdp synth_xilinx -top sync_ram_sdp -noiopad
cd sync_ram_sdp cd sync_ram_sdp
select -assert-count 0 t:RAMB18E1 select -assert-count 0 t:RAMB18E1
@ -76,7 +76,7 @@ design -reset
read_verilog ../common/blockram.v read_verilog ../common/blockram.v
hierarchy -top sync_ram_sdp -chparam ADDRESS_WIDTH 10 -chparam DATA_WIDTH 1 hierarchy -top sync_ram_sdp -chparam ADDRESS_WIDTH 10 -chparam DATA_WIDTH 1
setattr -set logic_block 1 m:memory setattr -set logic_block 1 m:memory
synth_xilinx -top sync_ram_sdp synth_xilinx -top sync_ram_sdp -noiopad
cd sync_ram_sdp cd sync_ram_sdp
select -assert-count 0 t:RAMB18E1 select -assert-count 0 t:RAMB18E1
@ -84,7 +84,7 @@ design -reset
read_verilog ../common/blockram.v read_verilog ../common/blockram.v
hierarchy -top sync_ram_sdp -chparam ADDRESS_WIDTH 8 -chparam DATA_WIDTH 1 hierarchy -top sync_ram_sdp -chparam ADDRESS_WIDTH 8 -chparam DATA_WIDTH 1
setattr -set ram_style "block" m:memory setattr -set ram_style "block" m:memory
synth_xilinx -top sync_ram_sdp synth_xilinx -top sync_ram_sdp -noiopad
cd sync_ram_sdp cd sync_ram_sdp
select -assert-count 1 t:RAMB18E1 select -assert-count 1 t:RAMB18E1
@ -92,6 +92,6 @@ design -reset
read_verilog ../common/blockram.v read_verilog ../common/blockram.v
hierarchy -top sync_ram_sdp -chparam ADDRESS_WIDTH 8 -chparam DATA_WIDTH 1 hierarchy -top sync_ram_sdp -chparam ADDRESS_WIDTH 8 -chparam DATA_WIDTH 1
setattr -set ram_block 1 m:memory setattr -set ram_block 1 m:memory
synth_xilinx -top sync_ram_sdp synth_xilinx -top sync_ram_sdp -noiopad
cd sync_ram_sdp cd sync_ram_sdp
select -assert-count 1 t:RAMB18E1 select -assert-count 1 t:RAMB18E1

2
tests/arch/xilinx/bug1460.ys
View file

@ -28,7 +28,7 @@ module register_file(
endmodule endmodule
EOT EOT
synth_xilinx synth_xilinx -noiopad
cd register_file cd register_file
select -assert-count 32 t:RAM32M select -assert-count 32 t:RAM32M
select -assert-none t:* t:BUFG %d t:RAM32M %d select -assert-none t:* t:BUFG %d t:RAM32M %d

2
tests/arch/xilinx/counter.ys
View file

@ -2,7 +2,7 @@ read_verilog ../common/counter.v
hierarchy -top top hierarchy -top top
proc proc
flatten flatten
equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check equiv_opt -async2sync -assert -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) 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 cd top # Constrain all select calls below inside the top module

4
tests/arch/xilinx/dffs.ys
View file

@ -3,7 +3,7 @@ design -save read
hierarchy -top dff hierarchy -top dff
proc proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check equiv_opt -assert -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) 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 cd dff # Constrain all select calls below inside the top module
select -assert-count 1 t:BUFG select -assert-count 1 t:BUFG
@ -15,7 +15,7 @@ select -assert-none t:BUFG t:FDRE %% t:* %D
design -load read design -load read
hierarchy -top dffe hierarchy -top dffe
proc proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check equiv_opt -assert -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) 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 cd dffe # Constrain all select calls below inside the top module
select -assert-count 1 t:BUFG select -assert-count 1 t:BUFG

2
tests/arch/xilinx/dsp_fastfir.ys
View file

@ -63,7 +63,7 @@ module fastfir_dynamictaps(i_clk, i_reset, i_tap_wr, i_tap, i_ce, i_sample, o_re
endmodule endmodule
EOT EOT
synth_xilinx synth_xilinx -noiopad
cd fastfir_dynamictaps cd fastfir_dynamictaps
select -assert-count 2 t:DSP48E1 select -assert-count 2 t:DSP48E1
select -assert-none t:* t:DSP48E1 %d t:BUFG %d select -assert-none t:* t:DSP48E1 %d t:BUFG %d

2
tests/arch/xilinx/fsm.ys
View file

@ -3,7 +3,7 @@ hierarchy -top fsm
proc proc
flatten flatten
equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad
miter -equiv -make_assert -flatten gold gate miter 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 sat -verify -prove-asserts -show-public -set-at 1 in_reset 1 -seq 20 -prove-skip 1 miter

6
tests/arch/xilinx/latches.ys
View file

@ -3,7 +3,7 @@ design -save read
hierarchy -top latchp hierarchy -top latchp
proc proc
equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check equiv_opt -async2sync -assert -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) design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd latchp # Constrain all select calls below inside the top module cd latchp # Constrain all select calls below inside the top module
select -assert-count 1 t:LDCE select -assert-count 1 t:LDCE
@ -14,7 +14,7 @@ select -assert-none t:LDCE %% t:* %D
design -load read design -load read
hierarchy -top latchn hierarchy -top latchn
proc proc
equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check equiv_opt -async2sync -assert -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) 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 cd latchn # Constrain all select calls below inside the top module
select -assert-count 1 t:LDCE select -assert-count 1 t:LDCE
@ -26,7 +26,7 @@ select -assert-none t:LDCE t:INV %% t:* %D
design -load read design -load read
hierarchy -top latchsr hierarchy -top latchsr
proc proc
equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check equiv_opt -async2sync -assert -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) design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd latchsr # Constrain all select calls below inside the top module cd latchsr # Constrain all select calls below inside the top module
select -assert-count 1 t:LDCE select -assert-count 1 t:LDCE

2
tests/arch/xilinx/logic.ys
View file

@ -1,7 +1,7 @@
read_verilog ../common/logic.v read_verilog ../common/logic.v
hierarchy -top top hierarchy -top top
proc proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check equiv_opt -assert -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) 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 cd top # Constrain all select calls below inside the top module

14
tests/arch/xilinx/lutram.ys
View file

@ -2,7 +2,7 @@
#hierarchy -top lutram_1w1r -chparam A_WIDTH 4 #hierarchy -top lutram_1w1r -chparam A_WIDTH 4
#proc #proc
#memory -nomap #memory -nomap
#equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx #equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad
#memory #memory
#opt -full #opt -full
# #
@ -22,7 +22,7 @@ read_verilog ../common/lutram.v
hierarchy -top lutram_1w1r -chparam A_WIDTH 5 hierarchy -top lutram_1w1r -chparam A_WIDTH 5
proc proc
memory -nomap memory -nomap
equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad
memory memory
opt -full opt -full
@ -42,7 +42,7 @@ read_verilog ../common/lutram.v
hierarchy -top lutram_1w1r hierarchy -top lutram_1w1r
proc proc
memory -nomap memory -nomap
equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad
memory memory
opt -full opt -full
@ -62,7 +62,7 @@ read_verilog ../common/lutram.v
hierarchy -top lutram_1w3r hierarchy -top lutram_1w3r
proc proc
memory -nomap memory -nomap
equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad
memory memory
opt -full opt -full
@ -82,7 +82,7 @@ read_verilog ../common/lutram.v
hierarchy -top lutram_1w3r -chparam A_WIDTH 6 hierarchy -top lutram_1w3r -chparam A_WIDTH 6
proc proc
memory -nomap memory -nomap
equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad
memory memory
opt -full opt -full
@ -102,7 +102,7 @@ read_verilog ../common/lutram.v
hierarchy -top lutram_1w1r -chparam A_WIDTH 5 -chparam D_WIDTH 6 hierarchy -top lutram_1w1r -chparam A_WIDTH 5 -chparam D_WIDTH 6
proc proc
memory -nomap memory -nomap
equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad
memory memory
opt -full opt -full
@ -122,7 +122,7 @@ read_verilog ../common/lutram.v
hierarchy -top lutram_1w1r -chparam A_WIDTH 6 -chparam D_WIDTH 6 hierarchy -top lutram_1w1r -chparam A_WIDTH 6 -chparam D_WIDTH 6
proc proc
memory -nomap memory -nomap
equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad
memory memory
opt -full opt -full

8
tests/arch/xilinx/macc.ys
View file

@ -3,8 +3,8 @@ design -save read
hierarchy -top macc hierarchy -top macc
proc proc
#equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx ### TODO #equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad ### TODO
equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad
miter -equiv -flatten -make_assert -make_outputs gold gate miter miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -seq 10 -show-inputs -show-outputs miter sat -verify -prove-asserts -seq 10 -show-inputs -show-outputs miter
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
@ -17,8 +17,8 @@ select -assert-none t:BUFG t:FDRE t:DSP48E1 %% t:* %D
design -load read design -load read
hierarchy -top macc2 hierarchy -top macc2
proc proc
#equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx ### TODO #equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad ### TODO
equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad
miter -equiv -flatten -make_assert -make_outputs gold gate miter miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -seq 10 -show-inputs -show-outputs miter sat -verify -prove-asserts -seq 10 -show-inputs -show-outputs miter
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)

2
tests/arch/xilinx/mul.ys
View file

@ -1,7 +1,7 @@
read_verilog ../common/mul.v read_verilog ../common/mul.v
hierarchy -top top hierarchy -top top
proc proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check equiv_opt -assert -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) 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 cd top # Constrain all select calls below inside the top module

2
tests/arch/xilinx/mul_unsigned.ys
View file

@ -2,7 +2,7 @@ read_verilog mul_unsigned.v
hierarchy -top mul_unsigned hierarchy -top mul_unsigned
proc proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check equiv_opt -assert -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) design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd mul_unsigned # Constrain all select calls below inside the top module cd mul_unsigned # Constrain all select calls below inside the top module
select -assert-count 1 t:BUFG select -assert-count 1 t:BUFG

8
tests/arch/xilinx/mux.ys
View file

@ -3,7 +3,7 @@ design -save read
hierarchy -top mux2 hierarchy -top mux2
proc proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check equiv_opt -assert -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) 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 cd mux2 # Constrain all select calls below inside the top module
select -assert-count 1 t:LUT3 select -assert-count 1 t:LUT3
@ -14,7 +14,7 @@ select -assert-none t:LUT3 %% t:* %D
design -load read design -load read
hierarchy -top mux4 hierarchy -top mux4
proc proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check equiv_opt -assert -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) 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 cd mux4 # Constrain all select calls below inside the top module
select -assert-count 1 t:LUT6 select -assert-count 1 t:LUT6
@ -25,7 +25,7 @@ select -assert-none t:LUT6 %% t:* %D
design -load read design -load read
hierarchy -top mux8 hierarchy -top mux8
proc proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check equiv_opt -assert -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) 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 cd mux8 # Constrain all select calls below inside the top module
select -assert-count 1 t:LUT3 select -assert-count 1 t:LUT3
@ -37,7 +37,7 @@ select -assert-none t:LUT3 t:LUT6 %% t:* %D
design -load read design -load read
hierarchy -top mux16 hierarchy -top mux16
proc proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check equiv_opt -assert -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) 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 cd mux16 # Constrain all select calls below inside the top module
select -assert-min 5 t:LUT6 select -assert-min 5 t:LUT6

2
tests/arch/xilinx/shifter.ys
View file

@ -2,7 +2,7 @@ read_verilog ../common/shifter.v
hierarchy -top top hierarchy -top top
proc proc
flatten flatten
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check equiv_opt -assert -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) 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 cd top # Constrain all select calls below inside the top module