Skip to content

Y
yosys-tests
Unverified Commit f3acf17b by Miodrag Milanović Committed by GitHub
Options

Merge pull request #64 from SergeyDegtyar/SergeyDegtyar/xilinx_ug901_synthesis_examples_tests 

Move tests for Xilinx UG901 examples from tests/xilinx_ug901 to yosys…
parents bc3a25f0 2d5dab20
Showing with 2956 additions and 0 deletions
architecture/Makefile
...@@ -75,6 +75,9 @@ $(eval $(call template,synth_xilinx_srl,synth_xilinx_srl)) ...@@ -75,6 +75,9 @@ $(eval $(call template,synth_xilinx_srl,synth_xilinx_srl))
$(eval $(call template,synth_xilinx_mux,synth_xilinx_mux)) $(eval $(call template,synth_xilinx_mux,synth_xilinx_mux))
endif endif
#xilinx_ug901_synthesis_examples
$(eval $(call template,xilinx_ug901_synthesis_examples,xilinx_ug901_synthesis_examples))
#greenpak4 #greenpak4
$(eval $(call template,synth_greenpak4,synth_greenpak4 synth_greenpak4_top synth_greenpak4_json synth_greenpak4_run synth_greenpak4_noflatten synth_greenpak4_retime synth_greenpak4_part621 synth_greenpak4_part620 synth_greenpak4_part140)) $(eval $(call template,synth_greenpak4,synth_greenpak4 synth_greenpak4_top synth_greenpak4_json synth_greenpak4_run synth_greenpak4_noflatten synth_greenpak4_retime synth_greenpak4_part621 synth_greenpak4_part620 synth_greenpak4_part140))
$(eval $(call template,synth_greenpak4_wide_ffs,synth_greenpak4 synth_greenpak4_top synth_greenpak4_json synth_greenpak4_run synth_greenpak4_noflatten synth_greenpak4_retime synth_greenpak4_part621 synth_greenpak4_part620 synth_greenpak4_part140)) $(eval $(call template,synth_greenpak4_wide_ffs,synth_greenpak4 synth_greenpak4_top synth_greenpak4_json synth_greenpak4_run synth_greenpak4_noflatten synth_greenpak4_retime synth_greenpak4_part621 synth_greenpak4_part620 synth_greenpak4_part140))
......
architecture/xilinx_ug901_synthesis_examples/asym_ram_sdp_read_wider.v 0 → 100644
// 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
architecture/xilinx_ug901_synthesis_examples/asym_ram_sdp_read_wider.ys 0 → 100644
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
architecture/xilinx_ug901_synthesis_examples/asym_ram_sdp_write_wider.v 0 → 100644
// 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 WIDTHA = 4;
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
architecture/xilinx_ug901_synthesis_examples/asym_ram_sdp_write_wider.ys 0 → 100644
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 9 t:FDRE
select -assert-count 1 t:LUT1
select -assert-count 6 t:LUT3
select -assert-count 8 t:RAM128X1D
select -assert-none t:BUFG t:FDRE t:LUT1 t:LUT3 t:RAM128X1D %% t:* %D
architecture/xilinx_ug901_synthesis_examples/asym_ram_tdp_read_first.v 0 → 100644
// 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
architecture/xilinx_ug901_synthesis_examples/asym_ram_tdp_read_first.ys 0 → 100644
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
architecture/xilinx_ug901_synthesis_examples/asym_ram_tdp_write_first.v 0 → 100644
// 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
architecture/xilinx_ug901_synthesis_examples/asym_ram_tdp_write_first.ys 0 → 100644
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
architecture/xilinx_ug901_synthesis_examples/black_box_1.v 0 → 100644
// 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
architecture/xilinx_ug901_synthesis_examples/black_box_1.ys 0 → 100644
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
architecture/xilinx_ug901_synthesis_examples/bytewrite_ram_1b.v 0 → 100644
// 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);
//Default parameters were changed because of slow test
//parameter SIZEB = 1024;
parameter SIZE = 32;
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
architecture/xilinx_ug901_synthesis_examples/bytewrite_ram_1b.ys 0 → 100644
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:FDRE
select -assert-count 32 t:LUT2
select -assert-count 32 t:RAM32X1D
select -assert-none t:BUFG t:FDRE t:LUT2 t:RAM32X1D %% t:* %D
architecture/xilinx_ug901_synthesis_examples/bytewrite_tdp_ram_nc.v 0 → 100644
//
// 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
architecture/xilinx_ug901_synthesis_examples/bytewrite_tdp_ram_nc.ys 0 → 100644
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
architecture/xilinx_ug901_synthesis_examples/bytewrite_tdp_ram_readfirst2.v 0 → 100644
// 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
architecture/xilinx_ug901_synthesis_examples/bytewrite_tdp_ram_readfirst2.ys 0 → 100644
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
architecture/xilinx_ug901_synthesis_examples/bytewrite_tdp_ram_rf.v 0 → 100644
// 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
architecture/xilinx_ug901_synthesis_examples/bytewrite_tdp_ram_rf.ys 0 → 100644
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
architecture/xilinx_ug901_synthesis_examples/bytewrite_tdp_ram_wf.v 0 → 100644
// 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
architecture/xilinx_ug901_synthesis_examples/bytewrite_tdp_ram_wf.ys 0 → 100644
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
architecture/xilinx_ug901_synthesis_examples/cmacc.v 0 → 100644
// 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
architecture/xilinx_ug901_synthesis_examples/cmacc.ys 0 → 100644
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
architecture/xilinx_ug901_synthesis_examples/cmult.v 0 → 100644
//
// Complex Multiplier (pr+i.pi) = (ar+i.ai)*(br+i.bi)
// file: cmult.v
//module cmult # (parameter AWIDTH = 16, BWIDTH = 18)
module cmult # (parameter AWIDTH = 8, BWIDTH = 9)
(
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
architecture/xilinx_ug901_synthesis_examples/cmult.ys 0 → 100644
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 144 t:FDRE
select -assert-count 9 t:LUT1
select -assert-count 176 t:LUT2
select -assert-count 36 t:LUT3
select -assert-count 51 t:LUT4
select -assert-count 35 t:LUT5
select -assert-count 343 t:LUT6
select -assert-count 111 t:MUXCY
select -assert-count 60 t:MUXF7
select -assert-count 21 t:MUXF8
select -assert-count 43 t:SRL16E
select -assert-count 119 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
architecture/xilinx_ug901_synthesis_examples/dynamic_shift_registers_1.v 0 → 100644
// 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
architecture/xilinx_ug901_synthesis_examples/dynamic_shift_registers_1.ys 0 → 100644
read_verilog ../dynamic_shift_registers_1.v
hierarchy -top dynamic_shift_register_1
proc
flatten
#ERROR: Found 1 unproven $equiv cells in 'equiv_status -assert'.
#equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
equiv_opt -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd dynamic_shift_register_1 # Constrain all select calls below inside the top module
#Vivado synthesizes 1 BUFG, 3 SRLC32E.
stat
select -assert-count 1 t:BUFG
select -assert-count 1 t:SRLC32E
select -assert-none t:BUFG t:SRLC32E %% t:* %D
architecture/xilinx_ug901_synthesis_examples/dynpreaddmultadd.v 0 → 100644
// 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
architecture/xilinx_ug901_synthesis_examples/dynpreaddmultadd.ys 0 → 100644
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
architecture/xilinx_ug901_synthesis_examples/fsm_1.v 0 → 100644
// 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
architecture/xilinx_ug901_synthesis_examples/fsm_1.ys 0 → 100644
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
architecture/xilinx_ug901_synthesis_examples/latches.v 0 → 100644
// 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
architecture/xilinx_ug901_synthesis_examples/latches.ys 0 → 100644
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
architecture/xilinx_ug901_synthesis_examples/macc.v 0 → 100644
// 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
architecture/xilinx_ug901_synthesis_examples/macc.ys 0 → 100644
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
architecture/xilinx_ug901_synthesis_examples/mult_unsigned.v 0 → 100644
// 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
architecture/xilinx_ug901_synthesis_examples/mult_unsigned.ys 0 → 100644
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
architecture/xilinx_ug901_synthesis_examples/presubmult.v 0 → 100644
//
// 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
architecture/xilinx_ug901_synthesis_examples/presubmult.ys 0 → 100644
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
architecture/xilinx_ug901_synthesis_examples/ram_simple_dual_one_clock.v 0 → 100644
// 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
architecture/xilinx_ug901_synthesis_examples/ram_simple_dual_one_clock.ys 0 → 100644
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
architecture/xilinx_ug901_synthesis_examples/ram_simple_dual_two_clocks.v 0 → 100644
// 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
architecture/xilinx_ug901_synthesis_examples/ram_simple_dual_two_clocks.ys 0 → 100644
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
architecture/xilinx_ug901_synthesis_examples/rams_dist.v 0 → 100644
// 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
architecture/xilinx_ug901_synthesis_examples/rams_dist.ys 0 → 100644
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
architecture/xilinx_ug901_synthesis_examples/rams_init_file.data 0 → 100644
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
architecture/xilinx_ug901_synthesis_examples/rams_init_file.v 0 → 100644
// 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
architecture/xilinx_ug901_synthesis_examples/rams_init_file.ys 0 → 100644
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
architecture/xilinx_ug901_synthesis_examples/rams_pipeline.v 0 → 100644
// 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
architecture/xilinx_ug901_synthesis_examples/rams_pipeline.ys 0 → 100644
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
architecture/xilinx_ug901_synthesis_examples/rams_sp_nc.v 0 → 100644
// 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
architecture/xilinx_ug901_synthesis_examples/rams_sp_nc.ys 0 → 100644
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
architecture/xilinx_ug901_synthesis_examples/rams_sp_rf.v 0 → 100644
// 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
architecture/xilinx_ug901_synthesis_examples/rams_sp_rf.ys 0 → 100644
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
architecture/xilinx_ug901_synthesis_examples/rams_sp_rf_rst.v 0 → 100644
// 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
architecture/xilinx_ug901_synthesis_examples/rams_sp_rf_rst.ys 0 → 100644
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
architecture/xilinx_ug901_synthesis_examples/rams_sp_rom.v 0 → 100644
// 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
architecture/xilinx_ug901_synthesis_examples/rams_sp_rom.ys 0 → 100644
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
architecture/xilinx_ug901_synthesis_examples/rams_sp_rom_1.v 0 → 100644
// 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
architecture/xilinx_ug901_synthesis_examples/rams_sp_rom_1.ys 0 → 100644
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
architecture/xilinx_ug901_synthesis_examples/rams_sp_wf.v 0 → 100644
// 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
architecture/xilinx_ug901_synthesis_examples/rams_sp_wf.ys 0 → 100644
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
architecture/xilinx_ug901_synthesis_examples/rams_tdp_rf_rf.v 0 → 100644
// 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
architecture/xilinx_ug901_synthesis_examples/rams_tdp_rf_rf.ys 0 → 100644
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
architecture/xilinx_ug901_synthesis_examples/registers_1.v 0 → 100644
// 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
architecture/xilinx_ug901_synthesis_examples/registers_1.ys 0 → 100644
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
architecture/xilinx_ug901_synthesis_examples/run-test.sh 0 → 100755
#!/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
} > run-test.mk
exec ${MAKE:-make} -f run-test.mk
architecture/xilinx_ug901_synthesis_examples/sfir_shifter.v 0 → 100644
//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
architecture/xilinx_ug901_synthesis_examples/sfir_shifter.ys 0 → 100644
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
architecture/xilinx_ug901_synthesis_examples/shift_registers_0.v 0 → 100644
// 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
architecture/xilinx_ug901_synthesis_examples/shift_registers_0.ys 0 → 100644
read_verilog ../shift_registers_0.v
hierarchy -top shift_registers_0
proc
flatten
#ERROR: Found 2 unproven $equiv cells in 'equiv_status -assert'.
#equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
equiv_opt -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd shift_registers_0 # Constrain all select calls below inside the top module
#Vivado synthesizes 1 BUFG, 2 FDRE, 3 SRLC32E.
select -assert-count 1 t:BUFG
select -assert-count 1 t:SRLC32E
select -assert-none t:BUFG t:SRLC32E %% t:* %D
architecture/xilinx_ug901_synthesis_examples/shift_registers_1.v 0 → 100644
// 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
architecture/xilinx_ug901_synthesis_examples/shift_registers_1.ys 0 → 100644
read_verilog ../shift_registers_1.v
hierarchy -top shift_registers_1
proc
flatten
#ERROR: Found 2 unproven $equiv cells in 'equiv_status -assert'.
#equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
equiv_opt -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd shift_registers_1 # Constrain all select calls below inside the top module
#Vivado synthesizes 1 BUFG, 2 FDRE, 3 SRLC32E.
select -assert-count 1 t:BUFG
select -assert-count 1 t:SRLC32E
select -assert-none t:BUFG t:SRLC32E %% t:* %D
architecture/xilinx_ug901_synthesis_examples/squarediffmacc.v 0 → 100644
// 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
architecture/xilinx_ug901_synthesis_examples/squarediffmacc.ys 0 → 100644
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
architecture/xilinx_ug901_synthesis_examples/squarediffmult.v 0 → 100644
// 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
architecture/xilinx_ug901_synthesis_examples/squarediffmult.ys 0 → 100644
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
architecture/xilinx_ug901_synthesis_examples/top_mux.v 0 → 100644
// 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
architecture/xilinx_ug901_synthesis_examples/top_mux.ys 0 → 100644
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
architecture/xilinx_ug901_synthesis_examples/tristates_1.v 0 → 100644
// 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
architecture/xilinx_ug901_synthesis_examples/tristates_1.ys 0 → 100644
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
architecture/xilinx_ug901_synthesis_examples/tristates_2.v 0 → 100644
// 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
architecture/xilinx_ug901_synthesis_examples/tristates_2.ys 0 → 100644
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
architecture/xilinx_ug901_synthesis_examples/xilinx_ultraram_single_port_no_change.v 0 → 100644
// 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
architecture/xilinx_ug901_synthesis_examples/xilinx_ultraram_single_port_no_change.ys 0 → 100644
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
architecture/xilinx_ug901_synthesis_examples/xilinx_ultraram_single_port_read_first.v 0 → 100644
// 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
architecture/xilinx_ug901_synthesis_examples/xilinx_ultraram_single_port_read_first.ys 0 → 100644
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
architecture/xilinx_ug901_synthesis_examples/xilinx_ultraram_single_port_write_first.v 0 → 100644
// 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
architecture/xilinx_ug901_synthesis_examples/xilinx_ultraram_single_port_write_first.ys 0 → 100644
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
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment