From: SergeyDegtyar Date: Tue, 10 Sep 2019 05:11:56 +0000 (+0300) Subject: Remove xilinx_ug901 tests (will be moved to yosys-tests) X-Git-Tag: working-ls180~990^2~26 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6331fa5b022b9e16f9392d9604a545f86dc13385;p=yosys.git Remove xilinx_ug901 tests (will be moved to yosys-tests) --- diff --git a/Makefile b/Makefile index 82af448da..6f5184596 100644 --- a/Makefile +++ b/Makefile @@ -716,7 +716,6 @@ test: $(TARGETS) $(EXTRA_TARGETS) +cd tests/ice40 && bash run-test.sh $(SEEDOPT) +cd tests/rpc && bash run-test.sh +cd tests/xilinx && bash run-test.sh $(SEEDOPT) - +cd tests/xilinx_ug901 && bash run-test.sh $(SEEDOPT) @echo "" @echo " Passed \"make test\"." @echo "" diff --git a/tests/xilinx_ug901/asym_ram_sdp_read_wider.v b/tests/xilinx_ug901/asym_ram_sdp_read_wider.v deleted file mode 100644 index 0716dffdc..000000000 --- a/tests/xilinx_ug901/asym_ram_sdp_read_wider.v +++ /dev/null @@ -1,74 +0,0 @@ -// Asymmetric port RAM -// Read Wider than Write. Read Statement in loop -//asym_ram_sdp_read_wider.v - -module asym_ram_sdp_read_wider (clkA, clkB, enaA, weA, enaB, addrA, addrB, diA, doB); -parameter WIDTHA = 4; -parameter SIZEA = 1024; -parameter ADDRWIDTHA = 10; - -parameter WIDTHB = 16; -parameter SIZEB = 256; -parameter ADDRWIDTHB = 8; -input clkA; -input clkB; -input weA; -input enaA, enaB; -input [ADDRWIDTHA-1:0] addrA; -input [ADDRWIDTHB-1:0] addrB; -input [WIDTHA-1:0] diA; -output [WIDTHB-1:0] doB; -`define max(a,b) {(a) > (b) ? (a) : (b)} -`define min(a,b) {(a) < (b) ? (a) : (b)} - -function integer log2; -input integer value; -reg [31:0] shifted; -integer res; -begin - if (value < 2) - log2 = value; - else - begin - shifted = value-1; - for (res=0; shifted>0; res=res+1) - shifted = shifted>>1; - log2 = res; - end -end -endfunction - -localparam maxSIZE = `max(SIZEA, SIZEB); -localparam maxWIDTH = `max(WIDTHA, WIDTHB); -localparam minWIDTH = `min(WIDTHA, WIDTHB); - -localparam RATIO = maxWIDTH / minWIDTH; -localparam log2RATIO = log2(RATIO); - -reg [minWIDTH-1:0] RAM [0:maxSIZE-1]; -reg [WIDTHB-1:0] readB; - -always @(posedge clkA) -begin - if (enaA) begin - if (weA) - RAM[addrA] <= diA; - end -end - - -always @(posedge clkB) -begin : ramread - integer i; - reg [log2RATIO-1:0] lsbaddr; - if (enaB) begin - for (i = 0; i < RATIO; i = i+1) begin - lsbaddr = i; - readB[(i+1)*minWIDTH-1 -: minWIDTH] <= RAM[{addrB, lsbaddr}]; - end - end -end -assign doB = readB; - -endmodule - diff --git a/tests/xilinx_ug901/asym_ram_sdp_read_wider.ys b/tests/xilinx_ug901/asym_ram_sdp_read_wider.ys deleted file mode 100644 index c63157cdf..000000000 --- a/tests/xilinx_ug901/asym_ram_sdp_read_wider.ys +++ /dev/null @@ -1,22 +0,0 @@ -read_verilog asym_ram_sdp_read_wider.v -hierarchy -top asym_ram_sdp_read_wider -proc -memory -nomap -equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -memory -opt -full - -# TODO -#equiv_opt -run prove: -assert null -miter -equiv -flatten -make_assert -make_outputs gold gate miter -#sat -verify -prove-asserts -tempinduct -show-inputs -show-outputs miter - -design -load postopt -cd asym_ram_sdp_read_wider -stat -#Vivado synthesizes 1 RAMB18E1. -select -assert-count 2 t:BUFG -select -assert-count 1 t:LUT2 -select -assert-count 4 t:RAMB18E1 - -select -assert-none t:BUFG t:LUT2 t:RAMB18E1 %% t:* %D diff --git a/tests/xilinx_ug901/asym_ram_sdp_write_wider.v b/tests/xilinx_ug901/asym_ram_sdp_write_wider.v deleted file mode 100644 index 22d12d2ce..000000000 --- a/tests/xilinx_ug901/asym_ram_sdp_write_wider.v +++ /dev/null @@ -1,75 +0,0 @@ -// Asymmetric port RAM -// Write wider than Read. Write Statement in a loop. -// asym_ram_sdp_write_wider.v - -module asym_ram_sdp_write_wider (clkA, clkB, weA, enaA, enaB, addrA, addrB, diA, doB); -parameter WIDTHB = 4; -//Default parameters were changed because of slow test -//parameter SIZEB = 1024; -//parameter ADDRWIDTHB = 10; -parameter SIZEB = 256; -parameter ADDRWIDTHB = 8; - -//parameter WIDTHA = 16; -parameter WIDTHA = 8; -parameter SIZEA = 256; -parameter ADDRWIDTHA = 8; -input clkA; -input clkB; -input weA; -input enaA, enaB; -input [ADDRWIDTHA-1:0] addrA; -input [ADDRWIDTHB-1:0] addrB; -input [WIDTHA-1:0] diA; -output [WIDTHB-1:0] doB; -`define max(a,b) {(a) > (b) ? (a) : (b)} -`define min(a,b) {(a) < (b) ? (a) : (b)} - -function integer log2; -input integer value; -reg [31:0] shifted; -integer res; -begin - if (value < 2) - log2 = value; - else - begin - shifted = value-1; - for (res=0; shifted>0; res=res+1) - shifted = shifted>>1; - log2 = res; - end -end -endfunction - -localparam maxSIZE = `max(SIZEA, SIZEB); -localparam maxWIDTH = `max(WIDTHA, WIDTHB); -localparam minWIDTH = `min(WIDTHA, WIDTHB); - -localparam RATIO = maxWIDTH / minWIDTH; -localparam log2RATIO = log2(RATIO); - -reg [minWIDTH-1:0] RAM [0:maxSIZE-1]; -reg [WIDTHB-1:0] readB; - -always @(posedge clkB) begin - if (enaB) begin - readB <= RAM[addrB]; - end -end -assign doB = readB; - -always @(posedge clkA) -begin : ramwrite - integer i; - reg [log2RATIO-1:0] lsbaddr; - for (i=0; i< RATIO; i= i+ 1) begin : write1 - lsbaddr = i; - if (enaA) begin - if (weA) - RAM[{addrA, lsbaddr}] <= diA[(i+1)*minWIDTH-1 -: minWIDTH]; - end - end -end - -endmodule diff --git a/tests/xilinx_ug901/asym_ram_sdp_write_wider.ys b/tests/xilinx_ug901/asym_ram_sdp_write_wider.ys deleted file mode 100644 index 229d98df6..000000000 --- a/tests/xilinx_ug901/asym_ram_sdp_write_wider.ys +++ /dev/null @@ -1,31 +0,0 @@ -read_verilog asym_ram_sdp_write_wider.v -hierarchy -top asym_ram_sdp_write_wider -proc -memory -nomap -equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -memory -opt -full - -# TODO -#equiv_opt -run prove: -assert null -miter -equiv -flatten -make_assert -make_outputs gold gate miter -#sat -verify -prove-asserts -tempinduct -show-inputs -show-outputs miter - -design -load postopt -cd asym_ram_sdp_write_wider -stat -#Vivado synthesizes 1 RAMB18E1. -select -assert-count 2 t:BUFG -select -assert-count 1028 t:FDRE -select -assert-count 170 t:LUT2 -select -assert-count 6 t:LUT3 -select -assert-count 518 t:LUT4 -select -assert-count 10 t:LUT5 -select -assert-count 484 t:LUT6 -select -assert-count 157 t:MUXF7 -select -assert-count 3 t:MUXF8 - -#RRAM128X1D will be synthesized in case when the parameter WIDTHA=4 -#select -assert-count 8 t:RAM128X1D - -select -assert-none t:BUFG t:FDRE t:LUT2 t:LUT3 t:LUT4 t:LUT5 t:LUT6 t:MUXF7 t:MUXF8 %% t:* %D diff --git a/tests/xilinx_ug901/asym_ram_tdp_read_first.v b/tests/xilinx_ug901/asym_ram_tdp_read_first.v deleted file mode 100644 index 2b807a382..000000000 --- a/tests/xilinx_ug901/asym_ram_tdp_read_first.v +++ /dev/null @@ -1,85 +0,0 @@ -// Asymetric RAM - TDP -// READ_FIRST MODE. -// asym_ram_tdp_read_first.v - - -module asym_ram_tdp_read_first (clkA, clkB, enaA, weA, enaB, weB, addrA, addrB, diA, doA, diB, doB); -parameter WIDTHB = 4; -parameter SIZEB = 1024; -parameter ADDRWIDTHB = 10; -parameter WIDTHA = 16; -parameter SIZEA = 256; -parameter ADDRWIDTHA = 8; -input clkA; -input clkB; -input weA, weB; -input enaA, enaB; - -input [ADDRWIDTHA-1:0] addrA; -input [ADDRWIDTHB-1:0] addrB; -input [WIDTHA-1:0] diA; -input [WIDTHB-1:0] diB; - -output [WIDTHA-1:0] doA; -output [WIDTHB-1:0] doB; - -`define max(a,b) {(a) > (b) ? (a) : (b)} -`define min(a,b) {(a) < (b) ? (a) : (b)} - -function integer log2; -input integer value; -reg [31:0] shifted; -integer res; -begin - if (value < 2) - log2 = value; - else - begin - shifted = value-1; - for (res=0; shifted>0; res=res+1) - shifted = shifted>>1; - log2 = res; - end -end -endfunction - -localparam maxSIZE = `max(SIZEA, SIZEB); -localparam maxWIDTH = `max(WIDTHA, WIDTHB); -localparam minWIDTH = `min(WIDTHA, WIDTHB); - -localparam RATIO = maxWIDTH / minWIDTH; -localparam log2RATIO = log2(RATIO); - -reg [minWIDTH-1:0] RAM [0:maxSIZE-1]; -reg [WIDTHA-1:0] readA; -reg [WIDTHB-1:0] readB; - -always @(posedge clkB) -begin - if (enaB) begin - readB <= RAM[addrB] ; - if (weB) - RAM[addrB] <= diB; - end -end - - -always @(posedge clkA) -begin : portA - integer i; - reg [log2RATIO-1:0] lsbaddr ; - for (i=0; i< RATIO; i= i+ 1) begin - lsbaddr = i; - if (enaA) begin - readA[(i+1)*minWIDTH -1 -: minWIDTH] <= RAM[{addrA, lsbaddr}]; - - if (weA) - RAM[{addrA, lsbaddr}] <= diA[(i+1)*minWIDTH-1 -: minWIDTH]; - end - end -end - -assign doA = readA; -assign doB = readB; - -endmodule diff --git a/tests/xilinx_ug901/asym_ram_tdp_read_first.ys b/tests/xilinx_ug901/asym_ram_tdp_read_first.ys deleted file mode 100644 index 5f96b800c..000000000 --- a/tests/xilinx_ug901/asym_ram_tdp_read_first.ys +++ /dev/null @@ -1,21 +0,0 @@ -read_verilog asym_ram_tdp_read_first.v -hierarchy -top asym_ram_tdp_read_first -proc -memory -nomap -equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -memory -opt -full - -# TODO -#equiv_opt -run prove: -assert null -miter -equiv -flatten -make_assert -make_outputs gold gate miter -#sat -verify -prove-asserts -tempinduct -show-inputs -show-outputs miter - -design -load postopt -cd asym_ram_tdp_read_first -stat -#Vivado synthesizes 1 RAMB18E1. -select -assert-count 1 t:$mem -select -assert-count 2 t:LUT2 - -select -assert-none t:$mem t:LUT2 %% t:* %D diff --git a/tests/xilinx_ug901/asym_ram_tdp_write_first.v b/tests/xilinx_ug901/asym_ram_tdp_write_first.v deleted file mode 100644 index 90187ea26..000000000 --- a/tests/xilinx_ug901/asym_ram_tdp_write_first.v +++ /dev/null @@ -1,92 +0,0 @@ -// Asymmetric port RAM - TDP -// WRITE_FIRST MODE. -// asym_ram_tdp_write_first.v - - -module asym_ram_tdp_write_first (clkA, clkB, enaA, weA, enaB, weB, addrA, addrB, diA, doA, diB, doB); -parameter WIDTHB = 4; -//Default parameters were changed because of slow test -//parameter SIZEB = 1024; -//parameter ADDRWIDTHB = 10; -parameter SIZEB = 32; -parameter ADDRWIDTHB = 8; - -//parameter WIDTHA = 16; -parameter WIDTHA = 4; -//parameter SIZEA = 256; -parameter SIZEA = 32; -parameter ADDRWIDTHA = 8; -input clkA; -input clkB; -input weA, weB; -input enaA, enaB; - -input [ADDRWIDTHA-1:0] addrA; -input [ADDRWIDTHB-1:0] addrB; -input [WIDTHA-1:0] diA; -input [WIDTHB-1:0] diB; - -output [WIDTHA-1:0] doA; -output [WIDTHB-1:0] doB; - -`define max(a,b) {(a) > (b) ? (a) : (b)} -`define min(a,b) {(a) < (b) ? (a) : (b)} - -function integer log2; -input integer value; -reg [31:0] shifted; -integer res; -begin - if (value < 2) - log2 = value; - else - begin - shifted = value-1; - for (res=0; shifted>0; res=res+1) - shifted = shifted>>1; - log2 = res; - end -end -endfunction - -localparam maxSIZE = `max(SIZEA, SIZEB); -localparam maxWIDTH = `max(WIDTHA, WIDTHB); -localparam minWIDTH = `min(WIDTHA, WIDTHB); - -localparam RATIO = maxWIDTH / minWIDTH; -localparam log2RATIO = log2(RATIO); - -reg [minWIDTH-1:0] RAM [0:maxSIZE-1]; -reg [WIDTHA-1:0] readA; -reg [WIDTHB-1:0] readB; - -always @(posedge clkB) -begin - if (enaB) begin - if (weB) - RAM[addrB] = diB; - readB = RAM[addrB] ; - end -end - - -always @(posedge clkA) -begin : portA - integer i; - reg [log2RATIO-1:0] lsbaddr ; - for (i=0; i< RATIO; i= i+ 1) begin - lsbaddr = i; - if (enaA) begin - - if (weA) - RAM[{addrA, lsbaddr}] = diA[(i+1)*minWIDTH-1 -: minWIDTH]; - - readA[(i+1)*minWIDTH -1 -: minWIDTH] = RAM[{addrA, lsbaddr}]; - end - end -end - -assign doA = readA; -assign doB = readB; - -endmodule diff --git a/tests/xilinx_ug901/asym_ram_tdp_write_first.ys b/tests/xilinx_ug901/asym_ram_tdp_write_first.ys deleted file mode 100644 index bbe3cc849..000000000 --- a/tests/xilinx_ug901/asym_ram_tdp_write_first.ys +++ /dev/null @@ -1,29 +0,0 @@ -read_verilog asym_ram_tdp_write_first.v -hierarchy -top asym_ram_tdp_write_first -proc -memory -nomap -equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -memory -opt -full - -# TODO -#equiv_opt -run prove: -assert null -miter -equiv -flatten -make_assert -make_outputs gold gate miter -#sat -verify -prove-asserts -tempinduct -show-inputs -show-outputs miter - -design -load postopt -cd asym_ram_tdp_write_first -stat -#Vivado synthesizes 1 RAMB18E1. -select -assert-count 2 t:BUFG -select -assert-count 200 t:FDRE -select -assert-count 10 t:LUT2 -select -assert-count 44 t:LUT3 -select -assert-count 81 t:LUT4 -select -assert-count 104 t:LUT5 -select -assert-count 560 t:LUT6 -select -assert-count 261 t:MUXF7 -select -assert-count 127 t:MUXF8 - - -select -assert-none t:BUFG t:FDRE t:LUT2 t:LUT3 t:LUT4 t:LUT5 t:LUT6 t:MUXF7 t:MUXF8 %% t:* %D diff --git a/tests/xilinx_ug901/black_box_1.v b/tests/xilinx_ug901/black_box_1.v deleted file mode 100644 index 40caa1b10..000000000 --- a/tests/xilinx_ug901/black_box_1.v +++ /dev/null @@ -1,19 +0,0 @@ -// Black Box -// black_box_1.v -// -(* black_box *) module black_box1 (in1, in2, dout); -input in1, in2; -output dout; -endmodule - -module black_box_1 (DI_1, DI_2, DOUT); -input DI_1, DI_2; -output DOUT; - -black_box1 U1 ( - .in1(DI_1), - .in2(DI_2), - .dout(DOUT) - ); - -endmodule diff --git a/tests/xilinx_ug901/black_box_1.ys b/tests/xilinx_ug901/black_box_1.ys deleted file mode 100644 index acf0b5761..000000000 --- a/tests/xilinx_ug901/black_box_1.ys +++ /dev/null @@ -1,15 +0,0 @@ -read_verilog black_box_1.v -hierarchy -top black_box_1 -proc -tribuf -flatten -synth -#equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check -equiv_opt -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) -cd black_box_1 # Constrain all select calls below inside the top module -#Vivado synthesizes 1 black box. -#stat -#select -assert-count 0 t:LUT1 -#select -assert-count 1 t:$_TBUF_ -#select -assert-none t:LUT1 t:$_TBUF_ %% t:* %D diff --git a/tests/xilinx_ug901/bytewrite_ram_1b.v b/tests/xilinx_ug901/bytewrite_ram_1b.v deleted file mode 100644 index 46d86c297..000000000 --- a/tests/xilinx_ug901/bytewrite_ram_1b.v +++ /dev/null @@ -1,42 +0,0 @@ -// Single-Port BRAM with Byte-wide Write Enable -// Read-First mode -// Single-process description -// Compact description of the write with a generate-for -// statement -// Column width and number of columns easily configurable -// -// bytewrite_ram_1b.v -// - -module bytewrite_ram_1b (clk, we, addr, di, do); - -parameter SIZE = 1024; -parameter ADDR_WIDTH = 10; -parameter COL_WIDTH = 8; -parameter NB_COL = 4; - -input clk; -input [NB_COL-1:0] we; -input [ADDR_WIDTH-1:0] addr; -input [NB_COL*COL_WIDTH-1:0] di; -output reg [NB_COL*COL_WIDTH-1:0] do; - -reg [NB_COL*COL_WIDTH-1:0] RAM [SIZE-1:0]; - -always @(posedge clk) -begin - do <= RAM[addr]; -end - -generate genvar i; -for (i = 0; i < NB_COL; i = i+1) -begin -always @(posedge clk) -begin - if (we[i]) - RAM[addr][(i+1)*COL_WIDTH-1:i*COL_WIDTH] <= di[(i+1)*COL_WIDTH-1:i*COL_WIDTH]; - end -end -endgenerate - -endmodule diff --git a/tests/xilinx_ug901/bytewrite_ram_1b.ys b/tests/xilinx_ug901/bytewrite_ram_1b.ys deleted file mode 100644 index 4f0967801..000000000 --- a/tests/xilinx_ug901/bytewrite_ram_1b.ys +++ /dev/null @@ -1,22 +0,0 @@ -read_verilog bytewrite_ram_1b.v -hierarchy -top bytewrite_ram_1b -proc -memory -nomap -equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -memory -opt -full - -# TODO -#equiv_opt -run prove: -assert null -miter -equiv -flatten -make_assert -make_outputs gold gate miter -#sat -verify -prove-asserts -tempinduct -show-inputs -show-outputs miter - -design -load postopt -cd bytewrite_ram_1b -stat -#Vivado synthesizes 1 RAMB36E1. -select -assert-count 1 t:BUFG -select -assert-count 32 t:LUT2 -select -assert-count 8 t:RAMB36E1 - -select -assert-none t:BUFG t:LUT2 t:RAMB36E1 %% t:* %D diff --git a/tests/xilinx_ug901/bytewrite_tdp_ram_nc.v b/tests/xilinx_ug901/bytewrite_tdp_ram_nc.v deleted file mode 100644 index 1093b0838..000000000 --- a/tests/xilinx_ug901/bytewrite_tdp_ram_nc.v +++ /dev/null @@ -1,78 +0,0 @@ -// -// True-Dual-Port BRAM with Byte-wide Write Enable -// No-Change mode -// -// bytewrite_tdp_ram_nc.v -// -// ByteWide Write Enable, - NO_CHANGE mode template - Vivado recomended -module bytewrite_tdp_ram_nc - #( - //--------------------------------------------------------------- - parameter NUM_COL = 4, - parameter COL_WIDTH = 8, - parameter ADDR_WIDTH = 10, // Addr Width in bits : 2**ADDR_WIDTH = RAM Depth - parameter DATA_WIDTH = NUM_COL*COL_WIDTH // Data Width in bits - //--------------------------------------------------------------- - ) ( - input clkA, - input enaA, - input [NUM_COL-1:0] weA, - input [ADDR_WIDTH-1:0] addrA, - input [DATA_WIDTH-1:0] dinA, - output reg [DATA_WIDTH-1:0] doutA, - - input clkB, - input enaB, - input [NUM_COL-1:0] weB, - input [ADDR_WIDTH-1:0] addrB, - input [DATA_WIDTH-1:0] dinB, - output reg [DATA_WIDTH-1:0] doutB - ); - - - // Core Memory - reg [DATA_WIDTH-1:0] ram_block [(2**ADDR_WIDTH)-1:0]; - - // Port-A Operation - generate - genvar i; - for(i=0;i run-test.mk -exec ${MAKE:-make} -f run-test.mk diff --git a/tests/xilinx_ug901/sfir_shifter.v b/tests/xilinx_ug901/sfir_shifter.v deleted file mode 100644 index a8b144bcd..000000000 --- a/tests/xilinx_ug901/sfir_shifter.v +++ /dev/null @@ -1,19 +0,0 @@ -//sfir_shifter.v -(* dont_touch = "yes" *) -module sfir_shifter #(parameter dsize = 16, nbtap = 4) - (input clk,input [dsize-1:0] datain, output [dsize-1:0] dataout); - - (* srl_style = "srl_register" *) reg [dsize-1:0] tmp [0:2*nbtap-1]; - integer i; - - always @(posedge clk) - begin - tmp[0] <= datain; - for (i=0; i<=2*nbtap-2; i=i+1) - tmp[i+1] <= tmp[i]; - end - - assign dataout = tmp[2*nbtap-1]; - -endmodule -// sfir_shifter diff --git a/tests/xilinx_ug901/sfir_shifter.ys b/tests/xilinx_ug901/sfir_shifter.ys deleted file mode 100644 index b9fbeb8cb..000000000 --- a/tests/xilinx_ug901/sfir_shifter.ys +++ /dev/null @@ -1,16 +0,0 @@ -read_verilog sfir_shifter.v -hierarchy -top sfir_shifter -proc -flatten -#ERROR: Found 32 unproven $equiv cells in 'equiv_status -assert'. -#equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check -equiv_opt -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) - -cd sfir_shifter -#Vivado synthesizes 32 FDRE, 16 SRL16E. -stat -select -assert-count 1 t:BUFG -select -assert-count 16 t:SRL16E - -select -assert-none t:BUFG t:SRL16E %% t:* %D diff --git a/tests/xilinx_ug901/shift_registers_0.v b/tests/xilinx_ug901/shift_registers_0.v deleted file mode 100644 index 77a3ec893..000000000 --- a/tests/xilinx_ug901/shift_registers_0.v +++ /dev/null @@ -1,22 +0,0 @@ -// 8-bit Shift Register -// Rising edge clock -// Active high clock enable -// Concatenation-based template -// File: shift_registers_0.v - -module shift_registers_0 (clk, clken, SI, SO); -parameter WIDTH = 32; -input clk, clken, SI; -output SO; - -reg [WIDTH-1:0] shreg; - -always @(posedge clk) - begin - if (clken) - shreg = {shreg[WIDTH-2:0], SI}; - end - -assign SO = shreg[WIDTH-1]; - -endmodule diff --git a/tests/xilinx_ug901/shift_registers_0.ys b/tests/xilinx_ug901/shift_registers_0.ys deleted file mode 100644 index 89da1d7cc..000000000 --- a/tests/xilinx_ug901/shift_registers_0.ys +++ /dev/null @@ -1,14 +0,0 @@ -read_verilog shift_registers_0.v -hierarchy -top shift_registers_0 -proc -flatten -#ERROR: Found 2 unproven $equiv cells in 'equiv_status -assert'. -#equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check -equiv_opt -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) -cd shift_registers_0 # Constrain all select calls below inside the top module -#Vivado synthesizes 1 BUFG, 2 FDRE, 3 SRLC32E. -select -assert-count 1 t:BUFG -select -assert-count 1 t:SRLC32E -select -assert-none t:BUFG t:SRLC32E %% t:* %D diff --git a/tests/xilinx_ug901/shift_registers_1.v b/tests/xilinx_ug901/shift_registers_1.v deleted file mode 100644 index d50820e7b..000000000 --- a/tests/xilinx_ug901/shift_registers_1.v +++ /dev/null @@ -1,24 +0,0 @@ -// 32-bit Shift Register -// Rising edge clock -// Active high clock enable -// For-loop based template -// File: shift_registers_1.v - -module shift_registers_1 (clk, clken, SI, SO); -parameter WIDTH = 32; -input clk, clken, SI; -output SO; -reg [WIDTH-1:0] shreg; - -integer i; -always @(posedge clk) -begin - if (clken) - begin - for (i = 0; i < WIDTH-1; i = i+1) - shreg[i+1] <= shreg[i]; - shreg[0] <= SI; - end -end -assign SO = shreg[WIDTH-1]; -endmodule diff --git a/tests/xilinx_ug901/shift_registers_1.ys b/tests/xilinx_ug901/shift_registers_1.ys deleted file mode 100644 index b53b6cb25..000000000 --- a/tests/xilinx_ug901/shift_registers_1.ys +++ /dev/null @@ -1,14 +0,0 @@ -read_verilog shift_registers_1.v -hierarchy -top shift_registers_1 -proc -flatten -#ERROR: Found 2 unproven $equiv cells in 'equiv_status -assert'. -#equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check -equiv_opt -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) -cd shift_registers_1 # Constrain all select calls below inside the top module -#Vivado synthesizes 1 BUFG, 2 FDRE, 3 SRLC32E. -select -assert-count 1 t:BUFG -select -assert-count 1 t:SRLC32E -select -assert-none t:BUFG t:SRLC32E %% t:* %D diff --git a/tests/xilinx_ug901/squarediffmacc.v b/tests/xilinx_ug901/squarediffmacc.v deleted file mode 100644 index 6535b24c4..000000000 --- a/tests/xilinx_ug901/squarediffmacc.v +++ /dev/null @@ -1,52 +0,0 @@ -// This module performs subtraction of two inputs, squaring on the diff -// and then accumulation -// This can be implemented in 1 DSP Block (Ultrascale architecture) -// File : squarediffmacc.v -module squarediffmacc # ( - //Default parameters were changed because of slow test - //parameter SIZEIN = 16, - //SIZEOUT = 40 - parameter SIZEIN = 8, - SIZEOUT = 20 - ) - ( - input clk, - input ce, - input sload, - input signed [SIZEIN-1:0] a, - input signed [SIZEIN-1:0] b, - output signed [SIZEOUT+1:0] accum_out - ); - -// Declare registers for intermediate values -reg signed [SIZEIN-1:0] a_reg, b_reg; -reg signed [SIZEIN:0] diff_reg; -reg sload_reg; -reg signed [2*SIZEIN+1:0] m_reg; -reg signed [SIZEOUT-1:0] adder_out, old_result; - - always @(sload_reg or adder_out) - if (sload_reg) - old_result <= 0; - else - // 'sload' is now and opens the accumulation loop. - // The accumulator takes the next multiplier output - // in the same cycle. - old_result <= adder_out; - - always @(posedge clk) - if (ce) - begin - a_reg <= a; - b_reg <= b; - diff_reg <= a_reg - b_reg; - m_reg <= diff_reg * diff_reg; - sload_reg <= sload; - // Store accumulation result into a register - adder_out <= old_result + m_reg; - end - - // Output accumulation result - assign accum_out = adder_out; - -endmodule // squarediffmacc diff --git a/tests/xilinx_ug901/squarediffmacc.ys b/tests/xilinx_ug901/squarediffmacc.ys deleted file mode 100644 index 92474bea3..000000000 --- a/tests/xilinx_ug901/squarediffmacc.ys +++ /dev/null @@ -1,23 +0,0 @@ -read_verilog squarediffmacc.v -hierarchy -top squarediffmacc -proc -flatten -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) - -cd squarediffmacc -#Vivado synthesizes 1 DSP48E1, 33 FDRE, 16 LUT. -stat -select -assert-count 1 t:BUFG -select -assert-count 64 t:FDRE -select -assert-count 78 t:LUT2 -select -assert-count 7 t:LUT3 -select -assert-count 11 t:LUT4 -select -assert-count 8 t:LUT5 -select -assert-count 125 t:LUT6 -select -assert-count 44 t:MUXCY -select -assert-count 50 t:MUXF7 -select -assert-count 17 t:MUXF8 -select -assert-count 47 t:XORCY - -select -assert-none t:BUFG t:FDRE t:LUT2 t:LUT3 t:LUT4 t:LUT5 t:LUT6 t:MUXCY t:MUXF7 t:MUXF8 t:XORCY %% t:* %D diff --git a/tests/xilinx_ug901/squarediffmult.v b/tests/xilinx_ug901/squarediffmult.v deleted file mode 100644 index 0f41b67bc..000000000 --- a/tests/xilinx_ug901/squarediffmult.v +++ /dev/null @@ -1,42 +0,0 @@ -// Squarer support for DSP block (DSP48E2) with -// pre-adder configured -// as subtractor -// File: squarediffmult.v - -module squarediffmult # (parameter SIZEIN = 16) - ( - input clk, ce, rst, - input signed [SIZEIN-1:0] a, b, - output signed [2*SIZEIN+1:0] square_out - ); - - // Declare registers for intermediate values -reg signed [SIZEIN-1:0] a_reg, b_reg; -reg signed [SIZEIN:0] diff_reg; -reg signed [2*SIZEIN+1:0] m_reg, p_reg; - -always @(posedge clk) -begin - if (rst) - begin - a_reg <= 0; - b_reg <= 0; - diff_reg <= 0; - m_reg <= 0; - p_reg <= 0; - end - else - if (ce) - begin - a_reg <= a; - b_reg <= b; - diff_reg <= a_reg - b_reg; - m_reg <= diff_reg * diff_reg; - p_reg <= m_reg; - end -end - -// Output result -assign square_out = p_reg; - -endmodule // squarediffmult diff --git a/tests/xilinx_ug901/squarediffmult.ys b/tests/xilinx_ug901/squarediffmult.ys deleted file mode 100644 index 3468e5bb4..000000000 --- a/tests/xilinx_ug901/squarediffmult.ys +++ /dev/null @@ -1,30 +0,0 @@ -read_verilog squarediffmult.v -hierarchy -top squarediffmult -proc -memory -nomap -equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -memory -opt -full - -# TODO -#equiv_opt -run prove: -assert null -miter -equiv -flatten -make_assert -make_outputs gold gate miter -#sat -verify -prove-asserts -tempinduct -show-inputs -show-outputs miter - -design -load postopt -cd squarediffmult -stat -#Vivado synthesizes 16 FDRE, 1 DSP48E1. -select -assert-count 1 t:BUFG -select -assert-count 117 t:FDRE -select -assert-count 223 t:LUT2 -select -assert-count 50 t:LUT3 -select -assert-count 38 t:LUT4 -select -assert-count 56 t:LUT5 -select -assert-count 372 t:LUT6 -select -assert-count 49 t:MUXCY -select -assert-count 99 t:MUXF7 -select -assert-count 26 t:MUXF8 -select -assert-count 51 t:XORCY - -select -assert-none t:BUFG t:FDRE t:LUT2 t:LUT3 t:LUT4 t:LUT5 t:LUT6 t:MUXCY t:MUXF7 t:MUXF8 t:XORCY %% t:* %D diff --git a/tests/xilinx_ug901/top_mux.v b/tests/xilinx_ug901/top_mux.v deleted file mode 100644 index c23c7491c..000000000 --- a/tests/xilinx_ug901/top_mux.v +++ /dev/null @@ -1,18 +0,0 @@ -// Multiplexer using case statement -module mux4 (sel, a, b, c, d, outmux); -input [1:0] sel; -input [1:0] a, b, c, d; -output [1:0] outmux; -reg [1:0] outmux; - -always @ * - begin - case(sel) - 2'b00 : outmux = a; - 2'b01 : outmux = b; - 2'b10 : outmux = c; - 2'b11 : outmux = d; - endcase - end -endmodule - diff --git a/tests/xilinx_ug901/top_mux.ys b/tests/xilinx_ug901/top_mux.ys deleted file mode 100644 index 0245f3bbc..000000000 --- a/tests/xilinx_ug901/top_mux.ys +++ /dev/null @@ -1,13 +0,0 @@ -read_verilog top_mux.v -hierarchy -top mux4 -proc -flatten -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) - -cd mux4 -#Vivado synthesizes 2 LUT. -stat -select -assert-count 2 t:LUT6 - -select -assert-none t:LUT6 %% t:* %D diff --git a/tests/xilinx_ug901/tristates_1.v b/tests/xilinx_ug901/tristates_1.v deleted file mode 100644 index 0038a9989..000000000 --- a/tests/xilinx_ug901/tristates_1.v +++ /dev/null @@ -1,17 +0,0 @@ -// Tristate Description Using Combinatorial Always Block -// File: tristates_1.v -// -module tristates_1 (T, I, O); -input T, I; -output O; -reg O; - -always @(T or I) -begin - if (~T) - O = I; - else - O = 1'bZ; -end - -endmodule diff --git a/tests/xilinx_ug901/tristates_1.ys b/tests/xilinx_ug901/tristates_1.ys deleted file mode 100644 index 7c13dc227..000000000 --- a/tests/xilinx_ug901/tristates_1.ys +++ /dev/null @@ -1,13 +0,0 @@ -read_verilog tristates_1.v -hierarchy -top tristates_1 -proc -tribuf -flatten -synth -equiv_opt -assert -map +/xilinx/cells_sim.v -map +/simcells.v synth_xilinx # equivalency check -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 -#Vivado synthesizes 3 IBUF, 1 OBUFT. -select -assert-count 1 t:LUT1 -select -assert-count 1 t:$_TBUF_ -select -assert-none t:LUT1 t:$_TBUF_ %% t:* %D diff --git a/tests/xilinx_ug901/tristates_2.v b/tests/xilinx_ug901/tristates_2.v deleted file mode 100644 index 0c70a1257..000000000 --- a/tests/xilinx_ug901/tristates_2.v +++ /dev/null @@ -1,10 +0,0 @@ -// Tristate Description Using Concurrent Assignment -// File: tristates_2.v -// -module tristates_2 (T, I, O); -input T, I; -output O; - -assign O = (~T) ? I: 1'bZ; - -endmodule diff --git a/tests/xilinx_ug901/tristates_2.ys b/tests/xilinx_ug901/tristates_2.ys deleted file mode 100644 index ba2e1d855..000000000 --- a/tests/xilinx_ug901/tristates_2.ys +++ /dev/null @@ -1,13 +0,0 @@ -read_verilog tristates_2.v -hierarchy -top tristates_2 -proc -tribuf -flatten -synth -equiv_opt -assert -map +/xilinx/cells_sim.v -map +/simcells.v synth_xilinx # equivalency check -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 -#Vivado synthesizes 3 IBUF, 1 OBUFT. -select -assert-count 1 t:LUT1 -select -assert-count 1 t:$_TBUF_ -select -assert-none t:LUT1 t:$_TBUF_ %% t:* %D diff --git a/tests/xilinx_ug901/xilinx_ultraram_single_port_no_change.v b/tests/xilinx_ug901/xilinx_ultraram_single_port_no_change.v deleted file mode 100644 index f5e843dc9..000000000 --- a/tests/xilinx_ug901/xilinx_ultraram_single_port_no_change.v +++ /dev/null @@ -1,78 +0,0 @@ -// Xilinx UltraRAM Single Port No Change Mode. This code implements -// a parameterizable UltraRAM block in No Change mode. The behavior of this RAM is -// when data is written, the output of RAM is unchanged. Only when write is -// inactive data corresponding to the address is presented on the output port. -// -module xilinx_ultraram_single_port_no_change #( -//Default parameters were changed because of slow test - //parameter AWIDTH = 12, // Address Width - //parameter DWIDTH = 72, // Data Width - //parameter NBPIPE = 3 // Number of pipeline Registers - parameter AWIDTH = 8, // Address Width - parameter DWIDTH = 8, // Data Width - parameter NBPIPE = 3 // Number of pipeline Registers - ) ( - input clk, // Clock - input rst, // Reset - input we, // Write Enable - input regce, // Output Register Enable - input mem_en, // Memory Enable - input [DWIDTH-1:0] din, // Data Input - input [AWIDTH-1:0] addr, // Address Input - output reg [DWIDTH-1:0] dout // Data Output - ); - -(* ram_style = "ultra" *) -reg [DWIDTH-1:0] mem[(1<