diff options
| author | SergeyDegtyar <sndegtyar@gmail.com> | 2019-09-10 08:11:56 +0300 |
|---|---|---|
| committer | Miodrag Milanovic <mmicko@gmail.com> | 2019-10-17 17:10:02 +0200 |
| commit | 6331fa5b022b9e16f9392d9604a545f86dc13385 (patch) | |
| tree | 1be8bae4611fcb193893c73ac3bb3848c0c6944b /tests | |
| parent | 757c476f625bef871f9a4388d4d19bf8c3bc400b (diff) | |
| download | yosys-6331fa5b022b9e16f9392d9604a545f86dc13385.tar.gz yosys-6331fa5b022b9e16f9392d9604a545f86dc13385.tar.bz2 yosys-6331fa5b022b9e16f9392d9604a545f86dc13385.zip | |
Remove xilinx_ug901 tests (will be moved to yosys-tests)
Diffstat (limited to 'tests')
88 files changed, 0 insertions, 2962 deletions
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<NUM_COL;i=i+1) begin
- always @ (posedge clkA) begin
- if(enaA) begin
- if(weA[i]) begin
- ram_block[addrA][i*COL_WIDTH +: COL_WIDTH] <= dinA[i*COL_WIDTH +: COL_WIDTH];
- end
- end
- end
- end
- endgenerate
-
- always @ (posedge clkA) begin
- if(enaA) begin
- if (~|weA)
- doutA <= ram_block[addrA];
- end
- end
-
-
- // Port-B Operation:
- generate
- for(i=0;i<NUM_COL;i=i+1) begin
- always @ (posedge clkB) begin
- if(enaB) begin
- if(weB[i]) begin
- ram_block[addrB][i*COL_WIDTH +: COL_WIDTH] <= dinB[i*COL_WIDTH +: COL_WIDTH];
- end
- end
- end
- end
- endgenerate
-
- always @ (posedge clkB) begin
- if(enaB) begin
- if (~|weB)
- doutB <= ram_block[addrB];
- end
- end
-
-endmodule // bytewrite_tdp_ram_nc
diff --git a/tests/xilinx_ug901/bytewrite_tdp_ram_nc.ys b/tests/xilinx_ug901/bytewrite_tdp_ram_nc.ys deleted file mode 100644 index b6818e322..000000000 --- a/tests/xilinx_ug901/bytewrite_tdp_ram_nc.ys +++ /dev/null @@ -1,22 +0,0 @@ -read_verilog bytewrite_tdp_ram_nc.v -hierarchy -top bytewrite_tdp_ram_nc -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_tdp_ram_nc -stat -#Vivado synthesizes 1 RAMB36E1. -select -assert-count 1 t:$mem -select -assert-count 8 t:LUT2 -select -assert-count 64 t:LUT3 -select -assert-count 2 t:LUT5 -select -assert-none t:LUT2 t:LUT3 t:LUT5 t:$mem %% t:* %D diff --git a/tests/xilinx_ug901/bytewrite_tdp_ram_readfirst2.v b/tests/xilinx_ug901/bytewrite_tdp_ram_readfirst2.v deleted file mode 100644 index 349aa2aec..000000000 --- a/tests/xilinx_ug901/bytewrite_tdp_ram_readfirst2.v +++ /dev/null @@ -1,71 +0,0 @@ -// ByteWide Write Enable, - Alternate READ_FIRST mode template - Vivado recomended
-// bytewrite_tdp_ram_readfirst2.v
-module bytewrite_tdp_ram_readfirst2
- #(
- //-------------------------------------------------------------------------
- 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<NUM_COL;i=i+1) begin
- always @ (posedge clkA) begin
- if(enaA) begin
- if(weA[i]) begin
- ram_block[addrA][i*COL_WIDTH +: COL_WIDTH] <= dinA[i*COL_WIDTH +: COL_WIDTH];
- end
- end
- end
- end
- endgenerate
-
- always @ (posedge clkA) begin
- if(enaA) begin
- doutA <= ram_block[addrA];
- end
- end
-
-
- // Port-B Operation:
- generate
- for(i=0;i<NUM_COL;i=i+1) begin
- always @ (posedge clkB) begin
- if(enaB) begin
- if(weB[i]) begin
- ram_block[addrB][i*COL_WIDTH +: COL_WIDTH] <= dinB[i*COL_WIDTH +: COL_WIDTH];
- end
- end
- end
- end
- endgenerate
-
- always @ (posedge clkB) begin
- if(enaB) begin
- doutB <= ram_block[addrB];
- end
- end
-
-endmodule // bytewrite_tdp_ram_readfirst2
diff --git a/tests/xilinx_ug901/bytewrite_tdp_ram_readfirst2.ys b/tests/xilinx_ug901/bytewrite_tdp_ram_readfirst2.ys deleted file mode 100644 index 3273d0d43..000000000 --- a/tests/xilinx_ug901/bytewrite_tdp_ram_readfirst2.ys +++ /dev/null @@ -1,21 +0,0 @@ -read_verilog bytewrite_tdp_ram_readfirst2.v -hierarchy -top bytewrite_tdp_ram_readfirst2 -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_tdp_ram_readfirst2 -stat -#Vivado synthesizes 1 RAMB36E1. -select -assert-count 1 t:$mem -select -assert-count 8 t:LUT2 -select -assert-count 64 t:LUT3 -select -assert-none t:LUT2 t:LUT3 t:$mem %% t:* %D diff --git a/tests/xilinx_ug901/bytewrite_tdp_ram_rf.v b/tests/xilinx_ug901/bytewrite_tdp_ram_rf.v deleted file mode 100644 index 72dad9d8f..000000000 --- a/tests/xilinx_ug901/bytewrite_tdp_ram_rf.v +++ /dev/null @@ -1,61 +0,0 @@ -// True-Dual-Port BRAM with Byte-wide Write Enable
-// Read-First mode
-// bytewrite_tdp_ram_rf.v
-//
-
-module bytewrite_tdp_ram_rf
- #(
-//--------------------------------------------------------------------------
-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];
-
- integer i;
- // Port-A Operation
- always @ (posedge clkA) begin
- if(enaA) begin
- for(i=0;i<NUM_COL;i=i+1) begin
- if(weA[i]) begin
- ram_block[addrA][i*COL_WIDTH +: COL_WIDTH] <= dinA[i*COL_WIDTH +: COL_WIDTH];
- end
- end
- doutA <= ram_block[addrA];
- end
- end
-
- // Port-B Operation:
- always @ (posedge clkB) begin
- if(enaB) begin
- for(i=0;i<NUM_COL;i=i+1) begin
- if(weB[i]) begin
- ram_block[addrB][i*COL_WIDTH +: COL_WIDTH] <= dinB[i*COL_WIDTH +: COL_WIDTH];
- end
- end
-
- doutB <= ram_block[addrB];
- end
- end
-
-endmodule // bytewrite_tdp_ram_rf
diff --git a/tests/xilinx_ug901/bytewrite_tdp_ram_rf.ys b/tests/xilinx_ug901/bytewrite_tdp_ram_rf.ys deleted file mode 100644 index 2a34d9abe..000000000 --- a/tests/xilinx_ug901/bytewrite_tdp_ram_rf.ys +++ /dev/null @@ -1,21 +0,0 @@ -read_verilog bytewrite_tdp_ram_rf.v -hierarchy -top bytewrite_tdp_ram_rf -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_tdp_ram_rf -stat -#Vivado synthesizes 1 RAMB36E1. -select -assert-count 1 t:$mem -select -assert-count 8 t:LUT2 -select -assert-count 64 t:LUT3 -select -assert-none t:LUT2 t:LUT3 t:$mem %% t:* %D diff --git a/tests/xilinx_ug901/bytewrite_tdp_ram_wf.v b/tests/xilinx_ug901/bytewrite_tdp_ram_wf.v deleted file mode 100644 index d39565e52..000000000 --- a/tests/xilinx_ug901/bytewrite_tdp_ram_wf.v +++ /dev/null @@ -1,68 +0,0 @@ -// True-Dual-Port BRAM with Byte-wide Write Enable
-// Write-First mode
-// File: HDL_Coding_Techniques/rams/bytewrite_tdp_ram_wf.v
-//
-// ByteWide Write Enable, - WRITE_FIRST mode template - Vivado recomended
-module bytewrite_tdp_ram_wf
- #(
- //----------------------------------------------------------------------
-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<NUM_COL;i=i+1) begin
- always @ (posedge clkA) begin
- if(enaA) begin
- if(weA[i]) begin
- ram_block[addrA][i*COL_WIDTH +: COL_WIDTH] <= dinA[i*COL_WIDTH +: COL_WIDTH];
- doutA[i*COL_WIDTH +: COL_WIDTH] <= dinA[i*COL_WIDTH +: COL_WIDTH] ;
- end else begin
- doutA[i*COL_WIDTH +: COL_WIDTH] <= ram_block[addrA][i*COL_WIDTH +: COL_WIDTH] ;
- end
- end
- end
- end
- endgenerate
-
- // Port-B Operation:
- generate
- for(i=0;i<NUM_COL;i=i+1) begin
- always @ (posedge clkB) begin
- if(enaB) begin
- if(weB[i]) begin
- ram_block[addrB][i*COL_WIDTH +: COL_WIDTH] <= dinB[i*COL_WIDTH +: COL_WIDTH];
- doutB[i*COL_WIDTH +: COL_WIDTH] <= dinB[i*COL_WIDTH +: COL_WIDTH] ;
- end else begin
- doutB[i*COL_WIDTH +: COL_WIDTH] <= ram_block[addrB][i*COL_WIDTH +: COL_WIDTH] ;
- end
- end
- end
- end
- endgenerate
-
-endmodule // bytewrite_tdp_ram_wf
diff --git a/tests/xilinx_ug901/bytewrite_tdp_ram_wf.ys b/tests/xilinx_ug901/bytewrite_tdp_ram_wf.ys deleted file mode 100644 index b681d0c2b..000000000 --- a/tests/xilinx_ug901/bytewrite_tdp_ram_wf.ys +++ /dev/null @@ -1,23 +0,0 @@ -read_verilog bytewrite_tdp_ram_wf.v -hierarchy -top bytewrite_tdp_ram_wf -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_tdp_ram_wf -stat -#Vivado synthesizes 1 RAMB36E1. -select -assert-count 1 t:$mem -select -assert-count 2 t:BUFG -select -assert-count 64 t:FDRE -select -assert-count 8 t:LUT2 -select -assert-count 128 t:LUT3 -select -assert-none t:BUFG t:FDRE t:LUT2 t:LUT3 t:$mem %% t:* %D diff --git a/tests/xilinx_ug901/cmacc.v b/tests/xilinx_ug901/cmacc.v deleted file mode 100644 index 038402daf..000000000 --- a/tests/xilinx_ug901/cmacc.v +++ /dev/null @@ -1,122 +0,0 @@ -// Complex Multiplier with accumulation (pr+i.pi) = (ar+i.ai)*(br+i.bi)
-// File: cmacc.v
-// The RTL below describes a complex multiplier with accumulation
-// which can be packed into 3 DSP blocks (Ultrascale architecture)
-//Default parameters were changed because of slow test
-//module cmacc # (parameter AWIDTH = 16, BWIDTH = 18, SIZEOUT = 40)
-module cmacc # (parameter AWIDTH = 4, BWIDTH = 5, SIZEOUT = 9)
- (
- input clk,
- input sload,
- input signed [AWIDTH-1:0] ar,
- input signed [AWIDTH-1:0] ai,
- input signed [BWIDTH-1:0] br,
- input signed [BWIDTH-1:0] bi,
- output signed [SIZEOUT-1:0] pr,
- output signed [SIZEOUT-1:0] pi);
-
- reg signed [AWIDTH-1:0] ai_d, ai_dd, ai_ddd, ai_dddd;
- reg signed [AWIDTH-1:0] ar_d, ar_dd, ar_ddd, ar_dddd;
- reg signed [BWIDTH-1:0] bi_d, bi_dd, bi_ddd, br_d, br_dd, br_ddd;
- reg signed [AWIDTH:0] addcommon;
- reg signed [BWIDTH:0] addr, addi;
- reg signed [AWIDTH+BWIDTH:0] mult0, multr, multi;
- reg signed [SIZEOUT-1:0] pr_int, pi_int, old_result_real, old_result_im;
- reg signed [AWIDTH+BWIDTH:0] common, commonr1, commonr2;
-
- reg sload_reg;
-
- `ifdef SIM
- initial
- begin
- ai_d = 0;
- ai_dd = 0;
- ai_ddd = 0;
- ai_dddd = 0;
- ar_d = 0;
- ar_dd = 0;
- ar_ddd = 0;
- ar_dddd = 0;
- bi_d = 0;
- bi_dd = 0;
- bi_ddd = 0;
- br_d = 0;
- br_dd = 0;
- br_ddd = 0;
- end
- `endif
-
- always @(posedge clk)
- begin
- ar_d <= ar;
- ar_dd <= ar_d;
- ai_d <= ai;
- ai_dd <= ai_d;
- br_d <= br;
- br_dd <= br_d;
- br_ddd <= br_dd;
- bi_d <= bi;
- bi_dd <= bi_d;
- bi_ddd <= bi_dd;
- sload_reg <= sload;
- end
-
- // Common factor (ar ai) x bi, shared for the calculations of the real and imaginary final products
- //
- always @(posedge clk)
- begin
- addcommon <= ar_d - ai_d;
- mult0 <= addcommon * bi_dd;
- common <= mult0;
- end
-
- // Accumulation loop (combinatorial) for *Real*
- //
- always @(sload_reg or pr_int)
- if (sload_reg)
- old_result_real <= 0;
- else
- // 'sload' is now and opens the accumulation loop.
- // The accumulator takes the next multiplier output
- // in the same cycle.
- old_result_real <= pr_int;
-
- // Real product
- //
- always @(posedge clk)
- begin
- ar_ddd <= ar_dd;
- ar_dddd <= ar_ddd;
- addr <= br_ddd - bi_ddd;
- multr <= addr * ar_dddd;
- commonr1 <= common;
- pr_int <= multr + commonr1 + old_result_real;
- end
-
- // Accumulation loop (combinatorial) for *Imaginary*
- //
- always @(sload_reg or pi_int)
- if (sload_reg)
- old_result_im <= 0;
- else
- // 'sload' is now and opens the accumulation loop.
- // The accumulator takes the next multiplier output
- // in the same cycle.
- old_result_im <= pi_int;
-
- // Imaginary product
- //
- always @(posedge clk)
- begin
- ai_ddd <= ai_dd;
- ai_dddd <= ai_ddd;
- addi <= br_ddd + bi_ddd;
- multi <= addi * ai_dddd;
- commonr2 <= common;
- pi_int <= multi + commonr2 + old_result_im;
- end
-
- assign pr = pr_int;
- assign pi = pi_int;
-
-endmodule // cmacc
diff --git a/tests/xilinx_ug901/cmacc.ys b/tests/xilinx_ug901/cmacc.ys deleted file mode 100644 index c1ac931c8..000000000 --- a/tests/xilinx_ug901/cmacc.ys +++ /dev/null @@ -1,25 +0,0 @@ -read_verilog cmacc.v -hierarchy -top cmacc -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 cmacc -#Vivado synthesizes 5 DSP48E1, 32 FDRE, 18 LUT. -stat -select -assert-count 1 t:BUFG -select -assert-count 77 t:FDRE -select -assert-count 5 t:LUT1 -select -assert-count 46 t:LUT2 -select -assert-count 25 t:LUT3 -select -assert-count 8 t:LUT4 -select -assert-count 16 t:LUT5 -select -assert-count 85 t:LUT6 -select -assert-count 54 t:MUXCY -select -assert-count 8 t:MUXF7 -select -assert-count 2 t:MUXF8 -select -assert-count 22 t:SRL16E -select -assert-count 62 t:XORCY - -select -assert-none t:BUFG t:FDRE t:LUT1 t:LUT2 t:LUT3 t:LUT4 t:LUT5 t:LUT6 t:MUXCY t:MUXF7 t:MUXF8 t:SRL16E t:XORCY %% t:* %D diff --git a/tests/xilinx_ug901/cmult.v b/tests/xilinx_ug901/cmult.v deleted file mode 100644 index d5d85a28c..000000000 --- a/tests/xilinx_ug901/cmult.v +++ /dev/null @@ -1,71 +0,0 @@ -//
-// Complex Multiplier (pr+i.pi) = (ar+i.ai)*(br+i.bi)
-// file: cmult.v
-
-module cmult # (parameter AWIDTH = 16, BWIDTH = 18)
- (
- input clk,
- input signed [AWIDTH-1:0] ar, ai,
- input signed [BWIDTH-1:0] br, bi,
- output signed [AWIDTH+BWIDTH:0] pr, pi
- );
-
-reg signed [AWIDTH-1:0] ai_d, ai_dd, ai_ddd, ai_dddd ;
-reg signed [AWIDTH-1:0] ar_d, ar_dd, ar_ddd, ar_dddd ;
-reg signed [BWIDTH-1:0] bi_d, bi_dd, bi_ddd, br_d, br_dd, br_ddd ;
-reg signed [AWIDTH:0] addcommon ;
-reg signed [BWIDTH:0] addr, addi ;
-reg signed [AWIDTH+BWIDTH:0] mult0, multr, multi, pr_int, pi_int ;
-reg signed [AWIDTH+BWIDTH:0] common, commonr1, commonr2 ;
-
-always @(posedge clk)
- begin
- ar_d <= ar;
- ar_dd <= ar_d;
- ai_d <= ai;
- ai_dd <= ai_d;
- br_d <= br;
- br_dd <= br_d;
- br_ddd <= br_dd;
- bi_d <= bi;
- bi_dd <= bi_d;
- bi_ddd <= bi_dd;
- end
-
-// Common factor (ar ai) x bi, shared for the calculations of the real and imaginary final products
-//
-always @(posedge clk)
- begin
- addcommon <= ar_d - ai_d;
- mult0 <= addcommon * bi_dd;
- common <= mult0;
- end
-
-// Real product
-//
-always @(posedge clk)
- begin
- ar_ddd <= ar_dd;
- ar_dddd <= ar_ddd;
- addr <= br_ddd - bi_ddd;
- multr <= addr * ar_dddd;
- commonr1 <= common;
- pr_int <= multr + commonr1;
- end
-
-// Imaginary product
-//
-always @(posedge clk)
- begin
- ai_ddd <= ai_dd;
- ai_dddd <= ai_ddd;
- addi <= br_ddd + bi_ddd;
- multi <= addi * ai_dddd;
- commonr2 <= common;
- pi_int <= multi + commonr2;
- end
-
-assign pr = pr_int;
-assign pi = pi_int;
-
-endmodule // cmult
diff --git a/tests/xilinx_ug901/cmult.ys b/tests/xilinx_ug901/cmult.ys deleted file mode 100644 index 605f00983..000000000 --- a/tests/xilinx_ug901/cmult.ys +++ /dev/null @@ -1,31 +0,0 @@ -read_verilog cmult.v -hierarchy -top cmult -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 cmult -#Vivado synthesizes 3 DSP48E1, 68 FDRE. -select -assert-count 1 t:BUFG -select -assert-count 281 t:FDRE -select -assert-count 18 t:LUT1 -select -assert-count 467 t:LUT2 -select -assert-count 187 t:LUT3 -select -assert-count 98 t:LUT4 -select -assert-count 165 t:LUT5 -select -assert-count 1596 t:LUT6 -select -assert-count 222 t:MUXCY -select -assert-count 393 t:MUXF7 -select -assert-count 121 t:MUXF8 -select -assert-count 85 t:SRL16E -select -assert-count 230 t:XORCY - -select -assert-none t:BUFG t:FDRE t:LUT1 t:LUT2 t:LUT3 t:LUT4 t:LUT5 t:LUT6 t:MUXCY t:MUXF7 t:MUXF8 t:SRL16E t:XORCY %% t:* %D diff --git a/tests/xilinx_ug901/dynamic_shift_registers_1.v b/tests/xilinx_ug901/dynamic_shift_registers_1.v deleted file mode 100644 index b69c022cd..000000000 --- a/tests/xilinx_ug901/dynamic_shift_registers_1.v +++ /dev/null @@ -1,21 +0,0 @@ -// 32-bit dynamic shift register.
-// Download:
-// File: dynamic_shift_registers_1.v
-
-module dynamic_shift_register_1 (CLK, CE, SEL, SI, DO);
-parameter SELWIDTH = 5;
-input CLK, CE, SI;
-input [SELWIDTH-1:0] SEL;
-output DO;
-
-localparam DATAWIDTH = 2**SELWIDTH;
-reg [DATAWIDTH-1:0] data;
-
-assign DO = data[SEL];
-
-always @(posedge CLK)
- begin
- if (CE == 1'b1)
- data <= {data[DATAWIDTH-2:0], SI};
- end
-endmodule
diff --git a/tests/xilinx_ug901/dynamic_shift_registers_1.ys b/tests/xilinx_ug901/dynamic_shift_registers_1.ys deleted file mode 100644 index f70c84f2f..000000000 --- a/tests/xilinx_ug901/dynamic_shift_registers_1.ys +++ /dev/null @@ -1,15 +0,0 @@ -read_verilog dynamic_shift_registers_1.v -hierarchy -top dynamic_shift_register_1 -proc -flatten -#ERROR: Found 1 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 dynamic_shift_register_1 # Constrain all select calls below inside the top module -#Vivado synthesizes 1 BUFG, 3 SRLC32E. -stat -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/dynpreaddmultadd.v b/tests/xilinx_ug901/dynpreaddmultadd.v deleted file mode 100644 index e3bb3a86c..000000000 --- a/tests/xilinx_ug901/dynpreaddmultadd.v +++ /dev/null @@ -1,47 +0,0 @@ -// Pre-add/subtract select with Dynamic control
-// dynpreaddmultadd.v
-//Default parameters were changed because of slow test.
-//module dynpreaddmultadd # (parameter SIZEIN = 16)
-module dynpreaddmultadd # (parameter SIZEIN = 8)
- (
- input clk, ce, rst, subadd,
- input signed [SIZEIN-1:0] a, b, c, d,
- output signed [2*SIZEIN:0] dynpreaddmultadd_out
- );
-
-// Declare registers for intermediate values
-reg signed [SIZEIN-1:0] a_reg, b_reg, c_reg;
-reg signed [SIZEIN:0] add_reg;
-reg signed [2*SIZEIN:0] d_reg, m_reg, p_reg;
-
-always @(posedge clk)
-begin
- if (rst)
- begin
- a_reg <= 0;
- b_reg <= 0;
- c_reg <= 0;
- d_reg <= 0;
- add_reg <= 0;
- m_reg <= 0;
- p_reg <= 0;
- end
- else if (ce)
- begin
- a_reg <= a;
- b_reg <= b;
- c_reg <= c;
- d_reg <= d;
- if (subadd)
- add_reg <= a_reg - b_reg;
- else
- add_reg <= a_reg + b_reg;
- m_reg <= add_reg * c_reg;
- p_reg <= m_reg + d_reg;
- end
-end
-
-// Output accumulation result
-assign dynpreaddmultadd_out = p_reg;
-
-endmodule // dynpreaddmultadd
diff --git a/tests/xilinx_ug901/dynpreaddmultadd.ys b/tests/xilinx_ug901/dynpreaddmultadd.ys deleted file mode 100644 index f74128dae..000000000 --- a/tests/xilinx_ug901/dynpreaddmultadd.ys +++ /dev/null @@ -1,31 +0,0 @@ -read_verilog dynpreaddmultadd.v -hierarchy -top dynpreaddmultadd -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 dynpreaddmultadd - -#Vivado synthesizes 1 DSP48E1. -select -assert-count 1 t:BUFG -select -assert-count 75 t:FDRE -select -assert-count 8 t:LUT1 -select -assert-count 131 t:LUT2 -select -assert-count 19 t:LUT3 -select -assert-count 26 t:LUT4 -select -assert-count 12 t:LUT5 -select -assert-count 142 t:LUT6 -select -assert-count 48 t:MUXCY -select -assert-count 50 t:MUXF7 -select -assert-count 15 t:MUXF8 -select -assert-count 52 t:XORCY - -select -assert-none t:BUFG t:FDRE t:LUT1 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/fsm_1.v b/tests/xilinx_ug901/fsm_1.v deleted file mode 100644 index ee3571d0d..000000000 --- a/tests/xilinx_ug901/fsm_1.v +++ /dev/null @@ -1,42 +0,0 @@ -// State Machine with single sequential block
-//fsm_1.v
-module fsm_1(clk,reset,flag,sm_out);
-input clk,reset,flag;
-output reg sm_out;
-
-parameter s1 = 3'b000;
-parameter s2 = 3'b001;
-parameter s3 = 3'b010;
-parameter s4 = 3'b011;
-parameter s5 = 3'b111;
-
-reg [2:0] state;
-
-always@(posedge clk)
- begin
- if(reset)
- begin
- state <= s1;
- sm_out <= 1'b1;
- end
- else
- begin
- case(state)
- s1: if(flag)
- begin
- state <= s2;
- sm_out <= 1'b1;
- end
- else
- begin
- state <= s3;
- sm_out <= 1'b0;
- end
- s2: begin state <= s4; sm_out <= 1'b0; end
- s3: begin state <= s4; sm_out <= 1'b0; end
- s4: begin state <= s5; sm_out <= 1'b1; end
- s5: begin state <= s1; sm_out <= 1'b1; end
- endcase
- end
- end
-endmodule
diff --git a/tests/xilinx_ug901/fsm_1.ys b/tests/xilinx_ug901/fsm_1.ys deleted file mode 100644 index 192966163..000000000 --- a/tests/xilinx_ug901/fsm_1.ys +++ /dev/null @@ -1,16 +0,0 @@ -read_verilog fsm_1.v -hierarchy -top fsm_1 -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 fsm_1 # Constrain all select calls below inside the top module -#Vivado synthesizes 2 LUT5, 2 LUT4, 1 LUT3, 4 FDRE. -stat -select -assert-count 1 t:BUFG -select -assert-count 4 t:FDRE -select -assert-count 2 t:LUT4 -select -assert-count 2 t:LUT5 -select -assert-count 1 t:LUT6 - -select -assert-none t:BUFG t:FDRE t:LUT4 t:LUT5 t:LUT6 %% t:* %D diff --git a/tests/xilinx_ug901/latches.v b/tests/xilinx_ug901/latches.v deleted file mode 100644 index 09d0f9f73..000000000 --- a/tests/xilinx_ug901/latches.v +++ /dev/null @@ -1,17 +0,0 @@ -// Latch with Positive Gate and Asynchronous Reset -// File: latches.v -module latches ( - input G, - input D, - input CLR, - output reg Q - ); -always @ * -begin - if(CLR) - Q = 0; - else if(G) - Q = D; -end - -endmodule diff --git a/tests/xilinx_ug901/latches.ys b/tests/xilinx_ug901/latches.ys deleted file mode 100644 index be4a8de94..000000000 --- a/tests/xilinx_ug901/latches.ys +++ /dev/null @@ -1,10 +0,0 @@ -read_verilog latches.v -proc -hierarchy -top latches -flatten -synth_xilinx -#Vivado synthesizes 1 BUFG, 8 LDCE. -select -assert-count 2 t:LUT2 -select -assert-count 1 t:$_DLATCH_P_ -#ERROR: Assertion failed: selection is not empty: t:LUT2 t:$_DLATCH_P_ %% t:* %D -#select -assert-none t:LUT2 t:$_DLATCH_P_ %% t:* %D diff --git a/tests/xilinx_ug901/macc.v b/tests/xilinx_ug901/macc.v deleted file mode 100644 index 9db8ea2c9..000000000 --- a/tests/xilinx_ug901/macc.v +++ /dev/null @@ -1,47 +0,0 @@ -// Signed 40-bit streaming accumulator with 16-bit inputs
-// File: macc.v
-//
-module macc # (
- //Default parameters were changed because of slow test
- // parameter SIZEIN = 16, SIZEOUT = 40
- // parameter SIZEIN = 12, SIZEOUT = 30
- parameter SIZEIN = 8, SIZEOUT = 20
- )
- (
- input clk, ce, sload,
- input signed [SIZEIN-1:0] a, b,
- output signed [SIZEOUT-1:0] accum_out
- );
-
- // Declare registers for intermediate values
-reg signed [SIZEIN-1:0] a_reg, b_reg;
-reg sload_reg;
-reg signed [2*SIZEIN:0] mult_reg;
-reg signed [SIZEOUT-1:0] adder_out, old_result;
-
-always @(adder_out or sload_reg)
-begin
- if (sload_reg)
- old_result <= 0;
- else
- // 'sload' is now active (=low) and opens the accumulation loop.
- // The accumulator takes the next multiplier output in
- // the same cycle.
- old_result <= adder_out;
-end
-
-always @(posedge clk)
- if (ce)
- begin
- a_reg <= a;
- b_reg <= b;
- mult_reg <= a_reg * b_reg;
- sload_reg <= sload;
- // Store accumulation result into a register
- adder_out <= old_result + mult_reg;
- end
-
-// Output accumulation result
-assign accum_out = adder_out;
-
-endmodule // macc
diff --git a/tests/xilinx_ug901/macc.ys b/tests/xilinx_ug901/macc.ys deleted file mode 100644 index 5a78a352c..000000000 --- a/tests/xilinx_ug901/macc.ys +++ /dev/null @@ -1,23 +0,0 @@ -read_verilog macc.v -hierarchy -top macc -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 macc -#Vivado synthesizes 1 DSP48E1, 1 FDRE. (When SIZEIN = 12, SIZEOUT = 30) -stat -select -assert-count 1 t:BUFG -select -assert-count 53 t:FDRE -select -assert-count 64 t:LUT2 -select -assert-count 10 t:LUT3 -select -assert-count 22 t:LUT4 -select -assert-count 14 t:LUT5 -select -assert-count 123 t:LUT6 -select -assert-count 34 t:MUXCY -select -assert-count 41 t:MUXF7 -select -assert-count 14 t:MUXF8 -select -assert-count 36 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/mult_unsigned.v b/tests/xilinx_ug901/mult_unsigned.v deleted file mode 100644 index 466c16cf8..000000000 --- a/tests/xilinx_ug901/mult_unsigned.v +++ /dev/null @@ -1,33 +0,0 @@ -// Unsigned 16x24-bit Multiplier
-// 1 latency stage on operands
-// 3 latency stage after the multiplication
-// File: multipliers2.v
-//
-module mult_unsigned (clk, A, B, RES);
-//Default parameters were changed because of slow test
-//parameter WIDTHA = 16;
-//parameter WIDTHB = 24;
-parameter WIDTHA = 8;
-parameter WIDTHB = 12;
-input clk;
-input [WIDTHA-1:0] A;
-input [WIDTHB-1:0] B;
-output [WIDTHA+WIDTHB-1:0] RES;
-
-reg [WIDTHA-1:0] rA;
-reg [WIDTHB-1:0] rB;
-reg [WIDTHA+WIDTHB-1:0] M [3:0];
-
-integer i;
-always @(posedge clk)
- begin
- rA <= A;
- rB <= B;
- M[0] <= rA * rB;
- for (i = 0; i < 3; i = i+1)
- M[i+1] <= M[i];
- end
-
-assign RES = M[3];
-
-endmodule
diff --git a/tests/xilinx_ug901/mult_unsigned.ys b/tests/xilinx_ug901/mult_unsigned.ys deleted file mode 100644 index a929ca3ad..000000000 --- a/tests/xilinx_ug901/mult_unsigned.ys +++ /dev/null @@ -1,29 +0,0 @@ -read_verilog mult_unsigned.v -hierarchy -top mult_unsigned -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 mult_unsigned - -#Vivado synthesizes 1 DSP48E1, 40 FDRE. -select -assert-count 1 t:BUFG -select -assert-count 20 t:FDRE -select -assert-count 33 t:LUT2 -select -assert-count 1 t:LUT3 -select -assert-count 11 t:LUT4 -select -assert-count 4 t:LUT5 -select -assert-count 139 t:LUT6 -select -assert-count 19 t:MUXCY -select -assert-count 35 t:MUXF7 -select -assert-count 20 t:SRL16E -select -assert-count 20 t:XORCY -select -assert-none t:BUFG t:FDRE t:LUT2 t:LUT3 t:LUT4 t:LUT5 t:LUT6 t:MUXCY t:MUXF7 t:SRL16E t:XORCY %% t:* %D diff --git a/tests/xilinx_ug901/presubmult.v b/tests/xilinx_ug901/presubmult.v deleted file mode 100644 index 30e6133ff..000000000 --- a/tests/xilinx_ug901/presubmult.v +++ /dev/null @@ -1,43 +0,0 @@ -//
-// Pre-adder support in subtract mode for DSP block
-// File: presubmult.v
-
-module presubmult # (//Default parameters were changed because of slow test
- // parameter SIZEIN = 16
- parameter SIZEIN = 8
- )
- (
- input clk, ce, rst,
- input signed [SIZEIN-1:0] a, b, c,
- output signed [2*SIZEIN:0] presubmult_out
- );
-
-// Declare registers for intermediate values
-reg signed [SIZEIN-1:0] a_reg, b_reg, c_reg;
-reg signed [SIZEIN:0] add_reg;
-reg signed [2*SIZEIN:0] m_reg, p_reg;
-
-always @(posedge clk)
- if (rst)
- begin
- a_reg <= 0;
- b_reg <= 0;
- c_reg <= 0;
- add_reg <= 0;
- m_reg <= 0;
- p_reg <= 0;
- end
- else if (ce)
- begin
- a_reg <= a;
- b_reg <= b;
- c_reg <= c;
- add_reg <= a - b;
- m_reg <= add_reg * c_reg;
- p_reg <= m_reg;
- end
-
-// Output accumulation result
-assign presubmult_out = p_reg;
-
-endmodule // presubmult
diff --git a/tests/xilinx_ug901/presubmult.ys b/tests/xilinx_ug901/presubmult.ys deleted file mode 100644 index 831458dec..000000000 --- a/tests/xilinx_ug901/presubmult.ys +++ /dev/null @@ -1,23 +0,0 @@ -read_verilog presubmult.v -hierarchy -top presubmult -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 presubmult -#Vivado synthesizes 1 DSP48E1. (When SIZEIN = 8) -stat -select -assert-count 1 t:BUFG -select -assert-count 51 t:FDRE -select -assert-count 75 t:LUT2 -select -assert-count 10 t:LUT3 -select -assert-count 24 t:LUT4 -select -assert-count 15 t:LUT5 -select -assert-count 136 t:LUT6 -select -assert-count 24 t:MUXCY -select -assert-count 46 t:MUXF7 -select -assert-count 14 t:MUXF8 -select -assert-count 26 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/ram_simple_dual_one_clock.v b/tests/xilinx_ug901/ram_simple_dual_one_clock.v deleted file mode 100644 index 3390e2da5..000000000 --- a/tests/xilinx_ug901/ram_simple_dual_one_clock.v +++ /dev/null @@ -1,25 +0,0 @@ -// Simple Dual-Port Block RAM with One Clock
-// File: simple_dual_one_clock.v
-
-module simple_dual_one_clock (clk,ena,enb,wea,addra,addrb,dia,dob);
-
-input clk,ena,enb,wea;
-input [9:0] addra,addrb;
-input [15:0] dia;
-output [15:0] dob;
-reg [15:0] ram [1023:0];
-reg [15:0] doa,dob;
-
-always @(posedge clk) begin
- if (ena) begin
- if (wea)
- ram[addra] <= dia;
- end
-end
-
-always @(posedge clk) begin
- if (enb)
- dob <= ram[addrb];
-end
-
-endmodule
\ No newline at end of file diff --git a/tests/xilinx_ug901/ram_simple_dual_one_clock.ys b/tests/xilinx_ug901/ram_simple_dual_one_clock.ys deleted file mode 100644 index c1bde951e..000000000 --- a/tests/xilinx_ug901/ram_simple_dual_one_clock.ys +++ /dev/null @@ -1,20 +0,0 @@ -read_verilog ram_simple_dual_one_clock.v -hierarchy -top simple_dual_one_clock -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 simple_dual_one_clock -#Vivado synthesizes 1 RAMB18E1. -select -assert-count 1 t:BUFG -select -assert-count 1 t:LUT2 -select -assert-count 1 t:RAMB18E1 - -select -assert-none t:BUFG t:LUT2 t:RAMB18E1 %% t:* %D diff --git a/tests/xilinx_ug901/ram_simple_dual_two_clocks.v b/tests/xilinx_ug901/ram_simple_dual_two_clocks.v deleted file mode 100644 index 1113b928e..000000000 --- a/tests/xilinx_ug901/ram_simple_dual_two_clocks.v +++ /dev/null @@ -1,30 +0,0 @@ -// Simple Dual-Port Block RAM with Two Clocks
-// File: simple_dual_two_clocks.v
-
-module simple_dual_two_clocks (clka,clkb,ena,enb,wea,addra,addrb,dia,dob);
-
-input clka,clkb,ena,enb,wea;
-input [9:0] addra,addrb;
-input [15:0] dia;
-output [15:0] dob;
-reg [15:0] ram [1023:0];
-reg [15:0] dob;
-
-always @(posedge clka)
-begin
- if (ena)
- begin
- if (wea)
- ram[addra] <= dia;
- end
-end
-
-always @(posedge clkb)
-begin
- if (enb)
- begin
- dob <= ram[addrb];
- end
-end
-
-endmodule
diff --git a/tests/xilinx_ug901/ram_simple_dual_two_clocks.ys b/tests/xilinx_ug901/ram_simple_dual_two_clocks.ys deleted file mode 100644 index db0d789e9..000000000 --- a/tests/xilinx_ug901/ram_simple_dual_two_clocks.ys +++ /dev/null @@ -1,20 +0,0 @@ -read_verilog ram_simple_dual_two_clocks.v -hierarchy -top simple_dual_two_clocks -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 simple_dual_two_clocks -#Vivado synthesizes 1 RAMB18E1. -select -assert-count 2 t:BUFG -select -assert-count 1 t:LUT2 -select -assert-count 1 t:RAMB18E1 - -select -assert-none t:BUFG t:LUT2 t:RAMB18E1 %% t:* %D diff --git a/tests/xilinx_ug901/rams_dist.v b/tests/xilinx_ug901/rams_dist.v deleted file mode 100644 index 405283b69..000000000 --- a/tests/xilinx_ug901/rams_dist.v +++ /dev/null @@ -1,24 +0,0 @@ -// Dual-Port RAM with Asynchronous Read (Distributed RAM)
-// File: rams_dist.v
-
-module rams_dist (clk, we, a, dpra, di, spo, dpo);
-
-input clk;
-input we;
-input [5:0] a;
-input [5:0] dpra;
-input [15:0] di;
-output [15:0] spo;
-output [15:0] dpo;
-reg [15:0] ram [63:0];
-
-always @(posedge clk)
-begin
- if (we)
- ram[a] <= di;
-end
-
-assign spo = ram[a];
-assign dpo = ram[dpra];
-
-endmodule
diff --git a/tests/xilinx_ug901/rams_dist.ys b/tests/xilinx_ug901/rams_dist.ys deleted file mode 100644 index 0aa1a8309..000000000 --- a/tests/xilinx_ug901/rams_dist.ys +++ /dev/null @@ -1,21 +0,0 @@ -read_verilog rams_dist.v -hierarchy -top rams_dist -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 rams_dist -stat -#Vivado synthesizes 32 RAM64X1D. -select -assert-count 1 t:BUFG -select -assert-count 32 t:RAM64X1D - -select -assert-none t:BUFG t:RAM64X1D %% t:* %D diff --git a/tests/xilinx_ug901/rams_init_file.data b/tests/xilinx_ug901/rams_init_file.data deleted file mode 100644 index f14f0b324..000000000 --- a/tests/xilinx_ug901/rams_init_file.data +++ /dev/null @@ -1,64 +0,0 @@ -00001110110000011001111011000110 -00101011001011010101001000100011 -01110100010100011000011100001111 -01000001010000100101001110010100 -00001001101001111111101000101011 -00101101001011111110101010100111 -11101111000100111000111101101101 -10001111010010011001000011101111 -00000001100011100011110010011111 -11011111001110101011111001001010 -11100111010100111110110011001010 -11000100001001101100111100101001 -10001011100101011111111111100001 -11110101110110010000010110111010 -01001011000000111001010110101110 -11100001111111001010111010011110 -01101111011010010100001101110001 -01010100011011111000011000100100 -11110000111101101111001100001011 -10101101001111010100100100011100 -01011100001010111111101110101110 -01011101000100100111010010110101 -11110111000100000101011101101101 -11100111110001111010101100001101 -01110100000011101111111000011111 -00010011110101111000111001011101 -01101110001111100011010101101111 -10111100000000010011101011011011 -11000001001101001101111100010000 -00011111110010110110011111010101 -01100100100000011100100101110000 -10001000000100111011001010001111 -11001000100011101001010001100001 -10000000100111010011100111100011 -11011111010010100010101010000111 -10000000110111101000111110111011 -10110011010111101111000110011001 -00010111100001001010110111011100 -10011100101110101111011010110011 -01010011101101010001110110011010 -01111011011100010101000101000001 -10001000000110010110111001101010 -11101000001101010000111001010110 -11100011111100000111110101110101 -01001010000000001111111101101111 -00100011000011001000000010001111 -10011000111010110001001011100100 -11111111111011110101000101000111 -11000011000101000011100110100000 -01101101001011111010100011101001 -10000111101100101001110011010111 -11010110100100101110110010100100 -01001111111001101101011111001011 -11011001001101110110000100110111 -10110110110111100101110011100110 -10011100111001000010111111010110 -00000000001011011111001010110010 -10100110011010000010001000011011 -11001010111111001001110001110101 -00100001100010000111000101001000 -00111100101111110001101101111010 -11000010001010000000010100100001 -11000001000110001101000101001110 -10010011010100010001100100100111 diff --git a/tests/xilinx_ug901/rams_init_file.v b/tests/xilinx_ug901/rams_init_file.v deleted file mode 100644 index 046779af9..000000000 --- a/tests/xilinx_ug901/rams_init_file.v +++ /dev/null @@ -1,24 +0,0 @@ -// Initializing Block RAM from external data file
-// Binary data
-// File: rams_init_file.v
-
-module rams_init_file (clk, we, addr, din, dout);
-input clk;
-input we;
-input [5:0] addr;
-input [31:0] din;
-output [31:0] dout;
-
-reg [31:0] ram [0:63];
-reg [31:0] dout;
-
-initial begin
-$readmemb("rams_init_file.data",ram);
-end
-
-always @(posedge clk)
-begin
- if (we)
- ram[addr] <= din;
- dout <= ram[addr];
-end endmodule
diff --git a/tests/xilinx_ug901/rams_init_file.ys b/tests/xilinx_ug901/rams_init_file.ys deleted file mode 100644 index d22a0f52c..000000000 --- a/tests/xilinx_ug901/rams_init_file.ys +++ /dev/null @@ -1,22 +0,0 @@ -read_verilog rams_init_file.v -hierarchy -top rams_init_file -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 rams_init_file -stat -#Vivado synthesizes 1 RAMB18E1. -select -assert-count 1 t:BUFG -select -assert-count 32 t:FDRE -select -assert-count 32 t:RAM64X1D - -select -assert-none t:BUFG t:FDRE t:RAM64X1D %% t:* %D diff --git a/tests/xilinx_ug901/rams_pipeline.v b/tests/xilinx_ug901/rams_pipeline.v deleted file mode 100644 index e86d417f5..000000000 --- a/tests/xilinx_ug901/rams_pipeline.v +++ /dev/null @@ -1,42 +0,0 @@ -// Block RAM with Optional Output Registers
-// File: rams_pipeline
-
-module rams_pipeline (clk1, clk2, we, en1, en2, addr1, addr2, di, res1, res2);
-input clk1;
-input clk2;
-input we, en1, en2;
-input [9:0] addr1;
-input [9:0] addr2;
-input [15:0] di;
-output [15:0] res1;
-output [15:0] res2;
-reg [15:0] res1;
-reg [15:0] res2;
-reg [15:0] RAM [1023:0];
-reg [15:0] do1;
-reg [15:0] do2;
-
-always @(posedge clk1)
-begin
- if (we == 1'b1)
- RAM[addr1] <= di;
- do1 <= RAM[addr1];
-end
-
-always @(posedge clk2)
-begin
- do2 <= RAM[addr2];
-end
-
-always @(posedge clk1)
-begin
- if (en1 == 1'b1)
- res1 <= do1;
-end
-
-always @(posedge clk2)
-begin
- if (en2 == 1'b1)
- res2 <= do2;
-end
-endmodule
diff --git a/tests/xilinx_ug901/rams_pipeline.ys b/tests/xilinx_ug901/rams_pipeline.ys deleted file mode 100644 index 7fd7c76e4..000000000 --- a/tests/xilinx_ug901/rams_pipeline.ys +++ /dev/null @@ -1,22 +0,0 @@ -read_verilog rams_pipeline.v -hierarchy -top rams_pipeline -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 rams_pipeline -stat -#Vivado synthesizes 1 RAMB18E1. -select -assert-count 2 t:BUFG -select -assert-count 32 t:FDRE -select -assert-count 2 t:RAMB18E1 - -select -assert-none t:BUFG t:FDRE t:RAMB18E1 %% t:* %D diff --git a/tests/xilinx_ug901/rams_sp_nc.v b/tests/xilinx_ug901/rams_sp_nc.v deleted file mode 100644 index 08abc0d2c..000000000 --- a/tests/xilinx_ug901/rams_sp_nc.v +++ /dev/null @@ -1,26 +0,0 @@ -// Single-Port Block RAM No-Change Mode
-// File: rams_sp_nc.v
-
-module rams_sp_nc (clk, we, en, addr, di, dout);
-
-input clk;
-input we;
-input en;
-input [9:0] addr;
-input [15:0] di;
-output [15:0] dout;
-
-reg [15:0] RAM [1023:0];
-reg [15:0] dout;
-
-always @(posedge clk)
-begin
- if (en)
- begin
- if (we)
- RAM[addr] <= di;
- else
- dout <= RAM[addr];
- end
-end
-endmodule
diff --git a/tests/xilinx_ug901/rams_sp_nc.ys b/tests/xilinx_ug901/rams_sp_nc.ys deleted file mode 100644 index 9b7d6386f..000000000 --- a/tests/xilinx_ug901/rams_sp_nc.ys +++ /dev/null @@ -1,22 +0,0 @@ -read_verilog rams_sp_nc.v -hierarchy -top rams_sp_nc -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 rams_sp_nc -stat -#Vivado synthesizes 1 RAMB18E1. -select -assert-count 1 t:BUFG -select -assert-count 2 t:LUT2 -select -assert-count 1 t:RAMB18E1 - -select -assert-none t:BUFG t:LUT2 t:RAMB18E1 %% t:* %D diff --git a/tests/xilinx_ug901/rams_sp_rf.v b/tests/xilinx_ug901/rams_sp_rf.v deleted file mode 100644 index 5e0adf88b..000000000 --- a/tests/xilinx_ug901/rams_sp_rf.v +++ /dev/null @@ -1,26 +0,0 @@ -// Single-Port Block RAM Read-First Mode
-// rams_sp_rf.v
-module rams_sp_rf (clk, en, we, addr, di, dout);
-
-input clk;
-input we;
-input en;
-input [9:0] addr;
-input [15:0] di;
-output [15:0] dout;
-
-reg [15:0] RAM [1023:0];
-reg [15:0] dout;
-
-always @(posedge clk)
-begin
- if (en)
- begin
- if (we)
- RAM[addr]<=di;
- dout <= RAM[addr];
- end
-end
-
-endmodule
-
diff --git a/tests/xilinx_ug901/rams_sp_rf.ys b/tests/xilinx_ug901/rams_sp_rf.ys deleted file mode 100644 index 56f345c63..000000000 --- a/tests/xilinx_ug901/rams_sp_rf.ys +++ /dev/null @@ -1,22 +0,0 @@ -read_verilog rams_sp_rf.v -hierarchy -top rams_sp_rf -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 rams_sp_rf -stat -#Vivado synthesizes 1 RAMB18E1. -select -assert-count 1 t:BUFG -select -assert-count 1 t:LUT2 -select -assert-count 1 t:RAMB18E1 - -select -assert-none t:BUFG t:LUT2 t:RAMB18E1 %% t:* %D diff --git a/tests/xilinx_ug901/rams_sp_rf_rst.v b/tests/xilinx_ug901/rams_sp_rf_rst.v deleted file mode 100644 index cb8d50c4c..000000000 --- a/tests/xilinx_ug901/rams_sp_rf_rst.v +++ /dev/null @@ -1,29 +0,0 @@ -// Block RAM with Resettable Data Output
-// File: rams_sp_rf_rst.v
-
-module rams_sp_rf_rst (clk, en, we, rst, addr, di, dout);
-input clk;
-input en;
-input we;
-input rst;
-input [9:0] addr;
-input [15:0] di;
-output [15:0] dout;
-
-reg [15:0] ram [1023:0];
-reg [15:0] dout;
-
-always @(posedge clk)
-begin
- if (en) //optional enable
- begin
- if (we) //write enable
- ram[addr] <= di;
- if (rst) //optional reset
- dout <= 0;
- else
- dout <= ram[addr];
- end
-end
-
-endmodule
diff --git a/tests/xilinx_ug901/rams_sp_rf_rst.ys b/tests/xilinx_ug901/rams_sp_rf_rst.ys deleted file mode 100644 index 57e4df9f5..000000000 --- a/tests/xilinx_ug901/rams_sp_rf_rst.ys +++ /dev/null @@ -1,28 +0,0 @@ -read_verilog rams_sp_rf_rst.v -hierarchy -top rams_sp_rf_rst -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 rams_sp_rf_rst -stat -#Vivado synthesizes 1 RAMB18E1. - -select -assert-count 1 t:BUFG -select -assert-count 16 t:FDRE -select -assert-count 5 t:LUT2 -select -assert-count 4 t:LUT3 -select -assert-count 13 t:LUT4 -select -assert-count 23 t:LUT5 -select -assert-count 32 t:LUT6 -select -assert-count 128 t:RAM128X1D - -select -assert-none t:BUFG t:FDRE t:LUT2 t:LUT3 t:LUT4 t:LUT5 t:LUT6 t:RAM128X1D %% t:* %D diff --git a/tests/xilinx_ug901/rams_sp_rom.v b/tests/xilinx_ug901/rams_sp_rom.v deleted file mode 100644 index b6e05f6c8..000000000 --- a/tests/xilinx_ug901/rams_sp_rom.v +++ /dev/null @@ -1,46 +0,0 @@ -// Initializing Block RAM (Single-Port Block RAM)
-// File: rams_sp_rom
-module rams_sp_rom (clk, we, addr, di, dout);
-input clk;
-input we;
-input [5:0] addr;
-input [19:0] di;
-output [19:0] dout;
-
-reg [19:0] ram [63:0];
-reg [19:0] dout;
-
-initial
-begin
- ram[63] = 20'h0200A; ram[62] = 20'h00300; ram[61] = 20'h08101;
- ram[60] = 20'h04000; ram[59] = 20'h08601; ram[58] = 20'h0233A;
- ram[57] = 20'h00300; ram[56] = 20'h08602; ram[55] = 20'h02310;
- ram[54] = 20'h0203B; ram[53] = 20'h08300; ram[52] = 20'h04002;
- ram[51] = 20'h08201; ram[50] = 20'h00500; ram[49] = 20'h04001;
- ram[48] = 20'h02500; ram[47] = 20'h00340; ram[46] = 20'h00241;
- ram[45] = 20'h04002; ram[44] = 20'h08300; ram[43] = 20'h08201;
- ram[42] = 20'h00500; ram[41] = 20'h08101; ram[40] = 20'h00602;
- ram[39] = 20'h04003; ram[38] = 20'h0241E; ram[37] = 20'h00301;
- ram[36] = 20'h00102; ram[35] = 20'h02122; ram[34] = 20'h02021;
- ram[33] = 20'h00301; ram[32] = 20'h00102; ram[31] = 20'h02222;
- ram[30] = 20'h04001; ram[29] = 20'h00342; ram[28] = 20'h0232B;
- ram[27] = 20'h00900; ram[26] = 20'h00302; ram[25] = 20'h00102;
- ram[24] = 20'h04002; ram[23] = 20'h00900; ram[22] = 20'h08201;
- ram[21] = 20'h02023; ram[20] = 20'h00303; ram[19] = 20'h02433;
- ram[18] = 20'h00301; ram[17] = 20'h04004; ram[16] = 20'h00301;
- ram[15] = 20'h00102; ram[14] = 20'h02137; ram[13] = 20'h02036;
- ram[12] = 20'h00301; ram[11] = 20'h00102; ram[10] = 20'h02237;
- ram[9] = 20'h04004; ram[8] = 20'h00304; ram[7] = 20'h04040;
- ram[6] = 20'h02500; ram[5] = 20'h02500; ram[4] = 20'h02500;
- ram[3] = 20'h0030D; ram[2] = 20'h02341; ram[1] = 20'h08201;
- ram[0] = 20'h0400D;
-end
-
-always @(posedge clk)
-begin
- if (we)
- ram[addr] <= di;
- dout <= ram[addr];
-end
-
-endmodule
diff --git a/tests/xilinx_ug901/rams_sp_rom.ys b/tests/xilinx_ug901/rams_sp_rom.ys deleted file mode 100644 index bb8680df0..000000000 --- a/tests/xilinx_ug901/rams_sp_rom.ys +++ /dev/null @@ -1,22 +0,0 @@ -read_verilog rams_sp_rom.v -hierarchy -top rams_sp_rom -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 rams_sp_rom -stat -#Vivado synthesizes 1 RAMB18E1. -select -assert-count 1 t:BUFG -select -assert-count 20 t:RAM64X1D -select -assert-count 20 t:FDRE - -select -assert-none t:BUFG t:RAM64X1D t:FDRE %% t:* %D diff --git a/tests/xilinx_ug901/rams_sp_rom_1.v b/tests/xilinx_ug901/rams_sp_rom_1.v deleted file mode 100644 index b3b8e89fe..000000000 --- a/tests/xilinx_ug901/rams_sp_rom_1.v +++ /dev/null @@ -1,53 +0,0 @@ -// ROMs Using Block RAM Resources.
-// File: rams_sp_rom_1.v
-//
-module rams_sp_rom_1 (clk, en, addr, dout);
-input clk;
-input en;
-input [5:0] addr;
-output [19:0] dout;
-
-(*rom_style = "block" *) reg [19:0] data;
-
-always @(posedge clk)
-begin
- if (en)
- case(addr)
- 6'b000000: data <= 20'h0200A; 6'b100000: data <= 20'h02222;
- 6'b000001: data <= 20'h00300; 6'b100001: data <= 20'h04001;
- 6'b000010: data <= 20'h08101; 6'b100010: data <= 20'h00342;
- 6'b000011: data <= 20'h04000; 6'b100011: data <= 20'h0232B;
- 6'b000100: data <= 20'h08601; 6'b100100: data <= 20'h00900;
- 6'b000101: data <= 20'h0233A; 6'b100101: data <= 20'h00302;
- 6'b000110: data <= 20'h00300; 6'b100110: data <= 20'h00102;
- 6'b000111: data <= 20'h08602; 6'b100111: data <= 20'h04002;
- 6'b001000: data <= 20'h02310; 6'b101000: data <= 20'h00900;
- 6'b001001: data <= 20'h0203B; 6'b101001: data <= 20'h08201;
- 6'b001010: data <= 20'h08300; 6'b101010: data <= 20'h02023;
- 6'b001011: data <= 20'h04002; 6'b101011: data <= 20'h00303;
- 6'b001100: data <= 20'h08201; 6'b101100: data <= 20'h02433;
- 6'b001101: data <= 20'h00500; 6'b101101: data <= 20'h00301;
- 6'b001110: data <= 20'h04001; 6'b101110: data <= 20'h04004;
- 6'b001111: data <= 20'h02500; 6'b101111: data <= 20'h00301;
- 6'b010000: data <= 20'h00340; 6'b110000: data <= 20'h00102;
- 6'b010001: data <= 20'h00241; 6'b110001: data <= 20'h02137;
- 6'b010010: data <= 20'h04002; 6'b110010: data <= 20'h02036;
- 6'b010011: data <= 20'h08300; 6'b110011: data <= 20'h00301;
- 6'b010100: data <= 20'h08201; 6'b110100: data <= 20'h00102;
- 6'b010101: data <= 20'h00500; 6'b110101: data <= 20'h02237;
- 6'b010110: data <= 20'h08101; 6'b110110: data <= 20'h04004;
- 6'b010111: data <= 20'h00602; 6'b110111: data <= 20'h00304;
- 6'b011000: data <= 20'h04003; 6'b111000: data <= 20'h04040;
- 6'b011001: data <= 20'h0241E; 6'b111001: data <= 20'h02500;
- 6'b011010: data <= 20'h00301; 6'b111010: data <= 20'h02500;
- 6'b011011: data <= 20'h00102; 6'b111011: data <= 20'h02500;
- 6'b011100: data <= 20'h02122; 6'b111100: data <= 20'h0030D;
- 6'b011101: data <= 20'h02021; 6'b111101: data <= 20'h02341;
- 6'b011110: data <= 20'h00301; 6'b111110: data <= 20'h08201;
- 6'b011111: data <= 20'h00102; 6'b111111: data <= 20'h0400D;
- endcase
-end
-
-assign dout = data;
-
-endmodule
diff --git a/tests/xilinx_ug901/rams_sp_rom_1.ys b/tests/xilinx_ug901/rams_sp_rom_1.ys deleted file mode 100644 index 4285df1f8..000000000 --- a/tests/xilinx_ug901/rams_sp_rom_1.ys +++ /dev/null @@ -1,22 +0,0 @@ -read_verilog rams_sp_rom_1.v -hierarchy -top rams_sp_rom_1 -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 rams_sp_rom_1 -stat -#Vivado synthesizes 1 RAMB18E1. -select -assert-count 1 t:BUFG -select -assert-count 14 t:LUT6 -select -assert-count 14 t:FDRE - -select -assert-none t:BUFG t:LUT6 t:FDRE %% t:* %D diff --git a/tests/xilinx_ug901/rams_sp_wf.v b/tests/xilinx_ug901/rams_sp_wf.v deleted file mode 100644 index 55ed6bd54..000000000 --- a/tests/xilinx_ug901/rams_sp_wf.v +++ /dev/null @@ -1,26 +0,0 @@ -// Single-Port Block RAM Write-First Mode (recommended template)
-// File: rams_sp_wf.v
-module rams_sp_wf (clk, we, en, addr, di, dout);
-input clk;
-input we;
-input en;
-input [9:0] addr;
-input [15:0] di;
-output [15:0] dout;
-reg [15:0] RAM [1023:0];
-reg [15:0] dout;
-
-always @(posedge clk)
-begin
- if (en)
- begin
- if (we)
- begin
- RAM[addr] <= di;
- dout <= di;
- end
- else
- dout <= RAM[addr];
- end
-end
-endmodule
diff --git a/tests/xilinx_ug901/rams_sp_wf.ys b/tests/xilinx_ug901/rams_sp_wf.ys deleted file mode 100644 index 4d9a9cfea..000000000 --- a/tests/xilinx_ug901/rams_sp_wf.ys +++ /dev/null @@ -1,26 +0,0 @@ -read_verilog rams_sp_wf.v -hierarchy -top rams_sp_wf -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 rams_sp_wf -stat -#Vivado synthesizes 1 RAMB18E1. - -select -assert-count 1 t:BUFG -select -assert-count 16 t:FDRE -select -assert-count 44 t:LUT5 -select -assert-count 38 t:LUT6 -select -assert-count 10 t:MUXF7 -select -assert-count 128 t:RAM128X1D - -select -assert-none t:BUFG t:LUT2 t:FDRE t:LUT5 t:LUT6 t:MUXF7 t:RAM128X1D %% t:* %D diff --git a/tests/xilinx_ug901/rams_tdp_rf_rf.v b/tests/xilinx_ug901/rams_tdp_rf_rf.v deleted file mode 100644 index 63899226f..000000000 --- a/tests/xilinx_ug901/rams_tdp_rf_rf.v +++ /dev/null @@ -1,33 +0,0 @@ -// Dual-Port Block RAM with Two Write Ports
-// File: rams_tdp_rf_rf.v
-
-module rams_tdp_rf_rf (clka,clkb,ena,enb,wea,web,addra,addrb,dia,dib,doa,dob);
-
-input clka,clkb,ena,enb,wea,web;
-input [9:0] addra,addrb;
-input [15:0] dia,dib;
-output [15:0] doa,dob;
-reg [15:0] ram [1023:0];
-reg [15:0] doa,dob;
-
-always @(posedge clka)
-begin
- if (ena)
- begin
- if (wea)
- ram[addra] <= dia;
- doa <= ram[addra];
- end
-end
-
-always @(posedge clkb)
-begin
- if (enb)
- begin
- if (web)
- ram[addrb] <= dib;
- dob <= ram[addrb];
- end
-end
-
-endmodule
diff --git a/tests/xilinx_ug901/rams_tdp_rf_rf.ys b/tests/xilinx_ug901/rams_tdp_rf_rf.ys deleted file mode 100644 index 20cf4fdcc..000000000 --- a/tests/xilinx_ug901/rams_tdp_rf_rf.ys +++ /dev/null @@ -1,21 +0,0 @@ -read_verilog rams_tdp_rf_rf.v -hierarchy -top rams_tdp_rf_rf -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 rams_tdp_rf_rf -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/registers_1.v b/tests/xilinx_ug901/registers_1.v deleted file mode 100644 index beea6e666..000000000 --- a/tests/xilinx_ug901/registers_1.v +++ /dev/null @@ -1,25 +0,0 @@ -// 8-bit Register with
-// Rising-edge Clock
-// Active-high Synchronous Clear
-// Active-high Clock Enable
-// File: registers_1.v
-
-module registers_1(d_in,ce,clk,clr,dout);
-input [7:0] d_in;
-input ce;
-input clk;
-input clr;
-output [7:0] dout;
-reg [7:0] d_reg;
-
-always @ (posedge clk)
-begin
- if(clr)
- d_reg <= 8'b0;
- else if(ce)
- d_reg <= d_in;
-end
-
-assign dout = d_reg;
-endmodule
-
diff --git a/tests/xilinx_ug901/registers_1.ys b/tests/xilinx_ug901/registers_1.ys deleted file mode 100644 index 39ca894a2..000000000 --- a/tests/xilinx_ug901/registers_1.ys +++ /dev/null @@ -1,12 +0,0 @@ -read_verilog registers_1.v -hierarchy -top registers_1 -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 registers_1 # Constrain all select calls below inside the top module -#Vivado synthesizes 1 BUFG, 8 FDRE. -select -assert-count 1 t:BUFG -select -assert-count 8 t:FDRE -select -assert-count 9 t:LUT2 -select -assert-none t:BUFG t:FDRE t:LUT2 %% t:* %D diff --git a/tests/xilinx_ug901/run-test.sh b/tests/xilinx_ug901/run-test.sh deleted file mode 100755 index ea56b70f0..000000000 --- a/tests/xilinx_ug901/run-test.sh +++ /dev/null @@ -1,20 +0,0 @@ -#!/usr/bin/env bash -set -e -{ -echo "all::" -for x in *.ys; do - echo "all:: run-$x" - echo "run-$x:" - echo " @echo 'Running $x..'" - echo " @../../yosys -ql ${x%.ys}.log $x" -done -for s in *.sh; do - if [ "$s" != "run-test.sh" ]; then - echo "all:: run-$s" - echo "run-$s:" - echo " @echo 'Running $s..'" - echo " @bash $s" - fi -done -} > 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<<AWIDTH)-1:0]; // Memory Declaration
-reg [DWIDTH-1:0] memreg;
-reg [DWIDTH-1:0] mem_pipe_reg[NBPIPE-1:0]; // Pipelines for memory
-reg mem_en_pipe_reg[NBPIPE:0]; // Pipelines for memory enable
-
-integer i;
-
-// RAM : Read has one latency, Write has one latency as well.
-always @ (posedge clk)
-begin
- if(mem_en)
- begin
- if(we)
- mem[addr] <= din;
- else
- memreg <= mem[addr];
- end
-end
-// The enable of the RAM goes through a pipeline to produce a
-// series of pipelined enable signals required to control the data
-// pipeline.
-always @ (posedge clk)
-begin
-mem_en_pipe_reg[0] <= mem_en;
- for (i=0; i<NBPIPE; i=i+1)
- mem_en_pipe_reg[i+1] <= mem_en_pipe_reg[i];
-end
-
-// RAM output data goes through a pipeline.
-always @ (posedge clk)
-begin
- if (mem_en_pipe_reg[0])
- mem_pipe_reg[0] <= memreg;
-end
-
-always @ (posedge clk)
-begin
- for (i = 0; i < NBPIPE-1; i = i+1)
- if (mem_en_pipe_reg[i+1])
- mem_pipe_reg[i+1] <= mem_pipe_reg[i];
-end
-
-// Final output register gives user the option to add a reset and
-// an additional enable signal just for the data ouptut
-always @ (posedge clk)
-begin
- if (rst)
- dout <= 0;
- else if (mem_en_pipe_reg[NBPIPE] && regce)
- dout <= mem_pipe_reg[NBPIPE-1];
-end
-endmodule
-
diff --git a/tests/xilinx_ug901/xilinx_ultraram_single_port_no_change.ys b/tests/xilinx_ug901/xilinx_ultraram_single_port_no_change.ys deleted file mode 100644 index df3126e67..000000000 --- a/tests/xilinx_ug901/xilinx_ultraram_single_port_no_change.ys +++ /dev/null @@ -1,25 +0,0 @@ -read_verilog xilinx_ultraram_single_port_no_change.v -hierarchy -top xilinx_ultraram_single_port_no_change -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 xilinx_ultraram_single_port_no_change -stat -#Vivado synthesizes 1 RAMB36E1, 28 FDRE. -select -assert-count 1 t:BUFG -select -assert-count 53 t:FDRE -select -assert-count 1 t:LUT1 -select -assert-count 9 t:LUT2 -select -assert-count 11 t:LUT3 -select -assert-count 16 t:RAM128X1D - -select -assert-none t:BUFG t:FDRE t:LUT1 t:LUT2 t:LUT3 t:RAM128X1D %% t:* %D diff --git a/tests/xilinx_ug901/xilinx_ultraram_single_port_read_first.v b/tests/xilinx_ug901/xilinx_ultraram_single_port_read_first.v deleted file mode 100644 index d36c38fe1..000000000 --- a/tests/xilinx_ug901/xilinx_ultraram_single_port_read_first.v +++ /dev/null @@ -1,78 +0,0 @@ -// Xilinx UltraRAM Single Port Read First Mode. This code implements
-// a parameterizable UltraRAM block in read first mode. The behavior of this RAM is
-// when data is written, the old memory contents at the write address are
-// presented on the output port.
-//
-module xilinx_ultraram_single_port_read_first #(
-
-//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<<AWIDTH)-1:0]; // Memory Declaration
-reg [DWIDTH-1:0] memreg;
-reg [DWIDTH-1:0] mem_pipe_reg[NBPIPE-1:0]; // Pipelines for memory
-reg mem_en_pipe_reg[NBPIPE:0]; // Pipelines for memory enable
-
-integer i;
-
-// RAM : Both READ and WRITE have a latency of one
-always @ (posedge clk)
-begin
- if(mem_en)
- begin
- if(we)
- mem[addr] <= din;
- memreg <= mem[addr];
- end
-end
-
-// The enable of the RAM goes through a pipeline to produce a
-// series of pipelined enable signals required to control the data
-// pipeline.
-always @ (posedge clk)
-begin
- mem_en_pipe_reg[0] <= mem_en;
- for (i=0; i<NBPIPE; i=i+1)
- mem_en_pipe_reg[i+1] <= mem_en_pipe_reg[i];
-end
-
-// RAM output data goes through a pipeline.
-always @ (posedge clk)
-begin
- if (mem_en_pipe_reg[0])
- mem_pipe_reg[0] <= memreg;
-end
-
-always @ (posedge clk)
-begin
- for (i = 0; i < NBPIPE-1; i = i+1)
- if (mem_en_pipe_reg[i+1])
- mem_pipe_reg[i+1] <= mem_pipe_reg[i];
-end
-
-// Final output register gives user the option to add a reset and
-// an additional enable signal just for the data ouptut
-always @ (posedge clk)
-begin
- if (rst)
- dout <= 0;
- else if (mem_en_pipe_reg[NBPIPE] && regce)
- dout <= mem_pipe_reg[NBPIPE-1];
-end
-endmodule
diff --git a/tests/xilinx_ug901/xilinx_ultraram_single_port_read_first.ys b/tests/xilinx_ug901/xilinx_ultraram_single_port_read_first.ys deleted file mode 100644 index 4907d042d..000000000 --- a/tests/xilinx_ug901/xilinx_ultraram_single_port_read_first.ys +++ /dev/null @@ -1,24 +0,0 @@ -read_verilog xilinx_ultraram_single_port_read_first.v -hierarchy -top xilinx_ultraram_single_port_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 xilinx_ultraram_single_port_read_first -#Vivado synthesizes 1 RAMB18E1, 28 FDRE. -select -assert-count 1 t:BUFG -select -assert-count 53 t:FDRE -select -assert-count 1 t:LUT1 -select -assert-count 8 t:LUT2 -select -assert-count 11 t:LUT3 -select -assert-count 16 t:RAM128X1D - -select -assert-none t:BUFG t:FDRE t:LUT1 t:LUT2 t:LUT3 t:RAM128X1D %% t:* %D diff --git a/tests/xilinx_ug901/xilinx_ultraram_single_port_write_first.v b/tests/xilinx_ug901/xilinx_ultraram_single_port_write_first.v deleted file mode 100644 index 7985d3d4a..000000000 --- a/tests/xilinx_ug901/xilinx_ultraram_single_port_write_first.v +++ /dev/null @@ -1,82 +0,0 @@ -// Xilinx UltraRAM Single Port Write First Mode. This code implements
-// a parameterizable UltraRAM block in write first mode. The behavior of this RAM is
-// when data is written, the new memory contents at the write address are
-// presented on the output port.
-//
-module xilinx_ultraram_single_port_write_first #(
-
-//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<<AWIDTH)-1:0]; // Memory Declaration
-reg [DWIDTH-1:0] memreg;
-reg [DWIDTH-1:0] mem_pipe_reg[NBPIPE-1:0]; // Pipelines for memory
-reg mem_en_pipe_reg[NBPIPE:0]; // Pipelines for memory enable
-
-integer i;
-
-// RAM : Both READ and WRITE have a latency of one
-always @ (posedge clk)
-begin
- if(mem_en)
- begin
- if(we)
- begin
- mem[addr] <= din;
- memreg <= din;
- end
- else
- memreg <= mem[addr];
- end
-end
-
-// The enable of the RAM goes through a pipeline to produce a
-// series of pipelined enable signals required to control the data
-// pipeline.
-always @ (posedge clk)
-begin
- mem_en_pipe_reg[0] <= mem_en;
- for (i=0; i<NBPIPE; i=i+1)
- mem_en_pipe_reg[i+1] <= mem_en_pipe_reg[i];
-end
-
-// RAM output data goes through a pipeline.
-always @ (posedge clk)
-begin
- if (mem_en_pipe_reg[0])
- mem_pipe_reg[0] <= memreg;
-end
-
-always @ (posedge clk)
-begin
- for (i = 0; i < NBPIPE-1; i = i+1)
- if (mem_en_pipe_reg[i+1])
- mem_pipe_reg[i+1] <= mem_pipe_reg[i];
-end
-
-// Final output register gives user the option to add a reset and
-// an additional enable signal just for the data ouptut
-always @ (posedge clk)
-begin
- if (rst)
- dout <= 0;
- else if (mem_en_pipe_reg[NBPIPE] && regce)
- dout <= mem_pipe_reg[NBPIPE-1];
-end
-endmodule
diff --git a/tests/xilinx_ug901/xilinx_ultraram_single_port_write_first.ys b/tests/xilinx_ug901/xilinx_ultraram_single_port_write_first.ys deleted file mode 100644 index 9ca6b4d89..000000000 --- a/tests/xilinx_ug901/xilinx_ultraram_single_port_write_first.ys +++ /dev/null @@ -1,24 +0,0 @@ -read_verilog xilinx_ultraram_single_port_write_first.v -hierarchy -top xilinx_ultraram_single_port_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 xilinx_ultraram_single_port_write_first -#Vivado synthesizes 1 RAMB18E1, 28 FDRE. -select -assert-count 1 t:BUFG -select -assert-count 44 t:FDRE -select -assert-count 8 t:LUT5 -select -assert-count 8 t:LUT2 -select -assert-count 3 t:LUT3 -select -assert-count 16 t:RAM128X1D - -select -assert-none t:BUFG t:FDRE t:LUT5 t:LUT2 t:LUT3 t:RAM128X1D %% t:* %D |