diff options
| author | SergeyDegtyar <sndegtyar@gmail.com> | 2019-09-09 08:33:26 +0300 |
|---|---|---|
| committer | Miodrag Milanovic <mmicko@gmail.com> | 2019-10-17 17:08:38 +0200 |
| commit | 2ae7dec5300bb61a90842fefb1e846cd9f667a9e (patch) | |
| tree | 08dc91d97768a9dc657a298d87b06e31576cb06c /tests | |
| parent | 0d037bf9d8d866239de15d72dc8c5acd7ab5e5cf (diff) | |
| download | yosys-2ae7dec5300bb61a90842fefb1e846cd9f667a9e.tar.gz yosys-2ae7dec5300bb61a90842fefb1e846cd9f667a9e.tar.bz2 yosys-2ae7dec5300bb61a90842fefb1e846cd9f667a9e.zip | |
Add tests for Xilinx UG901 examples
Diffstat (limited to 'tests')
88 files changed, 2961 insertions, 0 deletions
diff --git a/tests/xilinx_ug901/asym_ram_sdp_read_wider.v b/tests/xilinx_ug901/asym_ram_sdp_read_wider.v new file mode 100644 index 000000000..0716dffdc --- /dev/null +++ b/tests/xilinx_ug901/asym_ram_sdp_read_wider.v @@ -0,0 +1,74 @@ +// 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 new file mode 100644 index 000000000..c63157cdf --- /dev/null +++ b/tests/xilinx_ug901/asym_ram_sdp_read_wider.ys @@ -0,0 +1,22 @@ +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 new file mode 100644 index 000000000..22d12d2ce --- /dev/null +++ b/tests/xilinx_ug901/asym_ram_sdp_write_wider.v @@ -0,0 +1,75 @@ +// 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 new file mode 100644 index 000000000..229d98df6 --- /dev/null +++ b/tests/xilinx_ug901/asym_ram_sdp_write_wider.ys @@ -0,0 +1,31 @@ +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 new file mode 100644 index 000000000..2b807a382 --- /dev/null +++ b/tests/xilinx_ug901/asym_ram_tdp_read_first.v @@ -0,0 +1,85 @@ +// 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 new file mode 100644 index 000000000..5f96b800c --- /dev/null +++ b/tests/xilinx_ug901/asym_ram_tdp_read_first.ys @@ -0,0 +1,21 @@ +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 new file mode 100644 index 000000000..90187ea26 --- /dev/null +++ b/tests/xilinx_ug901/asym_ram_tdp_write_first.v @@ -0,0 +1,92 @@ +// 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 new file mode 100644 index 000000000..bbe3cc849 --- /dev/null +++ b/tests/xilinx_ug901/asym_ram_tdp_write_first.ys @@ -0,0 +1,29 @@ +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 new file mode 100644 index 000000000..40caa1b10 --- /dev/null +++ b/tests/xilinx_ug901/black_box_1.v @@ -0,0 +1,19 @@ +// 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 new file mode 100644 index 000000000..acf0b5761 --- /dev/null +++ b/tests/xilinx_ug901/black_box_1.ys @@ -0,0 +1,15 @@ +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 new file mode 100644 index 000000000..46d86c297 --- /dev/null +++ b/tests/xilinx_ug901/bytewrite_ram_1b.v @@ -0,0 +1,42 @@ +// 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 new file mode 100644 index 000000000..4f0967801 --- /dev/null +++ b/tests/xilinx_ug901/bytewrite_ram_1b.ys @@ -0,0 +1,22 @@ +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 new file mode 100644 index 000000000..1093b0838 --- /dev/null +++ b/tests/xilinx_ug901/bytewrite_tdp_ram_nc.v @@ -0,0 +1,78 @@ +//
+// 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 new file mode 100644 index 000000000..b6818e322 --- /dev/null +++ b/tests/xilinx_ug901/bytewrite_tdp_ram_nc.ys @@ -0,0 +1,22 @@ +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 new file mode 100644 index 000000000..349aa2aec --- /dev/null +++ b/tests/xilinx_ug901/bytewrite_tdp_ram_readfirst2.v @@ -0,0 +1,71 @@ +// 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 new file mode 100644 index 000000000..3273d0d43 --- /dev/null +++ b/tests/xilinx_ug901/bytewrite_tdp_ram_readfirst2.ys @@ -0,0 +1,21 @@ +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 new file mode 100644 index 000000000..72dad9d8f --- /dev/null +++ b/tests/xilinx_ug901/bytewrite_tdp_ram_rf.v @@ -0,0 +1,61 @@ +// 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 new file mode 100644 index 000000000..2a34d9abe --- /dev/null +++ b/tests/xilinx_ug901/bytewrite_tdp_ram_rf.ys @@ -0,0 +1,21 @@ +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 new file mode 100644 index 000000000..d39565e52 --- /dev/null +++ b/tests/xilinx_ug901/bytewrite_tdp_ram_wf.v @@ -0,0 +1,68 @@ +// 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 new file mode 100644 index 000000000..b681d0c2b --- /dev/null +++ b/tests/xilinx_ug901/bytewrite_tdp_ram_wf.ys @@ -0,0 +1,23 @@ +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 new file mode 100644 index 000000000..038402daf --- /dev/null +++ b/tests/xilinx_ug901/cmacc.v @@ -0,0 +1,122 @@ +// 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 new file mode 100644 index 000000000..c1ac931c8 --- /dev/null +++ b/tests/xilinx_ug901/cmacc.ys @@ -0,0 +1,25 @@ +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 new file mode 100644 index 000000000..d5d85a28c --- /dev/null +++ b/tests/xilinx_ug901/cmult.v @@ -0,0 +1,71 @@ +//
+// 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 new file mode 100644 index 000000000..605f00983 --- /dev/null +++ b/tests/xilinx_ug901/cmult.ys @@ -0,0 +1,31 @@ +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 new file mode 100644 index 000000000..b69c022cd --- /dev/null +++ b/tests/xilinx_ug901/dynamic_shift_registers_1.v @@ -0,0 +1,21 @@ +// 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 new file mode 100644 index 000000000..994e12a3e --- /dev/null +++ b/tests/xilinx_ug901/dynamic_shift_registers_1.ys @@ -0,0 +1,15 @@ +read_verilog dynamic_shift_registers_1.v +hierarchy -top dynamic_shift_register_1 +proc +flatten + +#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 new file mode 100644 index 000000000..e3bb3a86c --- /dev/null +++ b/tests/xilinx_ug901/dynpreaddmultadd.v @@ -0,0 +1,47 @@ +// 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 new file mode 100644 index 000000000..f74128dae --- /dev/null +++ b/tests/xilinx_ug901/dynpreaddmultadd.ys @@ -0,0 +1,31 @@ +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 new file mode 100644 index 000000000..ee3571d0d --- /dev/null +++ b/tests/xilinx_ug901/fsm_1.v @@ -0,0 +1,42 @@ +// 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 new file mode 100644 index 000000000..192966163 --- /dev/null +++ b/tests/xilinx_ug901/fsm_1.ys @@ -0,0 +1,16 @@ +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 new file mode 100644 index 000000000..09d0f9f73 --- /dev/null +++ b/tests/xilinx_ug901/latches.v @@ -0,0 +1,17 @@ +// 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 new file mode 100644 index 000000000..be4a8de94 --- /dev/null +++ b/tests/xilinx_ug901/latches.ys @@ -0,0 +1,10 @@ +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 new file mode 100644 index 000000000..9db8ea2c9 --- /dev/null +++ b/tests/xilinx_ug901/macc.v @@ -0,0 +1,47 @@ +// 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 new file mode 100644 index 000000000..5a78a352c --- /dev/null +++ b/tests/xilinx_ug901/macc.ys @@ -0,0 +1,23 @@ +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 new file mode 100644 index 000000000..466c16cf8 --- /dev/null +++ b/tests/xilinx_ug901/mult_unsigned.v @@ -0,0 +1,33 @@ +// 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 new file mode 100644 index 000000000..a929ca3ad --- /dev/null +++ b/tests/xilinx_ug901/mult_unsigned.ys @@ -0,0 +1,29 @@ +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 new file mode 100644 index 000000000..30e6133ff --- /dev/null +++ b/tests/xilinx_ug901/presubmult.v @@ -0,0 +1,43 @@ +//
+// 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 new file mode 100644 index 000000000..831458dec --- /dev/null +++ b/tests/xilinx_ug901/presubmult.ys @@ -0,0 +1,23 @@ +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 new file mode 100644 index 000000000..3390e2da5 --- /dev/null +++ b/tests/xilinx_ug901/ram_simple_dual_one_clock.v @@ -0,0 +1,25 @@ +// 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 new file mode 100644 index 000000000..c1bde951e --- /dev/null +++ b/tests/xilinx_ug901/ram_simple_dual_one_clock.ys @@ -0,0 +1,20 @@ +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 new file mode 100644 index 000000000..1113b928e --- /dev/null +++ b/tests/xilinx_ug901/ram_simple_dual_two_clocks.v @@ -0,0 +1,30 @@ +// 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 new file mode 100644 index 000000000..db0d789e9 --- /dev/null +++ b/tests/xilinx_ug901/ram_simple_dual_two_clocks.ys @@ -0,0 +1,20 @@ +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 new file mode 100644 index 000000000..405283b69 --- /dev/null +++ b/tests/xilinx_ug901/rams_dist.v @@ -0,0 +1,24 @@ +// 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 new file mode 100644 index 000000000..0aa1a8309 --- /dev/null +++ b/tests/xilinx_ug901/rams_dist.ys @@ -0,0 +1,21 @@ +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 new file mode 100644 index 000000000..f14f0b324 --- /dev/null +++ b/tests/xilinx_ug901/rams_init_file.data @@ -0,0 +1,64 @@ +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 new file mode 100644 index 000000000..046779af9 --- /dev/null +++ b/tests/xilinx_ug901/rams_init_file.v @@ -0,0 +1,24 @@ +// 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 new file mode 100644 index 000000000..d22a0f52c --- /dev/null +++ b/tests/xilinx_ug901/rams_init_file.ys @@ -0,0 +1,22 @@ +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 new file mode 100644 index 000000000..e86d417f5 --- /dev/null +++ b/tests/xilinx_ug901/rams_pipeline.v @@ -0,0 +1,42 @@ +// 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 new file mode 100644 index 000000000..7fd7c76e4 --- /dev/null +++ b/tests/xilinx_ug901/rams_pipeline.ys @@ -0,0 +1,22 @@ +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 new file mode 100644 index 000000000..08abc0d2c --- /dev/null +++ b/tests/xilinx_ug901/rams_sp_nc.v @@ -0,0 +1,26 @@ +// 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 new file mode 100644 index 000000000..9b7d6386f --- /dev/null +++ b/tests/xilinx_ug901/rams_sp_nc.ys @@ -0,0 +1,22 @@ +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 new file mode 100644 index 000000000..5e0adf88b --- /dev/null +++ b/tests/xilinx_ug901/rams_sp_rf.v @@ -0,0 +1,26 @@ +// 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 new file mode 100644 index 000000000..56f345c63 --- /dev/null +++ b/tests/xilinx_ug901/rams_sp_rf.ys @@ -0,0 +1,22 @@ +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 new file mode 100644 index 000000000..cb8d50c4c --- /dev/null +++ b/tests/xilinx_ug901/rams_sp_rf_rst.v @@ -0,0 +1,29 @@ +// 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 new file mode 100644 index 000000000..57e4df9f5 --- /dev/null +++ b/tests/xilinx_ug901/rams_sp_rf_rst.ys @@ -0,0 +1,28 @@ +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 new file mode 100644 index 000000000..b6e05f6c8 --- /dev/null +++ b/tests/xilinx_ug901/rams_sp_rom.v @@ -0,0 +1,46 @@ +// 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 new file mode 100644 index 000000000..bb8680df0 --- /dev/null +++ b/tests/xilinx_ug901/rams_sp_rom.ys @@ -0,0 +1,22 @@ +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 new file mode 100644 index 000000000..b3b8e89fe --- /dev/null +++ b/tests/xilinx_ug901/rams_sp_rom_1.v @@ -0,0 +1,53 @@ +// 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 new file mode 100644 index 000000000..4285df1f8 --- /dev/null +++ b/tests/xilinx_ug901/rams_sp_rom_1.ys @@ -0,0 +1,22 @@ +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 new file mode 100644 index 000000000..55ed6bd54 --- /dev/null +++ b/tests/xilinx_ug901/rams_sp_wf.v @@ -0,0 +1,26 @@ +// 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 new file mode 100644 index 000000000..4d9a9cfea --- /dev/null +++ b/tests/xilinx_ug901/rams_sp_wf.ys @@ -0,0 +1,26 @@ +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 new file mode 100644 index 000000000..63899226f --- /dev/null +++ b/tests/xilinx_ug901/rams_tdp_rf_rf.v @@ -0,0 +1,33 @@ +// 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 new file mode 100644 index 000000000..20cf4fdcc --- /dev/null +++ b/tests/xilinx_ug901/rams_tdp_rf_rf.ys @@ -0,0 +1,21 @@ +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 new file mode 100644 index 000000000..beea6e666 --- /dev/null +++ b/tests/xilinx_ug901/registers_1.v @@ -0,0 +1,25 @@ +// 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 new file mode 100644 index 000000000..39ca894a2 --- /dev/null +++ b/tests/xilinx_ug901/registers_1.ys @@ -0,0 +1,12 @@ +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 new file mode 100755 index 000000000..ea56b70f0 --- /dev/null +++ b/tests/xilinx_ug901/run-test.sh @@ -0,0 +1,20 @@ +#!/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 new file mode 100644 index 000000000..a8b144bcd --- /dev/null +++ b/tests/xilinx_ug901/sfir_shifter.v @@ -0,0 +1,19 @@ +//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 new file mode 100644 index 000000000..b9fbeb8cb --- /dev/null +++ b/tests/xilinx_ug901/sfir_shifter.ys @@ -0,0 +1,16 @@ +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 new file mode 100644 index 000000000..77a3ec893 --- /dev/null +++ b/tests/xilinx_ug901/shift_registers_0.v @@ -0,0 +1,22 @@ +// 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 new file mode 100644 index 000000000..ae7d23a7f --- /dev/null +++ b/tests/xilinx_ug901/shift_registers_0.ys @@ -0,0 +1,13 @@ +read_verilog shift_registers_0.v +hierarchy -top shift_registers_0 +proc +flatten +#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 new file mode 100644 index 000000000..d50820e7b --- /dev/null +++ b/tests/xilinx_ug901/shift_registers_1.v @@ -0,0 +1,24 @@ +// 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 new file mode 100644 index 000000000..fb935c446 --- /dev/null +++ b/tests/xilinx_ug901/shift_registers_1.ys @@ -0,0 +1,14 @@ +read_verilog shift_registers_1.v +hierarchy -top shift_registers_1 +proc +flatten + +#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 new file mode 100644 index 000000000..6535b24c4 --- /dev/null +++ b/tests/xilinx_ug901/squarediffmacc.v @@ -0,0 +1,52 @@ +// 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 new file mode 100644 index 000000000..92474bea3 --- /dev/null +++ b/tests/xilinx_ug901/squarediffmacc.ys @@ -0,0 +1,23 @@ +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 new file mode 100644 index 000000000..0f41b67bc --- /dev/null +++ b/tests/xilinx_ug901/squarediffmult.v @@ -0,0 +1,42 @@ +// 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 new file mode 100644 index 000000000..3468e5bb4 --- /dev/null +++ b/tests/xilinx_ug901/squarediffmult.ys @@ -0,0 +1,30 @@ +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 new file mode 100644 index 000000000..c23c7491c --- /dev/null +++ b/tests/xilinx_ug901/top_mux.v @@ -0,0 +1,18 @@ +// 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 new file mode 100644 index 000000000..0245f3bbc --- /dev/null +++ b/tests/xilinx_ug901/top_mux.ys @@ -0,0 +1,13 @@ +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 new file mode 100644 index 000000000..0038a9989 --- /dev/null +++ b/tests/xilinx_ug901/tristates_1.v @@ -0,0 +1,17 @@ +// 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 new file mode 100644 index 000000000..7c13dc227 --- /dev/null +++ b/tests/xilinx_ug901/tristates_1.ys @@ -0,0 +1,13 @@ +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 new file mode 100644 index 000000000..0c70a1257 --- /dev/null +++ b/tests/xilinx_ug901/tristates_2.v @@ -0,0 +1,10 @@ +// 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 new file mode 100644 index 000000000..ba2e1d855 --- /dev/null +++ b/tests/xilinx_ug901/tristates_2.ys @@ -0,0 +1,13 @@ +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 new file mode 100644 index 000000000..f5e843dc9 --- /dev/null +++ b/tests/xilinx_ug901/xilinx_ultraram_single_port_no_change.v @@ -0,0 +1,78 @@ +// 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 new file mode 100644 index 000000000..df3126e67 --- /dev/null +++ b/tests/xilinx_ug901/xilinx_ultraram_single_port_no_change.ys @@ -0,0 +1,25 @@ +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 new file mode 100644 index 000000000..d36c38fe1 --- /dev/null +++ b/tests/xilinx_ug901/xilinx_ultraram_single_port_read_first.v @@ -0,0 +1,78 @@ +// 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 new file mode 100644 index 000000000..4907d042d --- /dev/null +++ b/tests/xilinx_ug901/xilinx_ultraram_single_port_read_first.ys @@ -0,0 +1,24 @@ +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 new file mode 100644 index 000000000..7985d3d4a --- /dev/null +++ b/tests/xilinx_ug901/xilinx_ultraram_single_port_write_first.v @@ -0,0 +1,82 @@ +// 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 new file mode 100644 index 000000000..9ca6b4d89 --- /dev/null +++ b/tests/xilinx_ug901/xilinx_ultraram_single_port_write_first.ys @@ -0,0 +1,24 @@ +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 |