Skip to content

Y
yosys-tests
Commit f4c4f288 by Miodrag Milanovic
Options

Regression fix

parent d2e90b45
Showing with 191 additions and 115 deletions
architecture/synth_xilinx/synth_xilinx.ys
...@@ -9,7 +9,9 @@ cd dff # Constrain all select calls below inside the top module ...@@ -9,7 +9,9 @@ cd dff # Constrain all select calls below inside the top module
stat stat
select -assert-count 1 t:BUFG select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE select -assert-count 1 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D select -assert-count 2 t:IBUF
select -assert-count 1 t:OBUF
select -assert-none t:BUFG t:FDRE t:IBUF t:OBUF %% t:* %D
design -load read design -load read
hierarchy -top dffe hierarchy -top dffe
...@@ -20,7 +22,9 @@ cd dffe # Constrain all select calls below inside the top module ...@@ -20,7 +22,9 @@ cd dffe # Constrain all select calls below inside the top module
stat stat
select -assert-count 1 t:BUFG select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE select -assert-count 1 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D select -assert-count 3 t:IBUF
select -assert-count 1 t:OBUF
select -assert-none t:BUFG t:FDRE t:IBUF t:OBUF %% t:* %D
design -load read design -load read
...@@ -34,5 +38,7 @@ cd adff # Constrain all select calls below inside the top module ...@@ -34,5 +38,7 @@ cd adff # Constrain all select calls below inside the top module
stat stat
select -assert-count 1 t:BUFG select -assert-count 1 t:BUFG
select -assert-count 1 t:FDCE select -assert-count 1 t:FDCE
select -assert-none t:BUFG t:FDCE %% t:* %D select -assert-count 3 t:IBUF
select -assert-count 1 t:OBUF
select -assert-none t:BUFG t:FDCE t:IBUF t:OBUF %% t:* %D
architecture/synth_xilinx/synth_xilinx_abc9.ys
...@@ -9,7 +9,9 @@ cd dff # Constrain all select calls below inside the top module ...@@ -9,7 +9,9 @@ cd dff # Constrain all select calls below inside the top module
stat stat
select -assert-count 1 t:BUFG select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE select -assert-count 1 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D select -assert-count 2 t:IBUF
select -assert-count 1 t:OBUF
select -assert-none t:BUFG t:FDRE t:IBUF t:OBUF %% t:* %D
design -load read design -load read
hierarchy -top dffe hierarchy -top dffe
...@@ -20,5 +22,7 @@ cd dffe # Constrain all select calls below inside the top module ...@@ -20,5 +22,7 @@ cd dffe # Constrain all select calls below inside the top module
stat stat
select -assert-count 1 t:BUFG select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE select -assert-count 1 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D select -assert-count 3 t:IBUF
select -assert-count 1 t:OBUF
select -assert-none t:BUFG t:FDRE t:IBUF t:OBUF %% t:* %D
architecture/synth_xilinx/synth_xilinx_arch_xc6s.ys
...@@ -9,7 +9,9 @@ cd dff # Constrain all select calls below inside the top module ...@@ -9,7 +9,9 @@ cd dff # Constrain all select calls below inside the top module
stat stat
select -assert-count 1 t:BUFG select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE select -assert-count 1 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D select -assert-count 2 t:IBUF
select -assert-count 1 t:OBUF
select -assert-none t:BUFG t:FDRE t:IBUF t:OBUF %% t:* %D
design -load read design -load read
hierarchy -top dffe hierarchy -top dffe
...@@ -20,5 +22,7 @@ cd dffe # Constrain all select calls below inside the top module ...@@ -20,5 +22,7 @@ cd dffe # Constrain all select calls below inside the top module
stat stat
select -assert-count 1 t:BUFG select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE select -assert-count 1 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D select -assert-count 3 t:IBUF
select -assert-count 1 t:OBUF
select -assert-none t:BUFG t:FDRE t:IBUF t:OBUF %% t:* %D
architecture/synth_xilinx/synth_xilinx_arch_xc6s_abc9.ys
...@@ -9,7 +9,9 @@ cd dff # Constrain all select calls below inside the top module ...@@ -9,7 +9,9 @@ cd dff # Constrain all select calls below inside the top module
stat stat
select -assert-count 1 t:BUFG select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE select -assert-count 1 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D select -assert-count 2 t:IBUF
select -assert-count 1 t:OBUF
select -assert-none t:BUFG t:FDRE t:IBUF t:OBUF %% t:* %D
design -load read design -load read
hierarchy -top dffe hierarchy -top dffe
...@@ -20,5 +22,7 @@ cd dffe # Constrain all select calls below inside the top module ...@@ -20,5 +22,7 @@ cd dffe # Constrain all select calls below inside the top module
stat stat
select -assert-count 1 t:BUFG select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE select -assert-count 1 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D select -assert-count 3 t:IBUF
select -assert-count 1 t:OBUF
select -assert-none t:BUFG t:FDRE t:IBUF t:OBUF %% t:* %D
architecture/synth_xilinx/synth_xilinx_arch_xc6v.ys
...@@ -9,7 +9,9 @@ cd dff # Constrain all select calls below inside the top module ...@@ -9,7 +9,9 @@ cd dff # Constrain all select calls below inside the top module
stat stat
select -assert-count 1 t:BUFG select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE select -assert-count 1 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D select -assert-count 2 t:IBUF
select -assert-count 1 t:OBUF
select -assert-none t:BUFG t:FDRE t:IBUF t:OBUF %% t:* %D
design -load read design -load read
hierarchy -top dffe hierarchy -top dffe
...@@ -20,5 +22,7 @@ cd dffe # Constrain all select calls below inside the top module ...@@ -20,5 +22,7 @@ cd dffe # Constrain all select calls below inside the top module
stat stat
select -assert-count 1 t:BUFG select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE select -assert-count 1 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D select -assert-count 3 t:IBUF
select -assert-count 1 t:OBUF
select -assert-none t:BUFG t:FDRE t:IBUF t:OBUF %% t:* %D
architecture/synth_xilinx/synth_xilinx_arch_xc7.ys
...@@ -9,7 +9,9 @@ cd dff # Constrain all select calls below inside the top module ...@@ -9,7 +9,9 @@ cd dff # Constrain all select calls below inside the top module
stat stat
select -assert-count 1 t:BUFG select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE select -assert-count 1 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D select -assert-count 2 t:IBUF
select -assert-count 1 t:OBUF
select -assert-none t:BUFG t:FDRE t:IBUF t:OBUF %% t:* %D
design -load read design -load read
hierarchy -top dffe hierarchy -top dffe
...@@ -20,5 +22,7 @@ cd dffe # Constrain all select calls below inside the top module ...@@ -20,5 +22,7 @@ cd dffe # Constrain all select calls below inside the top module
stat stat
select -assert-count 1 t:BUFG select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE select -assert-count 1 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D select -assert-count 3 t:IBUF
select -assert-count 1 t:OBUF
select -assert-none t:BUFG t:FDRE t:IBUF t:OBUF %% t:* %D
architecture/synth_xilinx/synth_xilinx_arch_xcu.ys
...@@ -9,7 +9,9 @@ cd dff # Constrain all select calls below inside the top module ...@@ -9,7 +9,9 @@ cd dff # Constrain all select calls below inside the top module
stat stat
select -assert-count 1 t:BUFG select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE select -assert-count 1 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D select -assert-count 2 t:IBUF
select -assert-count 1 t:OBUF
select -assert-none t:BUFG t:FDRE t:IBUF t:OBUF %% t:* %D
design -load read design -load read
hierarchy -top dffe hierarchy -top dffe
...@@ -20,5 +22,7 @@ cd dffe # Constrain all select calls below inside the top module ...@@ -20,5 +22,7 @@ cd dffe # Constrain all select calls below inside the top module
stat stat
select -assert-count 1 t:BUFG select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE select -assert-count 1 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D select -assert-count 3 t:IBUF
select -assert-count 1 t:OBUF
select -assert-none t:BUFG t:FDRE t:IBUF t:OBUF %% t:* %D
architecture/synth_xilinx/synth_xilinx_arch_xcup.ys
...@@ -9,7 +9,9 @@ cd dff # Constrain all select calls below inside the top module ...@@ -9,7 +9,9 @@ cd dff # Constrain all select calls below inside the top module
stat stat
select -assert-count 1 t:BUFG select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE select -assert-count 1 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D select -assert-count 2 t:IBUF
select -assert-count 1 t:OBUF
select -assert-none t:BUFG t:FDRE t:IBUF t:OBUF %% t:* %D
design -load read design -load read
hierarchy -top dffe hierarchy -top dffe
...@@ -20,5 +22,7 @@ cd dffe # Constrain all select calls below inside the top module ...@@ -20,5 +22,7 @@ cd dffe # Constrain all select calls below inside the top module
stat stat
select -assert-count 1 t:BUFG select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE select -assert-count 1 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D select -assert-count 3 t:IBUF
select -assert-count 1 t:OBUF
select -assert-none t:BUFG t:FDRE t:IBUF t:OBUF %% t:* %D
architecture/synth_xilinx/synth_xilinx_blif.ys
...@@ -9,7 +9,9 @@ cd dff # Constrain all select calls below inside the top module ...@@ -9,7 +9,9 @@ cd dff # Constrain all select calls below inside the top module
stat stat
select -assert-count 1 t:BUFG select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE select -assert-count 1 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D select -assert-count 2 t:IBUF
select -assert-count 1 t:OBUF
select -assert-none t:BUFG t:FDRE t:IBUF t:OBUF %% t:* %D
design -load read design -load read
hierarchy -top dffe hierarchy -top dffe
...@@ -20,5 +22,7 @@ cd dffe # Constrain all select calls below inside the top module ...@@ -20,5 +22,7 @@ cd dffe # Constrain all select calls below inside the top module
stat stat
select -assert-count 1 t:BUFG select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE select -assert-count 1 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D select -assert-count 3 t:IBUF
select -assert-count 1 t:OBUF
select -assert-none t:BUFG t:FDRE t:IBUF t:OBUF %% t:* %D
architecture/synth_xilinx/synth_xilinx_dsp.ys
...@@ -3,7 +3,7 @@ design -save read ...@@ -3,7 +3,7 @@ design -save read
hierarchy -top simd hierarchy -top simd
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 simd # Constrain all select calls below inside the top module cd simd # Constrain all select calls below inside the top module
stat stat
......
architecture/synth_xilinx/synth_xilinx_edif.ys
...@@ -9,7 +9,9 @@ cd dff # Constrain all select calls below inside the top module ...@@ -9,7 +9,9 @@ cd dff # Constrain all select calls below inside the top module
stat stat
select -assert-count 1 t:BUFG select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE select -assert-count 1 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D select -assert-count 2 t:IBUF
select -assert-count 1 t:OBUF
select -assert-none t:BUFG t:FDRE t:IBUF t:OBUF %% t:* %D
design -load read design -load read
hierarchy -top dffe hierarchy -top dffe
...@@ -20,5 +22,7 @@ cd dffe # Constrain all select calls below inside the top module ...@@ -20,5 +22,7 @@ cd dffe # Constrain all select calls below inside the top module
stat stat
select -assert-count 1 t:BUFG select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE select -assert-count 1 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D select -assert-count 3 t:IBUF
select -assert-count 1 t:OBUF
select -assert-none t:BUFG t:FDRE t:IBUF t:OBUF %% t:* %D
architecture/synth_xilinx/synth_xilinx_flatten.ys
...@@ -9,7 +9,9 @@ cd dff # Constrain all select calls below inside the top module ...@@ -9,7 +9,9 @@ cd dff # Constrain all select calls below inside the top module
stat stat
select -assert-count 1 t:BUFG select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE select -assert-count 1 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D select -assert-count 2 t:IBUF
select -assert-count 1 t:OBUF
select -assert-none t:BUFG t:FDRE t:IBUF t:OBUF %% t:* %D
design -load read design -load read
hierarchy -top dffe hierarchy -top dffe
...@@ -20,5 +22,7 @@ cd dffe # Constrain all select calls below inside the top module ...@@ -20,5 +22,7 @@ cd dffe # Constrain all select calls below inside the top module
stat stat
select -assert-count 1 t:BUFG select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE select -assert-count 1 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D select -assert-count 3 t:IBUF
select -assert-count 1 t:OBUF
select -assert-none t:BUFG t:FDRE t:IBUF t:OBUF %% t:* %D
architecture/synth_xilinx/synth_xilinx_flatten_before_abc.ys
...@@ -9,7 +9,9 @@ cd dff # Constrain all select calls below inside the top module ...@@ -9,7 +9,9 @@ cd dff # Constrain all select calls below inside the top module
stat stat
select -assert-count 1 t:BUFG select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE select -assert-count 1 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D select -assert-count 2 t:IBUF
select -assert-count 1 t:OBUF
select -assert-none t:BUFG t:FDRE t:IBUF t:OBUF %% t:* %D
design -load read design -load read
hierarchy -top dffe hierarchy -top dffe
...@@ -20,5 +22,7 @@ cd dffe # Constrain all select calls below inside the top module ...@@ -20,5 +22,7 @@ cd dffe # Constrain all select calls below inside the top module
stat stat
select -assert-count 1 t:BUFG select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE select -assert-count 1 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D select -assert-count 3 t:IBUF
select -assert-count 1 t:OBUF
select -assert-none t:BUFG t:FDRE t:IBUF t:OBUF %% t:* %D
architecture/synth_xilinx/synth_xilinx_iopad.ys
...@@ -3,7 +3,7 @@ design -save read ...@@ -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 -iopad # equivalency check equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # 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
stat stat
...@@ -16,7 +16,7 @@ select -assert-none t:BUFG t:FDRE t:IBUF t:OBUF %% t:* %D ...@@ -16,7 +16,7 @@ select -assert-none t:BUFG t:FDRE t:IBUF t:OBUF %% 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 -iopad # equivalency check equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # 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
stat stat
......
architecture/synth_xilinx/synth_xilinx_nobram.ys
...@@ -4,7 +4,7 @@ design -save read ...@@ -4,7 +4,7 @@ design -save read
hierarchy -top top hierarchy -top top
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
...@@ -23,7 +23,7 @@ design -load read ...@@ -23,7 +23,7 @@ design -load read
hierarchy -top top hierarchy -top top
proc proc
memory -nomap memory -nomap
equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -nobram equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -nobram -noiopad
memory memory
opt -full opt -full
......
architecture/synth_xilinx/synth_xilinx_nocarry.ys
...@@ -3,7 +3,7 @@ design -save read ...@@ -3,7 +3,7 @@ design -save read
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
stat stat
...@@ -17,7 +17,7 @@ select -assert-none t:LUT2 t:LUT4 t:LUT6 t:MUXCY t:XORCY %% t:* %D ...@@ -17,7 +17,7 @@ select -assert-none t:LUT2 t:LUT4 t:LUT6 t:MUXCY t:XORCY %% t:* %D
design -load read design -load read
hierarchy -top top hierarchy -top top
proc proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -nocarry # equivalency check equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -nocarry -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
stat stat
......
architecture/synth_xilinx/synth_xilinx_noclkbuf.ys
...@@ -9,7 +9,9 @@ cd dff # Constrain all select calls below inside the top module ...@@ -9,7 +9,9 @@ cd dff # Constrain all select calls below inside the top module
stat stat
select -assert-count 1 t:BUFG select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE select -assert-count 1 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D select -assert-count 2 t:IBUF
select -assert-count 1 t:OBUF
select -assert-none t:BUFG t:FDRE t:IBUF t:OBUF %% t:* %D
design -load read design -load read
hierarchy -top dff hierarchy -top dff
...@@ -19,4 +21,6 @@ design -load postopt # load the post-opt design (otherwise equiv_opt loads the p ...@@ -19,4 +21,6 @@ design -load postopt # load the post-opt design (otherwise equiv_opt loads the p
cd dff # Constrain all select calls below inside the top module cd dff # Constrain all select calls below inside the top module
stat stat
select -assert-count 1 t:FDRE select -assert-count 1 t:FDRE
select -assert-none t:FDRE %% t:* %D select -assert-count 2 t:IBUF
select -assert-count 1 t:OBUF
select -assert-none t:FDRE t:IBUF t:OBUF %% t:* %D
architecture/synth_xilinx/synth_xilinx_nodram.ys
...@@ -4,7 +4,7 @@ design -save read ...@@ -4,7 +4,7 @@ design -save read
hierarchy -top top hierarchy -top top
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
...@@ -23,7 +23,7 @@ design -load read ...@@ -23,7 +23,7 @@ design -load read
hierarchy -top top hierarchy -top top
proc proc
memory -nomap memory -nomap
equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -nodram equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -nodram -noiopad
memory memory
opt -full opt -full
......
architecture/synth_xilinx/synth_xilinx_nodsp.ys
...@@ -3,7 +3,7 @@ design -save read ...@@ -3,7 +3,7 @@ design -save read
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
stat stat
...@@ -13,7 +13,7 @@ select -assert-none t:DSP48E1 %% t:* %D ...@@ -13,7 +13,7 @@ select -assert-none t:DSP48E1 %% t:* %D
design -load read design -load read
hierarchy -top top hierarchy -top top
proc proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -nodsp # equivalency check equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -nodsp -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
stat stat
......
architecture/synth_xilinx/synth_xilinx_nosrl.ys
...@@ -3,8 +3,8 @@ design -save read ...@@ -3,8 +3,8 @@ design -save read
hierarchy -top xilinx_srl_static_test hierarchy -top xilinx_srl_static_test
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
equiv_opt -map +/xilinx/cells_sim.v synth_xilinx # equivalency check equiv_opt -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 xilinx_srl_static_test # Constrain all select calls below inside the top module cd xilinx_srl_static_test # Constrain all select calls below inside the top module
stat stat
...@@ -15,7 +15,7 @@ select -assert-none t:BUFG t:SRL16E %% t:* %D ...@@ -15,7 +15,7 @@ select -assert-none t:BUFG t:SRL16E %% t:* %D
design -load read design -load read
hierarchy -top xilinx_srl_static_test hierarchy -top xilinx_srl_static_test
proc proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -nosrl # equivalency check equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -nosrl -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 xilinx_srl_static_test # Constrain all select calls below inside the top module cd xilinx_srl_static_test # Constrain all select calls below inside the top module
stat stat
......
architecture/synth_xilinx/synth_xilinx_nowidelut.ys
...@@ -3,7 +3,7 @@ design -save read ...@@ -3,7 +3,7 @@ design -save read
hierarchy -top top hierarchy -top top
proc proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -nodsp # equivalency check equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -nodsp -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
stat stat
...@@ -20,7 +20,7 @@ select -assert-none t:LUT2 t:LUT3 t:LUT4 t:LUT5 t:LUT6 t:MUXCY t:MUXF7 t:XORCY % ...@@ -20,7 +20,7 @@ select -assert-none t:LUT2 t:LUT3 t:LUT4 t:LUT5 t:LUT6 t:MUXCY t:MUXF7 t:XORCY %
design -load read design -load read
hierarchy -top top hierarchy -top top
proc proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -nodsp -nowidelut # equivalency check equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -nodsp -nowidelut -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
stat stat
......
architecture/synth_xilinx/synth_xilinx_nowidelut_abc9.ys
read_verilog ../top_dsp.v read_verilog ../top_dsp.v
hierarchy -top top hierarchy -top top
proc proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -nodsp -nowidelut -abc9 # equivalency check equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -nodsp -nowidelut -abc9 -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
stat stat
select -assert-count 3 t:CARRY4 select -assert-count 3 t:CARRY4
select -assert-count 12 t:LUT2 select -assert-count 11 t:LUT2
select -assert-count 1 t:LUT3 select -assert-count 1 t:LUT3
select -assert-count 8 t:LUT4 select -assert-count 8 t:LUT4
select -assert-count 21 t:LUT5 select -assert-count 20 t:LUT5
select -assert-count 16 t:LUT6 select -assert-count 17 t:LUT6
select -assert-none t:CARRY4 t:LUT2 t:LUT3 t:LUT4 t:LUT5 t:LUT6 %% t:* %D select -assert-none t:CARRY4 t:LUT2 t:LUT3 t:LUT4 t:LUT5 t:LUT6 %% t:* %D
architecture/synth_xilinx/synth_xilinx_retime.ys
...@@ -9,7 +9,9 @@ cd dff # Constrain all select calls below inside the top module ...@@ -9,7 +9,9 @@ cd dff # Constrain all select calls below inside the top module
stat stat
select -assert-count 1 t:BUFG select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE select -assert-count 1 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D select -assert-count 2 t:IBUF
select -assert-count 1 t:OBUF
select -assert-none t:BUFG t:FDRE t:IBUF t:OBUF %% t:* %D
design -load read design -load read
hierarchy -top dffe hierarchy -top dffe
...@@ -20,5 +22,7 @@ cd dffe # Constrain all select calls below inside the top module ...@@ -20,5 +22,7 @@ cd dffe # Constrain all select calls below inside the top module
stat stat
select -assert-count 1 t:BUFG select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE select -assert-count 1 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D select -assert-count 3 t:IBUF
select -assert-count 1 t:OBUF
select -assert-none t:BUFG t:FDRE t:IBUF t:OBUF %% t:* %D
architecture/synth_xilinx/synth_xilinx_run.ys
...@@ -9,7 +9,9 @@ cd dff # Constrain all select calls below inside the top module ...@@ -9,7 +9,9 @@ cd dff # Constrain all select calls below inside the top module
stat stat
select -assert-count 1 t:BUFG select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE select -assert-count 1 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D select -assert-count 2 t:IBUF
select -assert-count 1 t:OBUF
select -assert-none t:BUFG t:FDRE t:IBUF t:OBUF %% t:* %D
design -load read design -load read
hierarchy -top dffe hierarchy -top dffe
...@@ -20,5 +22,7 @@ cd dffe # Constrain all select calls below inside the top module ...@@ -20,5 +22,7 @@ cd dffe # Constrain all select calls below inside the top module
stat stat
select -assert-count 1 t:BUFG select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE select -assert-count 1 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D select -assert-count 3 t:IBUF
select -assert-count 1 t:OBUF
select -assert-none t:BUFG t:FDRE t:IBUF t:OBUF %% t:* %D
architecture/synth_xilinx/synth_xilinx_top.ys
...@@ -9,7 +9,9 @@ cd dff # Constrain all select calls below inside the top module ...@@ -9,7 +9,9 @@ cd dff # Constrain all select calls below inside the top module
stat stat
select -assert-count 1 t:BUFG select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE select -assert-count 1 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D select -assert-count 2 t:IBUF
select -assert-count 1 t:OBUF
select -assert-none t:BUFG t:FDRE t:IBUF t:OBUF %% t:* %D
design -load read design -load read
hierarchy -top dffe hierarchy -top dffe
...@@ -20,5 +22,7 @@ cd dffe # Constrain all select calls below inside the top module ...@@ -20,5 +22,7 @@ cd dffe # Constrain all select calls below inside the top module
stat stat
select -assert-count 1 t:BUFG select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE select -assert-count 1 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D select -assert-count 3 t:IBUF
select -assert-count 1 t:OBUF
select -assert-none t:BUFG t:FDRE t:IBUF t:OBUF %% t:* %D
architecture/synth_xilinx/synth_xilinx_vpr.ys
...@@ -9,7 +9,9 @@ cd dff # Constrain all select calls below inside the top module ...@@ -9,7 +9,9 @@ cd dff # Constrain all select calls below inside the top module
stat stat
select -assert-count 1 t:BUFG select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE select -assert-count 1 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D select -assert-count 2 t:IBUF
select -assert-count 1 t:OBUF
select -assert-none t:BUFG t:FDRE t:IBUF t:OBUF %% t:* %D
design -load read design -load read
hierarchy -top dffe hierarchy -top dffe
...@@ -20,5 +22,7 @@ cd dffe # Constrain all select calls below inside the top module ...@@ -20,5 +22,7 @@ cd dffe # Constrain all select calls below inside the top module
stat stat
select -assert-count 1 t:BUFG select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE select -assert-count 1 t:FDRE
select -assert-none t:BUFG t:FDRE %% t:* %D select -assert-count 3 t:IBUF
select -assert-count 1 t:OBUF
select -assert-none t:BUFG t:FDRE t:IBUF t:OBUF %% t:* %D
architecture/synth_xilinx/synth_xilinx_widemux.ys
...@@ -3,7 +3,7 @@ design -save read ...@@ -3,7 +3,7 @@ design -save read
hierarchy -top mux16 hierarchy -top mux16
proc proc
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -widemux 2 # equivalency check equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -widemux 2 -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
stat stat
...@@ -14,7 +14,7 @@ select -assert-none t:MUXF7 t:MUXF8 %% t:* %D ...@@ -14,7 +14,7 @@ select -assert-none t:MUXF7 t:MUXF8 %% 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 -widemux 3 # equivalency check equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -widemux 3 -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
stat stat
...@@ -26,7 +26,7 @@ select -assert-none t:LUT6 t:MUXF7 t:MUXF8 %% t:* %D ...@@ -26,7 +26,7 @@ select -assert-none t:LUT6 t:MUXF7 t:MUXF8 %% 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 -widemux 5 # equivalency check equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -widemux 5 -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
stat stat
...@@ -38,7 +38,7 @@ select -assert-none t:LUT6 t:MUXF7 t:MUXF8 %% t:* %D ...@@ -38,7 +38,7 @@ select -assert-none t:LUT6 t:MUXF7 t:MUXF8 %% 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 -widemux 9 # equivalency check equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -widemux 9 -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
stat stat
......
architecture/xilinx_ug901_synthesis_examples/xilinx_ug901_asym_ram_sdp_read_wider.ys
...@@ -2,7 +2,7 @@ read_verilog ../asym_ram_sdp_read_wider.v ...@@ -2,7 +2,7 @@ read_verilog ../asym_ram_sdp_read_wider.v
hierarchy -top asym_ram_sdp_read_wider hierarchy -top asym_ram_sdp_read_wider
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
......
architecture/xilinx_ug901_synthesis_examples/xilinx_ug901_asym_ram_sdp_write_wider.ys
...@@ -2,7 +2,7 @@ read_verilog ../asym_ram_sdp_write_wider.v ...@@ -2,7 +2,7 @@ read_verilog ../asym_ram_sdp_write_wider.v
hierarchy -top asym_ram_sdp_write_wider hierarchy -top asym_ram_sdp_write_wider
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
......
architecture/xilinx_ug901_synthesis_examples/xilinx_ug901_asym_ram_tdp_read_first.ys
...@@ -2,7 +2,7 @@ read_verilog ../asym_ram_tdp_read_first.v ...@@ -2,7 +2,7 @@ read_verilog ../asym_ram_tdp_read_first.v
hierarchy -top asym_ram_tdp_read_first hierarchy -top asym_ram_tdp_read_first
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
......
architecture/xilinx_ug901_synthesis_examples/xilinx_ug901_asym_ram_tdp_write_first.ys
...@@ -2,7 +2,7 @@ read_verilog ../asym_ram_tdp_write_first.v ...@@ -2,7 +2,7 @@ read_verilog ../asym_ram_tdp_write_first.v
hierarchy -top asym_ram_tdp_write_first hierarchy -top asym_ram_tdp_write_first
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
......
architecture/xilinx_ug901_synthesis_examples/xilinx_ug901_bytewrite_ram_1b.ys
...@@ -2,7 +2,7 @@ read_verilog ../bytewrite_ram_1b.v ...@@ -2,7 +2,7 @@ read_verilog ../bytewrite_ram_1b.v
hierarchy -top bytewrite_ram_1b hierarchy -top bytewrite_ram_1b
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
......
architecture/xilinx_ug901_synthesis_examples/xilinx_ug901_bytewrite_tdp_ram_nc.ys
...@@ -2,7 +2,7 @@ read_verilog ../bytewrite_tdp_ram_nc.v ...@@ -2,7 +2,7 @@ read_verilog ../bytewrite_tdp_ram_nc.v
hierarchy -top bytewrite_tdp_ram_nc hierarchy -top bytewrite_tdp_ram_nc
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
......
architecture/xilinx_ug901_synthesis_examples/xilinx_ug901_bytewrite_tdp_ram_readfirst2.ys
...@@ -2,7 +2,7 @@ read_verilog ../bytewrite_tdp_ram_readfirst2.v ...@@ -2,7 +2,7 @@ read_verilog ../bytewrite_tdp_ram_readfirst2.v
hierarchy -top bytewrite_tdp_ram_readfirst2 hierarchy -top bytewrite_tdp_ram_readfirst2
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
......
architecture/xilinx_ug901_synthesis_examples/xilinx_ug901_bytewrite_tdp_ram_rf.ys
...@@ -2,7 +2,7 @@ read_verilog ../bytewrite_tdp_ram_rf.v ...@@ -2,7 +2,7 @@ read_verilog ../bytewrite_tdp_ram_rf.v
hierarchy -top bytewrite_tdp_ram_rf hierarchy -top bytewrite_tdp_ram_rf
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
......
architecture/xilinx_ug901_synthesis_examples/xilinx_ug901_bytewrite_tdp_ram_wf.ys
...@@ -2,7 +2,7 @@ read_verilog ../bytewrite_tdp_ram_wf.v ...@@ -2,7 +2,7 @@ read_verilog ../bytewrite_tdp_ram_wf.v
hierarchy -top bytewrite_tdp_ram_wf hierarchy -top bytewrite_tdp_ram_wf
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
......
architecture/xilinx_ug901_synthesis_examples/xilinx_ug901_cmacc.ys
...@@ -2,7 +2,7 @@ read_verilog ../cmacc.v ...@@ -2,7 +2,7 @@ read_verilog ../cmacc.v
hierarchy -top cmacc hierarchy -top cmacc
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 cmacc cd cmacc
......
architecture/xilinx_ug901_synthesis_examples/xilinx_ug901_cmult.ys
...@@ -2,7 +2,7 @@ read_verilog ../cmult.v ...@@ -2,7 +2,7 @@ read_verilog ../cmult.v
hierarchy -top cmult hierarchy -top cmult
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
......
architecture/xilinx_ug901_synthesis_examples/xilinx_ug901_dynamic_shift_registers_1.ys
...@@ -3,8 +3,8 @@ hierarchy -top dynamic_shift_register_1 ...@@ -3,8 +3,8 @@ hierarchy -top dynamic_shift_register_1
proc proc
flatten flatten
#ERROR: Found 1 unproven $equiv cells in 'equiv_status -assert'. #ERROR: Found 1 unproven $equiv cells in 'equiv_status -assert'.
#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
equiv_opt -map +/xilinx/cells_sim.v synth_xilinx # equivalency check equiv_opt -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 dynamic_shift_register_1 # Constrain all select calls below inside the top module cd dynamic_shift_register_1 # Constrain all select calls below inside the top module
......
architecture/xilinx_ug901_synthesis_examples/xilinx_ug901_dynpreaddmultadd.ys
...@@ -2,7 +2,7 @@ read_verilog ../dynpreaddmultadd.v ...@@ -2,7 +2,7 @@ read_verilog ../dynpreaddmultadd.v
hierarchy -top dynpreaddmultadd hierarchy -top dynpreaddmultadd
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
......
architecture/xilinx_ug901_synthesis_examples/xilinx_ug901_fsm_1.ys
...@@ -2,7 +2,7 @@ read_verilog ../fsm_1.v ...@@ -2,7 +2,7 @@ read_verilog ../fsm_1.v
hierarchy -top fsm_1 hierarchy -top fsm_1
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
......
architecture/xilinx_ug901_synthesis_examples/xilinx_ug901_latches.ys
...@@ -2,7 +2,7 @@ read_verilog ../latches.v ...@@ -2,7 +2,7 @@ read_verilog ../latches.v
proc proc
hierarchy -top latches hierarchy -top latches
flatten flatten
synth_xilinx synth_xilinx -noiopad
#Vivado synthesizes 1 BUFG, 8 LDCE. #Vivado synthesizes 1 BUFG, 8 LDCE.
select -assert-count 2 t:LUT2 select -assert-count 2 t:LUT2
select -assert-count 1 t:LDCE select -assert-count 1 t:LDCE
......
architecture/xilinx_ug901_synthesis_examples/xilinx_ug901_macc.ys
...@@ -2,7 +2,7 @@ read_verilog ../macc.v ...@@ -2,7 +2,7 @@ read_verilog ../macc.v
hierarchy -top macc hierarchy -top macc
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 macc cd macc
......
architecture/xilinx_ug901_synthesis_examples/xilinx_ug901_mult_unsigned.ys
...@@ -2,7 +2,7 @@ read_verilog ../mult_unsigned.v ...@@ -2,7 +2,7 @@ read_verilog ../mult_unsigned.v
hierarchy -top mult_unsigned hierarchy -top mult_unsigned
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
......
architecture/xilinx_ug901_synthesis_examples/xilinx_ug901_presubmult.ys
...@@ -2,7 +2,7 @@ read_verilog ../presubmult.v ...@@ -2,7 +2,7 @@ read_verilog ../presubmult.v
hierarchy -top presubmult hierarchy -top presubmult
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 presubmult cd presubmult
......
architecture/xilinx_ug901_synthesis_examples/xilinx_ug901_ram_simple_dual_one_clock.ys
...@@ -2,7 +2,7 @@ read_verilog ../ram_simple_dual_one_clock.v ...@@ -2,7 +2,7 @@ read_verilog ../ram_simple_dual_one_clock.v
hierarchy -top simple_dual_one_clock hierarchy -top simple_dual_one_clock
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
......
architecture/xilinx_ug901_synthesis_examples/xilinx_ug901_ram_simple_dual_two_clocks.ys
...@@ -2,7 +2,7 @@ read_verilog ../ram_simple_dual_two_clocks.v ...@@ -2,7 +2,7 @@ read_verilog ../ram_simple_dual_two_clocks.v
hierarchy -top simple_dual_two_clocks hierarchy -top simple_dual_two_clocks
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
......
architecture/xilinx_ug901_synthesis_examples/xilinx_ug901_rams_dist.ys
...@@ -2,7 +2,7 @@ read_verilog ../rams_dist.v ...@@ -2,7 +2,7 @@ read_verilog ../rams_dist.v
hierarchy -top rams_dist hierarchy -top rams_dist
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
......
architecture/xilinx_ug901_synthesis_examples/xilinx_ug901_rams_init_file.ys
...@@ -2,7 +2,7 @@ read_verilog ../rams_init_file.v ...@@ -2,7 +2,7 @@ read_verilog ../rams_init_file.v
hierarchy -top rams_init_file hierarchy -top rams_init_file
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
......
architecture/xilinx_ug901_synthesis_examples/xilinx_ug901_rams_pipeline.ys
...@@ -2,7 +2,7 @@ read_verilog ../rams_pipeline.v ...@@ -2,7 +2,7 @@ read_verilog ../rams_pipeline.v
hierarchy -top rams_pipeline hierarchy -top rams_pipeline
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
...@@ -14,9 +14,15 @@ miter -equiv -flatten -make_assert -make_outputs gold gate miter ...@@ -14,9 +14,15 @@ miter -equiv -flatten -make_assert -make_outputs gold gate miter
design -load postopt design -load postopt
cd rams_pipeline cd rams_pipeline
stat stat
#Vivado synthesizes 1 RAMB18E1. #Vivado synthesizes 1 RAMB18E1.
select -assert-count 2 t:BUFG select -assert-count 2 t:BUFG
select -assert-count 32 t:FDRE select -assert-count 302 t:FDRE
select -assert-count 2 t:RAMB18E1 select -assert-count 25 t:LUT2
select -assert-count 5 t:LUT3
select -assert-count 42 t:LUT4
select -assert-count 21 t:LUT5
select -assert-count 58 t:LUT6
select -assert-count 2 t:MUXF7
select -assert-count 256 t:RAM128X1D
select -assert-none t:BUFG t:FDRE t:RAMB18E1 %% t:* %D select -assert-none t:BUFG t:FDRE t:LUT2 t:LUT3 t:LUT4 t:LUT5 t:LUT6 t:MUXF7 t:RAM128X1D %% t:* %D
architecture/xilinx_ug901_synthesis_examples/xilinx_ug901_rams_sp_nc.ys
...@@ -2,7 +2,7 @@ read_verilog ../rams_sp_nc.v ...@@ -2,7 +2,7 @@ read_verilog ../rams_sp_nc.v
hierarchy -top rams_sp_nc hierarchy -top rams_sp_nc
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
......
architecture/xilinx_ug901_synthesis_examples/xilinx_ug901_rams_sp_rf.ys
...@@ -2,7 +2,7 @@ read_verilog ../rams_sp_rf.v ...@@ -2,7 +2,7 @@ read_verilog ../rams_sp_rf.v
hierarchy -top rams_sp_rf hierarchy -top rams_sp_rf
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
......
architecture/xilinx_ug901_synthesis_examples/xilinx_ug901_rams_sp_rf_rst.ys
...@@ -2,7 +2,7 @@ read_verilog ../rams_sp_rf_rst.v ...@@ -2,7 +2,7 @@ read_verilog ../rams_sp_rf_rst.v
hierarchy -top rams_sp_rf_rst hierarchy -top rams_sp_rf_rst
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
......
architecture/xilinx_ug901_synthesis_examples/xilinx_ug901_rams_sp_rom.ys
...@@ -2,7 +2,7 @@ read_verilog ../rams_sp_rom.v ...@@ -2,7 +2,7 @@ read_verilog ../rams_sp_rom.v
hierarchy -top rams_sp_rom hierarchy -top rams_sp_rom
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
......
architecture/xilinx_ug901_synthesis_examples/xilinx_ug901_rams_sp_rom_1.ys
...@@ -2,7 +2,7 @@ read_verilog ../rams_sp_rom_1.v ...@@ -2,7 +2,7 @@ read_verilog ../rams_sp_rom_1.v
hierarchy -top rams_sp_rom_1 hierarchy -top rams_sp_rom_1
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
......
architecture/xilinx_ug901_synthesis_examples/xilinx_ug901_rams_sp_wf.ys
...@@ -2,7 +2,7 @@ read_verilog ../rams_sp_wf.v ...@@ -2,7 +2,7 @@ read_verilog ../rams_sp_wf.v
hierarchy -top rams_sp_wf hierarchy -top rams_sp_wf
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
......
architecture/xilinx_ug901_synthesis_examples/xilinx_ug901_rams_tdp_rf_rf.ys
...@@ -2,7 +2,7 @@ read_verilog ../rams_tdp_rf_rf.v ...@@ -2,7 +2,7 @@ read_verilog ../rams_tdp_rf_rf.v
hierarchy -top rams_tdp_rf_rf hierarchy -top rams_tdp_rf_rf
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
......
architecture/xilinx_ug901_synthesis_examples/xilinx_ug901_registers_1.ys
...@@ -2,7 +2,7 @@ read_verilog ../registers_1.v ...@@ -2,7 +2,7 @@ read_verilog ../registers_1.v
hierarchy -top registers_1 hierarchy -top registers_1
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 registers_1 # Constrain all select calls below inside the top module cd registers_1 # Constrain all select calls below inside the top module
#Vivado synthesizes 1 BUFG, 8 FDRE. #Vivado synthesizes 1 BUFG, 8 FDRE.
......
architecture/xilinx_ug901_synthesis_examples/xilinx_ug901_sfir_shifter.ys
...@@ -3,8 +3,8 @@ hierarchy -top sfir_shifter ...@@ -3,8 +3,8 @@ hierarchy -top sfir_shifter
proc proc
flatten flatten
#ERROR: Found 32 unproven $equiv cells in 'equiv_status -assert'. #ERROR: Found 32 unproven $equiv cells in 'equiv_status -assert'.
#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
equiv_opt -map +/xilinx/cells_sim.v synth_xilinx # equivalency check equiv_opt -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 sfir_shifter cd sfir_shifter
......
architecture/xilinx_ug901_synthesis_examples/xilinx_ug901_shift_registers_0.ys
...@@ -3,8 +3,8 @@ hierarchy -top shift_registers_0 ...@@ -3,8 +3,8 @@ hierarchy -top shift_registers_0
proc proc
flatten flatten
#ERROR: Found 2 unproven $equiv cells in 'equiv_status -assert'. #ERROR: Found 2 unproven $equiv cells in 'equiv_status -assert'.
#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
equiv_opt -map +/xilinx/cells_sim.v synth_xilinx # equivalency check equiv_opt -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 shift_registers_0 # Constrain all select calls below inside the top module cd shift_registers_0 # Constrain all select calls below inside the top module
......
architecture/xilinx_ug901_synthesis_examples/xilinx_ug901_shift_registers_1.ys
...@@ -3,8 +3,8 @@ hierarchy -top shift_registers_1 ...@@ -3,8 +3,8 @@ hierarchy -top shift_registers_1
proc proc
flatten flatten
#ERROR: Found 2 unproven $equiv cells in 'equiv_status -assert'. #ERROR: Found 2 unproven $equiv cells in 'equiv_status -assert'.
#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
equiv_opt -map +/xilinx/cells_sim.v synth_xilinx # equivalency check equiv_opt -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 shift_registers_1 # Constrain all select calls below inside the top module cd shift_registers_1 # Constrain all select calls below inside the top module
......
architecture/xilinx_ug901_synthesis_examples/xilinx_ug901_squarediffmacc.ys
...@@ -2,7 +2,7 @@ read_verilog ../squarediffmacc.v ...@@ -2,7 +2,7 @@ read_verilog ../squarediffmacc.v
hierarchy -top squarediffmacc hierarchy -top squarediffmacc
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 squarediffmacc cd squarediffmacc
......
architecture/xilinx_ug901_synthesis_examples/xilinx_ug901_squarediffmult.ys
...@@ -2,7 +2,7 @@ read_verilog ../squarediffmult.v ...@@ -2,7 +2,7 @@ read_verilog ../squarediffmult.v
hierarchy -top squarediffmult hierarchy -top squarediffmult
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
......
architecture/xilinx_ug901_synthesis_examples/xilinx_ug901_top_mux.ys
...@@ -2,7 +2,7 @@ read_verilog ../top_mux.v ...@@ -2,7 +2,7 @@ read_verilog ../top_mux.v
hierarchy -top mux4 hierarchy -top mux4
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 mux4 cd mux4
......
architecture/xilinx_ug901_synthesis_examples/xilinx_ug901_tristates_1.ys
...@@ -8,6 +8,6 @@ equiv_opt -assert -map +/xilinx/cells_sim.v -map +/simcells.v synth_xilinx # equ ...@@ -8,6 +8,6 @@ equiv_opt -assert -map +/xilinx/cells_sim.v -map +/simcells.v synth_xilinx # equ
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 tristates_1 # Constrain all select calls below inside the top module cd tristates_1 # Constrain all select calls below inside the top module
#Vivado synthesizes 3 IBUF, 1 OBUFT. #Vivado synthesizes 3 IBUF, 1 OBUFT.
select -assert-count 1 t:INV select -assert-count 2 t:IBUF
select -assert-count 1 t:$_TBUF_ select -assert-count 1 t:OBUFT
select -assert-none t:INV t:$_TBUF_ %% t:* %D select -assert-none t:IBUF t:OBUFT %% t:* %D
architecture/xilinx_ug901_synthesis_examples/xilinx_ug901_tristates_2.ys
...@@ -8,6 +8,6 @@ equiv_opt -assert -map +/xilinx/cells_sim.v -map +/simcells.v synth_xilinx # equ ...@@ -8,6 +8,6 @@ equiv_opt -assert -map +/xilinx/cells_sim.v -map +/simcells.v synth_xilinx # equ
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 tristates_2 # Constrain all select calls below inside the top module cd tristates_2 # Constrain all select calls below inside the top module
#Vivado synthesizes 3 IBUF, 1 OBUFT. #Vivado synthesizes 3 IBUF, 1 OBUFT.
select -assert-count 1 t:INV select -assert-count 2 t:IBUF
select -assert-count 1 t:$_TBUF_ select -assert-count 1 t:OBUFT
select -assert-none t:INV t:$_TBUF_ %% t:* %D select -assert-none t:IBUF t:OBUFT %% t:* %D
architecture/xilinx_ug901_synthesis_examples/xilinx_ug901_xilinx_ultraram_single_port_no_change.ys
...@@ -2,7 +2,7 @@ read_verilog ../xilinx_ultraram_single_port_no_change.v ...@@ -2,7 +2,7 @@ read_verilog ../xilinx_ultraram_single_port_no_change.v
hierarchy -top xilinx_ultraram_single_port_no_change hierarchy -top xilinx_ultraram_single_port_no_change
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
......
architecture/xilinx_ug901_synthesis_examples/xilinx_ug901_xilinx_ultraram_single_port_read_first.ys
...@@ -2,7 +2,7 @@ read_verilog ../xilinx_ultraram_single_port_read_first.v ...@@ -2,7 +2,7 @@ read_verilog ../xilinx_ultraram_single_port_read_first.v
hierarchy -top xilinx_ultraram_single_port_read_first hierarchy -top xilinx_ultraram_single_port_read_first
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
......
architecture/xilinx_ug901_synthesis_examples/xilinx_ug901_xilinx_ultraram_single_port_write_first.ys
...@@ -2,7 +2,7 @@ read_verilog ../xilinx_ultraram_single_port_write_first.v ...@@ -2,7 +2,7 @@ read_verilog ../xilinx_ultraram_single_port_write_first.v
hierarchy -top xilinx_ultraram_single_port_write_first hierarchy -top xilinx_ultraram_single_port_write_first
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
......
misc/abc/abc_lut_liberty_fail.pat
ERROR: Got -lut and -liberty! This two options are exclusive. ERROR: Got -lut and -liberty! These two options are exclusive.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment