A simple AXI demo

.gitignore

axi_demo
axi_demo_tb.vcd
axi_demo_cover/
axi_demo_proof/

axi_demo.sby

[tasks]
cover
proof

[options]
proof: mode prove
proof: depth 20

cover: mode cover
cover: depth 600
cover: append 40

#multiclock on

[engines]
smtbmc yices
# smtbmc boolector
# abc pdr
# aiger avy
# aiger suprove

[script]
read_verilog -formal axi_demo.v
read_verilog -formal axi_master.v
read_verilog -formal axi_slave_ram.v
read_verilog -formal cache_controller.v


prep -top axi_demo
opt_merge -share_all

[files]
axi_demo.v
axi_master.v
axi_slave_ram.v
cache_controller.v

axi_demo.v

//`define AXI_PROTOCOL_CHECKER 1
`define LOOPBACK 1

module axi_demo(clk, reset, done, error);

input clk, reset;
output reg done;
output reg error;


`ifdef FORMAL
	// AXI Address width (log wordsize) for slave
	parameter C_AXI_ADDR_WIDTH = 12;
	parameter C_AXI_DATA_WIDTH = 8; // related to AxSIZE
	parameter C_SIZE_OF_CACHE = 4; // for storing weights and biases parameters of neural network
`else
	// AXI Address width (log wordsize) for slave
	parameter C_AXI_ADDR_WIDTH = 12; // just for random test
	parameter C_AXI_DATA_WIDTH = 128; // related to AxSIZE
	parameter C_SIZE_OF_CACHE = 64; // for storing weights and biases parameters of neural network
`endif

parameter C_AXI_ID_WIDTH	=   1;

parameter SIZE_OF_SLAVE_MEMORY = (1 << C_AXI_ADDR_WIDTH);

localparam INCR_BURST_TYPE = 2'b01; // AxBURST[2:0] , see 'burst type' section in AXI spec

// AXI4 extends burst length support for the INCR burst type to 1 to 256 transfers. 
// Support for all other burst types in AXI4 remains at 1 to 16 transfers.
// for wrapping bursts, the burst length must be 2, 4, 8, or 16
// a burst must not cross a 4KB address boundary
// early termination of bursts is not supported
localparam MAX_BURST_LENGTH = 256; 

localparam BURST_SIZE_ENCODING_WIDTH = 3; // AxSIZE[2:0] , see 'burst size' section in AXI spec
localparam SUBWORD_SMALLEST_UNIT = 8; // smallest granularity in AXI protocol : 8 bit
localparam PROT_BITWIDTH = 3;
localparam QOS_BITWIDTH = 4;
localparam CACHE_BITWIDTH = 4;


// AXI write address channel signals
	wire			axi_awready; // Slave is ready to accept
	wire	[C_AXI_ID_WIDTH-1:0]	axi_awid;	// Write ID
	wire	[C_AXI_ADDR_WIDTH-1:0]	axi_awaddr;	// Write address
	wire	[$clog2(MAX_BURST_LENGTH)-1:0]		axi_awlen;	// Write Burst Length
	wire	[BURST_SIZE_ENCODING_WIDTH-1:0]		axi_awsize;	// Write Burst size
	wire	[1:0]		axi_awburst;	// Write Burst type
	wire	[0:0]		axi_awlock;	// Write lock type
	wire	[CACHE_BITWIDTH-1:0]		axi_awcache;	// Write Cache type
	wire	[PROT_BITWIDTH-1:0]		axi_awprot;	// Write Protection type
/* verilator lint_off UNUSED */
	wire	[QOS_BITWIDTH-1:0]		axi_awqos;	// Write Quality of Svc
/* verilator lint_on UNUSED */
	wire			axi_awvalid;	// Write address valid

// AXI write data channel signals
	wire			axi_wready;  // Write data ready
	wire	[C_AXI_DATA_WIDTH-1:0]	axi_wdata;	// Write data
	wire	[C_AXI_DATA_WIDTH/SUBWORD_SMALLEST_UNIT-1:0] axi_wstrb;	// Write strobes
	wire			axi_wlast;	// Last write transaction
	wire			axi_wvalid;	// Write valid

// AXI write response channel signals
 	wire 	[C_AXI_ID_WIDTH-1:0]	axi_bid;	// Response ID
	wire 	[1:0]		axi_bresp;	// Write response
	wire			axi_bvalid;  // Write reponse valid
	wire			axi_bready;  // Response ready

// AXI read address channel signals
	wire			axi_arready;	// Read address ready
	wire	[C_AXI_ID_WIDTH-1:0]	axi_arid;	// Read ID
	wire 	[C_AXI_ADDR_WIDTH-1:0]	axi_araddr;	// Read address
	wire	[$clog2(MAX_BURST_LENGTH)-1:0]		axi_arlen;	// Read Burst Length
	wire	[BURST_SIZE_ENCODING_WIDTH-1:0]		axi_arsize;	// Read Burst size
	wire	[1:0]		axi_arburst;	// Read Burst type
	wire	[0:0]		axi_arlock;	// Read lock type
	wire	[CACHE_BITWIDTH-1:0]		axi_arcache;	// Read Cache type
	wire	[PROT_BITWIDTH-1:0]		axi_arprot;	// Read Protection type
/* verilator lint_off UNUSED */
	wire	[QOS_BITWIDTH-1:0]		axi_arqos;	// Read Quality of Svc
/* verilator lint_on UNUSED */
	wire			axi_arvalid;	// Read address valid

// AXI read data channel signals
 	wire 	[C_AXI_ID_WIDTH-1:0]	axi_rid;     // Response ID
	wire	[1:0]		axi_rresp;   // Read response
	wire			axi_rvalid;  // Read reponse valid
 	wire 	[C_AXI_DATA_WIDTH-1:0] axi_rdata;    // Read data
	wire			axi_rlast;    // Read last
	wire			axi_rready;  // Read Response ready

`ifdef AXI_PROTOCOL_CHECKER

// https://www.xilinx.com/products/intellectual-property/axi_protocol_checker.html

localparam PC_STATUS_BITWIDTH = 160;
wire [PC_STATUS_BITWIDTH-1:0] pc_status ;
wire pc_asserted;

axi_protocol_checker_0 axi_pc0(
    .pc_status(pc_status),
    .pc_asserted(pc_asserted), 
    .aclk(clk), 
    .aresetn(!reset), 
    .pc_axi_awid(axi_awid),       .pc_axi_awaddr(axi_awaddr),   .pc_axi_awlen(axi_awlen),     
    .pc_axi_awsize(axi_awsize),   .pc_axi_awburst(axi_awburst), .pc_axi_awlock(axi_awlock),   
    .pc_axi_awcache(axi_awcache), .pc_axi_awprot(axi_awprot),   .pc_axi_awqos(axi_awqos),     
    .pc_axi_awregion(0),		  .pc_axi_awvalid(axi_awvalid), .pc_axi_awready(axi_awready), 
    .pc_axi_wlast(axi_wlast),     .pc_axi_wdata(axi_wdata),     .pc_axi_wstrb(axi_wstrb), 
    .pc_axi_wvalid(axi_wvalid),   .pc_axi_wready(axi_wready),   .pc_axi_bid(axi_bid),         
    .pc_axi_bresp(axi_bresp),     .pc_axi_bvalid(axi_bvalid),   .pc_axi_bready(axi_bready),   
    .pc_axi_arid(axi_arid),       .pc_axi_araddr(axi_araddr),   .pc_axi_arlen(axi_arlen), 
    .pc_axi_arsize(axi_arsize),   .pc_axi_arburst(axi_arburst), .pc_axi_arlock(axi_arlock), 
    .pc_axi_arcache(axi_arcache), .pc_axi_arprot(axi_arprot),   .pc_axi_arqos(axi_arqos), 
    .pc_axi_arregion(0),          .pc_axi_arvalid(axi_arvalid), .pc_axi_arready(axi_arready), 
    .pc_axi_rid(axi_rid),         .pc_axi_rlast(axi_rlast),     .pc_axi_rdata(axi_rdata),     
    .pc_axi_rresp(axi_rresp),     .pc_axi_rvalid(axi_rvalid),   .pc_axi_rready(axi_rready)
);
`endif

// there is no need of address generator logic for hard-coded instructions 

axi_master #(.C_AXI_DATA_WIDTH(C_AXI_DATA_WIDTH)) hardcoded_nn_params
(
    .clk(clk), .reset(reset),
    .i_axi_awready(axi_awready), .o_axi_awid(axi_awid),       .o_axi_awaddr(axi_awaddr), 
    .o_axi_awlen(axi_awlen),     .o_axi_awsize(axi_awsize),   .o_axi_awburst(axi_awburst),
    .o_axi_awlock(axi_awlock),   .o_axi_awcache(axi_awcache), .o_axi_awprot(axi_awprot), 
    .o_axi_awqos(axi_awqos),     .o_axi_awvalid(axi_awvalid), .i_axi_wready(axi_wready), 
    .o_axi_wdata(axi_wdata),     .o_axi_wstrb(axi_wstrb),     .o_axi_wlast(axi_wlast), 
    .o_axi_wvalid(axi_wvalid),   .i_axi_bid(axi_bid),         .i_axi_bresp(axi_bresp), 
    .i_axi_bvalid(axi_bvalid),   .o_axi_bready(axi_bready),   .i_axi_arready(axi_arready), 
    .o_axi_arid(axi_arid),       .o_axi_araddr(axi_araddr),   .o_axi_arlen(axi_arlen), 
    .o_axi_arsize(axi_arsize),   .o_axi_arburst(axi_arburst), .o_axi_arlock(axi_arlock), 
    .o_axi_arcache(axi_arcache), .o_axi_arprot(axi_arprot),   .o_axi_arqos(axi_arqos), 
    .o_axi_arvalid(axi_arvalid), .i_axi_rid(axi_rid),         .i_axi_rresp(axi_rresp), 
    .i_axi_rvalid(axi_rvalid),   .i_axi_rdata(axi_rdata),     .i_axi_rlast(axi_rlast), 
    .o_axi_rready(axi_rready)
);


// for storing NN params at source side 
// (the source is a slave memory device which is accessible using AXI)

axi_slave_ram axi_ram(
	.clk(clk), .rst(reset), 
    .s_axi_awready(axi_awready), .s_axi_awid(axi_awid),       .s_axi_awaddr(axi_awaddr), 
    .s_axi_awlen(axi_awlen),     .s_axi_awsize(axi_awsize),   .s_axi_awburst(axi_awburst),
    .s_axi_awlock(axi_awlock),   .s_axi_awcache(axi_awcache), .s_axi_awprot(axi_awprot), 
    .s_axi_awvalid(axi_awvalid), .s_axi_wready(axi_wready),   .s_axi_wdata(axi_wdata),     
    .s_axi_wstrb(axi_wstrb),     .s_axi_wlast(axi_wlast),     .s_axi_wvalid(axi_wvalid),   
    .s_axi_bid(axi_bid),         .s_axi_bresp(axi_bresp),     .s_axi_bvalid(axi_bvalid),   
    .s_axi_bready(axi_bready),   .s_axi_arready(axi_arready), .s_axi_arid(axi_arid),       
    .s_axi_araddr(axi_araddr),   .s_axi_arlen(axi_arlen),     .s_axi_arsize(axi_arsize),   
    .s_axi_arburst(axi_arburst), .s_axi_arlock(axi_arlock),   .s_axi_arcache(axi_arcache), 
    .s_axi_arprot(axi_arprot),   .s_axi_arvalid(axi_arvalid), .s_axi_rid(axi_rid),         
    .s_axi_rresp(axi_rresp),     .s_axi_rvalid(axi_rvalid),   .s_axi_rdata(axi_rdata),     
    .s_axi_rlast(axi_rlast),     .s_axi_rready(axi_rready)
);


// each read transaction only read one particular piece of data at one unique, non-consecutive address
reg [$clog2(SIZE_OF_SLAVE_MEMORY)-1:0] num_of_memory_data_read_transaction ;
wire valid_read_response_contains_error_messages ;

assign valid_read_response_contains_error_messages = (axi_rvalid && (axi_rresp != 0));


always @(posedge clk)
begin
	if(reset) num_of_memory_data_read_transaction <= 0;

	else if(axi_rready && axi_rvalid && (axi_rresp == 0)) 
		num_of_memory_data_read_transaction <=
		num_of_memory_data_read_transaction + 1;
end
	
always @(posedge clk)
begin
	if(reset) error <= 0;

	else error <= 
			((valid_read_response_contains_error_messages) 
			`ifdef AXI_PROTOCOL_CHECKER 
							| (pc_asserted) 
			`endif
			);
end

always @(posedge clk)
begin
	if(reset) done <= 0;

	else if(num_of_memory_data_read_transaction == SIZE_OF_SLAVE_MEMORY-1) 
			done <= 1;
end

endmodule

axi_demo_cover.gtkw

[*]
[*] GTKWave Analyzer v3.3.104 (w)1999-2020 BSI
[*] Fri May  1 07:32:10 2020
[*]
[dumpfile] "/home/phung/Downloads/AXI/axi_demo/axi_demo_cover/engine_0/trace0.vcd"
[dumpfile_mtime] "Fri May  1 07:29:21 2020"
[dumpfile_size] 220541
[savefile] "/home/phung/Downloads/AXI/axi_demo/axi_demo_cover.gtkw"
[timestart] 0
[size] 960 995
[pos] -1 -1
*-6.484500 200 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1
[sst_width] 48
[signals_width] 374
[sst_expanded] 0
[sst_vpaned_height] 152
@28
smt_clock
@420
smt_step
@23
axi_demo.axi_araddr[11:0]
@28
axi_demo.axi_arburst[1:0]
@22
axi_demo.axi_arcache[3:0]
@28
axi_demo.axi_arid
@22
axi_demo.axi_arlen[7:0]
@28
axi_demo.axi_arlock
axi_demo.axi_arprot[2:0]
@22
axi_demo.axi_arqos[3:0]
@29
axi_demo.axi_arready
@28
axi_demo.axi_arsize[2:0]
@29
axi_demo.axi_arvalid
@23
axi_demo.axi_awaddr[11:0]
@28
axi_demo.axi_awburst[1:0]
@22
axi_demo.axi_awcache[3:0]
@28
axi_demo.axi_awid
@22
axi_demo.axi_awlen[7:0]
@28
axi_demo.axi_awlock
axi_demo.axi_awprot[2:0]
@22
axi_demo.axi_awqos[3:0]
@29
axi_demo.axi_awready
@28
axi_demo.axi_awsize[2:0]
@29
axi_demo.axi_awvalid
@28
axi_demo.axi_bid
@29
axi_demo.axi_bready
axi_demo.axi_bresp[1:0]
axi_demo.axi_bvalid
@23
axi_demo.axi_rdata[7:0]
@28
axi_demo.axi_rid
axi_demo.axi_rlast
@29
axi_demo.axi_rready
@28
axi_demo.axi_rresp[1:0]
@29
axi_demo.axi_rvalid
@23
axi_demo.axi_wdata[7:0]
@28
axi_demo.axi_wlast
@29
axi_demo.axi_wready
@28
axi_demo.axi_wstrb
@29
axi_demo.axi_wvalid
@28
axi_demo.clk
axi_demo.done
axi_demo.error
@22
axi_demo.num_of_memory_data_read_transaction[11:0]
@28
axi_demo.reset
axi_demo.valid_read_response_contains_error_messages
[pattern_trace] 1
[pattern_trace] 0

axi_demo_tb.gtkw

[*]
[*] GTKWave Analyzer v3.3.86 (w)1999-2017 BSI
[*] Thu Apr 30 08:21:17 2020
[*]
[dumpfile] "/home/rog/Downloads/AXI/axi_demo_tb.vcd"
[dumpfile_mtime] "Thu Apr 30 08:20:44 2020"
[dumpfile_size] 99580
[savefile] "/home/rog/Downloads/AXI/axi_demo_tb.gtkw"
[timestart] 0
[size] 927 1025
[pos] -1 -1
*-20.585678 2055000 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1
[treeopen] axi_demo_tb.
[treeopen] axi_demo_tb.axi.
[sst_width] 43
[signals_width] 446
[sst_expanded] 0
[sst_vpaned_height] 152
@23
axi_demo_tb.axi.axi_araddr[11:0]
@28
axi_demo_tb.axi.axi_arburst[1:0]
@22
axi_demo_tb.axi.axi_arcache[3:0]
@28
axi_demo_tb.axi.axi_arid
@22
axi_demo_tb.axi.axi_arlen[7:0]
@28
axi_demo_tb.axi.axi_arlock
axi_demo_tb.axi.axi_arprot[2:0]
@22
axi_demo_tb.axi.axi_arqos[3:0]
@29
axi_demo_tb.axi.axi_arready
@28
axi_demo_tb.axi.axi_arsize[2:0]
@29
axi_demo_tb.axi.axi_arvalid
@23
axi_demo_tb.axi.axi_awaddr[11:0]
@28
axi_demo_tb.axi.axi_awburst[1:0]
@22
axi_demo_tb.axi.axi_awcache[3:0]
@28
axi_demo_tb.axi.axi_awid
@22
axi_demo_tb.axi.axi_awlen[7:0]
@28
axi_demo_tb.axi.axi_awlock
axi_demo_tb.axi.axi_awprot[2:0]
@22
axi_demo_tb.axi.axi_awqos[3:0]
@29
axi_demo_tb.axi.axi_awready
@28
axi_demo_tb.axi.axi_awsize[2:0]
@29
axi_demo_tb.axi.axi_awvalid
@28
axi_demo_tb.axi.axi_bid
axi_demo_tb.axi.axi_bready
axi_demo_tb.axi.axi_bresp[1:0]
axi_demo_tb.axi.axi_bvalid
@23
axi_demo_tb.axi.axi_rdata[127:0]
@28
axi_demo_tb.axi.axi_rid
axi_demo_tb.axi.axi_rlast
axi_demo_tb.axi.axi_rready
axi_demo_tb.axi.axi_rresp[1:0]
axi_demo_tb.axi.axi_rvalid
@23
axi_demo_tb.axi.axi_wdata[127:0]
@28
axi_demo_tb.axi.axi_wlast
axi_demo_tb.axi.axi_wready
@22
axi_demo_tb.axi.axi_wstrb[15:0]
@28
axi_demo_tb.axi.axi_wvalid
axi_demo_tb.axi.clk
axi_demo_tb.axi.done
axi_demo_tb.axi.error
@22
axi_demo_tb.axi.num_of_memory_data_read_transaction[11:0]
@28
axi_demo_tb.axi.reset
axi_demo_tb.axi.valid_read_response_contains_error_messages
[pattern_trace] 1
[pattern_trace] 0

axi_demo_tb.v

`timescale 1ns/1ns

module axi_demo_tb();

reg clk, reset;
wire done;
wire error;

localparam NUM_OF_RUNNING_CLOCK_CYCLES = 300;

axi_demo axi (.clk(clk), .reset(reset), .done(done), .error(error));

initial begin

    $dumpfile("axi_demo_tb.vcd");
    $dumpvars(0, axi_demo_tb);

    clk = 0;
    reset = 0;
    
    @(posedge clk);
    @(posedge clk);
    @(posedge clk);
    
    reset = 1;
    
    @(posedge clk);
    @(posedge clk);
    
    reset = 0;
    
    repeat(NUM_OF_RUNNING_CLOCK_CYCLES) @(posedge clk);  
    
    $finish;
end

localparam clk_period = 5;

always @(*) #clk_period clk <= !clk;
    
endmodule

axi_master.v

`define LOOPBACK 1

module axi_master(clk, reset,
			i_axi_awready, o_axi_awid, o_axi_awaddr, o_axi_awlen, o_axi_awsize, o_axi_awburst,
		 	o_axi_awlock, o_axi_awcache, o_axi_awprot, o_axi_awqos, o_axi_awvalid,
			i_axi_wready, o_axi_wdata, o_axi_wstrb, o_axi_wlast, o_axi_wvalid,
			i_axi_bid, i_axi_bresp, i_axi_bvalid, o_axi_bready, 
			i_axi_arready, o_axi_arid, o_axi_araddr, o_axi_arlen, o_axi_arsize, o_axi_arburst,
			o_axi_arlock, o_axi_arcache, o_axi_arprot, o_axi_arqos, o_axi_arvalid,
			i_axi_rid, i_axi_rresp, i_axi_rvalid, i_axi_rdata, i_axi_rlast, o_axi_rready);


`ifdef FORMAL
	// AXI Address width (log wordsize) for slave
	parameter C_AXI_ADDR_WIDTH = 12; 
	parameter C_AXI_DATA_WIDTH = 8; // related to AxSIZE
	parameter C_SIZE_OF_CACHE = 4; // for storing weights and biases parameters of neural network
`else
	// AXI Address width (log wordsize) for slave
	parameter C_AXI_ADDR_WIDTH = 12; // just for random test
	parameter C_AXI_DATA_WIDTH = 128; // related to AxSIZE
	parameter C_SIZE_OF_CACHE = 64; // for storing weights and biases parameters of neural network
`endif

parameter C_AXI_ID_WIDTH	=   1;

localparam NUM_OF_BITS_PER_BYTES = 8;
localparam INCR_BURST_TYPE = 2'b01; // AxBURST[2:0] , see 'burst type' section in AXI spec

// AXI4 extends burst length support for the INCR burst type to 1 to 256 transfers. 
// Support for all other burst types in AXI4 remains at 1 to 16 transfers.
// for wrapping bursts, the burst length must be 2, 4, 8, or 16
// a burst must not cross a 4KB address boundary
// early termination of bursts is not supported
localparam MAX_BURST_LENGTH = 256; 

localparam BURST_SIZE_ENCODING_WIDTH = 3; // AxSIZE[2:0] , see 'burst size' section in AXI spec
localparam SUBWORD_SMALLEST_UNIT = 8; // smallest granularity in AXI protocol : 8 bit
localparam PROT_BITWIDTH = 3;
localparam QOS_BITWIDTH = 4;
localparam CACHE_BITWIDTH = 4;

localparam BITWIDTH_DIFFERENCE_ADDR_AND_BURST_LENGTH = 
			 (C_AXI_ADDR_WIDTH > $clog2(MAX_BURST_LENGTH)) ?
		C_AXI_ADDR_WIDTH-$clog2(MAX_BURST_LENGTH) : $clog2(MAX_BURST_LENGTH)-C_AXI_ADDR_WIDTH ;

input clk, reset;

// AXI write address channel signals
	input	wire			i_axi_awready; // Slave is ready to accept
	output	wire	[C_AXI_ID_WIDTH-1:0]	o_axi_awid;	// Write ID
	output	reg		[C_AXI_ADDR_WIDTH-1:0]	o_axi_awaddr;	// Write address
	output	wire	[$clog2(MAX_BURST_LENGTH)-1:0]		o_axi_awlen;	// Write Burst Length
	output	wire	[BURST_SIZE_ENCODING_WIDTH-1:0]		o_axi_awsize;	// Write Burst size
	output	wire	[1:0]		o_axi_awburst;	// Write Burst type
	output	wire	[0:0]		o_axi_awlock;	// Write lock type
	output	wire	[CACHE_BITWIDTH-1:0]		o_axi_awcache;	// Write Cache type
	output	wire	[PROT_BITWIDTH-1:0]		o_axi_awprot;	// Write Protection type
/* verilator lint_off UNUSED */
	output	wire	[QOS_BITWIDTH-1:0]		o_axi_awqos;	// Write Quality of Svc
/* verilator lint_on UNUSED */
	output	reg			o_axi_awvalid;	// Write address valid

// AXI write data channel signals
	input	wire			i_axi_wready;  // Write data ready
	output	reg	[C_AXI_DATA_WIDTH-1:0]	o_axi_wdata;	// Write data
	output	reg	[C_AXI_DATA_WIDTH/SUBWORD_SMALLEST_UNIT-1:0] o_axi_wstrb;	// Write strobes
	output	reg			o_axi_wlast;	// Last write transaction
	output	reg			o_axi_wvalid;	// Write valid

// AXI write response channel signals
/* verilator lint_off UNUSED */
	input 	wire [C_AXI_ID_WIDTH-1:0]	i_axi_bid;	// Response ID
/* verilator lint_on UNUSED */
	input	wire [1:0]		i_axi_bresp;	// Write response
	input	wire			i_axi_bvalid;  // Write reponse valid
	output	wire			o_axi_bready;  // Response ready

// AXI read address channel signals
	input	wire			i_axi_arready;	// Read address ready
	output	wire	[C_AXI_ID_WIDTH-1:0]	o_axi_arid;	// Read ID
	output	reg 	[C_AXI_ADDR_WIDTH-1:0]	o_axi_araddr;	// Read address
	output	wire	[$clog2(MAX_BURST_LENGTH)-1:0]		o_axi_arlen;	// Read Burst Length
	output	wire	[BURST_SIZE_ENCODING_WIDTH-1:0]		o_axi_arsize;	// Read Burst size
	output	wire	[1:0]		o_axi_arburst;	// Read Burst type
	output	wire	[0:0]		o_axi_arlock;	// Read lock type
	output	wire	[CACHE_BITWIDTH-1:0]		o_axi_arcache;	// Read Cache type
	output	wire	[PROT_BITWIDTH-1:0]		o_axi_arprot;	// Read Protection type
/* verilator lint_off UNUSED */
	output	wire	[QOS_BITWIDTH-1:0]		o_axi_arqos;	// Read Quality of Svc
/* verilator lint_on UNUSED */
	output	reg			o_axi_arvalid;	// Read address valid

/* verilator lint_off UNUSED */
// AXI read data channel signals
	input wire 		[C_AXI_ID_WIDTH-1:0]	i_axi_rid;     // Response ID
/* verilator lint_on UNUSED */
	input	wire	[1:0]		i_axi_rresp;   // Read response
	input	wire			i_axi_rvalid;  // Read reponse valid
	input 	wire 	[C_AXI_DATA_WIDTH-1:0] i_axi_rdata;    // Read data
	input	wire			i_axi_rlast;    // Read last
	output	wire			o_axi_rready;  // Read Response ready




always @(posedge clk) 
begin
	if(reset) o_axi_wstrb <= 0;

	// burst alignment mechanism, see https://i.imgur.com/jKbzfFo.png
	// o_axi_wstrb <= (~0) << (o_axi_awaddr % (o_axi_awlen+1));
	// all the bracket variables are for removing verilator width warnings

	else o_axi_wstrb <= (C_AXI_DATA_WIDTH == SUBWORD_SMALLEST_UNIT) ? 1'b1 : 
								((~0) << (o_axi_awaddr % 
						   		  {{(BITWIDTH_DIFFERENCE_ADDR_AND_BURST_LENGTH){1'b0}},
								    (o_axi_awlen+1'b1)}));
end

wire write_response_is_ok = i_axi_bvalid && ((i_axi_bresp == 'b00) || (i_axi_bresp == 'b01));

// need to implement data re-transmission
wire write_response_is_not_ok = i_axi_bvalid && !((i_axi_bresp == 'b00) || (i_axi_bresp == 'b01));


always @(posedge clk) 
begin
	if(reset) 
	begin 
		o_axi_wvalid <= 0;
	end

	else if(!(o_axi_wvalid && !i_axi_wready))
	begin
		// since this is for testing, WDATA just uses some values within the write data space
		// Note: a master must not wait for AWREADY to be asserted before driving WVALID
		o_axi_wvalid <= (o_axi_wlast) ? 0 : 
						(o_axi_wdata < {C_AXI_DATA_WIDTH{1'b1}}); 
	end
end

wire slave_write_address_range_is_valid = (o_axi_awaddr < (1 << C_AXI_ADDR_WIDTH));

always @(posedge clk) 
begin	
	if(reset) o_axi_awvalid <= 0;

	// AXI specification: A3.3.1 Dependencies between channel handshake signal
	// the VALID signal of the AXI interface sending information must not be dependent on 
	// the READY signal of the AXI interface receiving that information
	// this is to prevent deadlock 
	// since AXI slave could wait for i_axi_awvalid to be true before setting o_axi_awready true.
	// Note: For same interface, VALID cannot depend upon READY, but READY can depends upon VALID
	// Note: Once VALID is asserted, it MUST be kept asserted until READY is asserted.
	// 		 VALID signal needs to be set (initially) independent of READY signal, 
	// 		 and then only ever adjusted if !(VALID && !READY)
	// Note: the master must not wait for the slave to assert AWREADY before asserting AWVALID
	// Note: (!(o_axi_awvalid && !i_axi_awready)) == (!awvalid || awready) 
	//       == (!awvalid || (awvalid && awready)). 
	//		 it means "no transaction in progress or transaction accepted"
	else if(!(o_axi_awvalid && !i_axi_awready))
			o_axi_awvalid <= /*i_axi_awready &&*/ (slave_write_address_range_is_valid);
end

reg [C_AXI_ADDR_WIDTH-1:0] axi_awaddr_previous;
always @(posedge clk)
begin
	if(reset) axi_awaddr_previous <= 0;

	else if(address_write_transaction_is_accepted) axi_awaddr_previous <= o_axi_awaddr;
end

wire write_transaction_is_accepted = (o_axi_wvalid) && (i_axi_wready);
wire address_write_transaction_is_accepted = (o_axi_awvalid) && (i_axi_awready);

wire bad_bresp_just_arrived = (!axi_bvalid_previous) && write_response_is_not_ok;

always @(posedge clk)
begin
	if(reset) o_axi_awaddr <= 0;

	else if(address_write_transaction_is_accepted) 
	begin
		if(write_response_is_not_ok) o_axi_awaddr <= axi_awaddr_previous;
		
		else o_axi_awaddr <= ((retransmit_wdata_now) ? axi_awaddr_previous : o_axi_awaddr) + 
							{{(BITWIDTH_DIFFERENCE_ADDR_AND_BURST_LENGTH){1'b0}}, 
								(o_axi_awlen+1'b1)} * (1 << o_axi_awsize);
	end
end

reg axi_bvalid_previous;
always @(posedge clk) axi_bvalid_previous <= i_axi_bvalid;

reg needs_to_retransmit_wdata; // a signal to prepare for asserting 'retransmit_wdata_now' in the next burst
reg retransmit_wdata_now;
// needs to store the entire write burst of data in the case of bad BRESP from AXI slave,
// let the next pair of AWADDR and WDATA to proceed before retransmitting the previous pair of AWADDR and WDATA
// because AWADDR is clocked-reg and can only transitions after (AWVALID && AWREADY) is true,
// and AWREADY as well as BVALID from AXI slave can be asserted at same clock edge
reg [C_AXI_DATA_WIDTH-1:0]  wdata_to_be_retransmitted [AxLEN:0];

always @(posedge clk)
begin
	if(reset || (retransmission_index == AxLEN)) retransmit_wdata_now <= 0;
	
	else if(needs_to_retransmit_wdata && o_axi_wlast && (retransmission_index != o_axi_awlen+1))
		retransmit_wdata_now <= 1;
end

`ifdef LOOPBACK

generate

genvar wdata_index;

	for(wdata_index=0; wdata_index<=AxLEN; wdata_index=wdata_index+1)
	begin
		always @(posedge clk) 
			if(bad_bresp_just_arrived && !retransmit_wdata_now) 
				wdata_to_be_retransmitted[wdata_index] <= o_axi_wdata - AxLEN + wdata_index;
	end

endgenerate

`endif

always @(*)
begin
	if(reset || write_response_is_ok) needs_to_retransmit_wdata = 0;
	
	else if(write_response_is_not_ok) needs_to_retransmit_wdata = 1;
end

reg [$clog2(AxLEN):0] retransmission_index;
reg [$clog2(AxLEN):0] retransmission_index_previous;

always @(posedge clk)
begin
	if(reset) retransmission_index <= 0;
	
	else if(retransmit_wdata_now) retransmission_index <= retransmission_index + 1;
	
	else retransmission_index <= 0;
end

always @(posedge clk) 
begin
	if(reset) retransmission_index_previous <= 0;

	else retransmission_index_previous <= retransmission_index;
end

wire wdata_retransmission_just_finished
	= (retransmission_index == 0) && (retransmission_index_previous == AxLEN+1);

reg [C_AXI_DATA_WIDTH-1:0] axi_wdata_next;

always @(posedge clk) 
	if(o_axi_wlast && needs_to_retransmit_wdata) axi_wdata_next <= o_axi_wdata;

always @(posedge clk)
begin
	if(reset) o_axi_wdata <= 0;

	else if(!(o_axi_wvalid && !i_axi_wready)) 
	begin
		if(retransmit_wdata_now) 
			o_axi_wdata <= wdata_to_be_retransmitted[retransmission_index];
		
		else o_axi_wdata <= ((wdata_retransmission_just_finished) ? axi_wdata_next : o_axi_wdata) 
								+ (!o_axi_wlast);
	end
end

`ifdef LOOPBACK

wire data_had_been_written_successfully = write_response_is_ok && o_axi_bready;

wire read_address_contains_loopback_data = data_had_been_written_successfully &&
(o_axi_awaddr >= (o_axi_araddr + {{(BITWIDTH_DIFFERENCE_ADDR_AND_BURST_LENGTH){1'b0}}, o_axi_awlen}));

`endif

wire slave_read_address_range_is_valid = (o_axi_araddr < (1 << C_AXI_ADDR_WIDTH));


always @(posedge clk) 
begin	
	if(reset) o_axi_arvalid <= 0;

	// AXI specification: A3.3.1 Dependencies between channel handshake signal
	// the VALID signal of the AXI interface sending information must not be dependent on 
	// the READY signal of the AXI interface receiving that information
	// this is to prevent deadlock 
	// since AXI slave could wait for i_axi_arvalid to be true before setting o_axi_arready true.
	// Note: For same interface, VALID cannot depend upon READY, but READY can depends upon VALID
	// Note: Once VALID is asserted, it MUST be kept asserted until READY is asserted.
	// 		 VALID signal needs to be set (initially) independent of READY signal, 
	// 		 and then only ever adjusted if !(VALID && !READY)
	// Note: the master must not wait for the slave to assert ARREADY before asserting ARVALID
	// Note: (!(o_axi_arvalid && !i_axi_arready)) == (!arvalid || arready) 
	//       == (!arvalid || (arvalid && arready)). 
	//		 it means "no transaction in progress or transaction accepted"
	else if(!(o_axi_arvalid && !i_axi_arready))
		`ifdef LOOPBACK
			o_axi_arvalid <= /*i_axi_arready &&*/ (slave_read_address_range_is_valid) && 
							//(read_address_contains_loopback_data) && 
							(o_axi_bready && i_axi_bvalid && write_response_is_ok);
		`else
			o_axi_arvalid <= /*i_axi_arready &&*/ (slave_read_address_range_is_valid);
		`endif
end


reg [$clog2(MAX_BURST_LENGTH)-1:0] num_of_write_transactions;

always @(posedge clk) 
begin	
	if(reset) num_of_write_transactions <= 0;

	else if(o_axi_wvalid && i_axi_wready)
			num_of_write_transactions <= (o_axi_wlast) ? 0 : num_of_write_transactions + 1;
end

always @(posedge clk) 
begin	
	if(reset) o_axi_wlast <= 0;

	else o_axi_wlast <= (num_of_write_transactions == (o_axi_awlen - 1));
end

localparam AxLEN = 15;

assign o_axi_awid = 0;
assign o_axi_awlen = AxLEN; // each burst has (Burst_Length = AxLEN[7:0] + 1) data transfers

/* verilator lint_off WIDTH */

// 128 bits (16 bytes) of data when AxSIZE[2:0] = 3'b100
// Burst_Length = AxLEN[7:0] + 1, to accommodate the extended burst length of the INCR burst type

assign o_axi_awsize = $clog2(C_AXI_DATA_WIDTH/NUM_OF_BITS_PER_BYTES); 
assign o_axi_arsize = $clog2(C_AXI_DATA_WIDTH/NUM_OF_BITS_PER_BYTES);

/* verilator lint_on WIDTH */

assign o_axi_awburst = INCR_BURST_TYPE;
assign o_axi_awlock = 0;
assign o_axi_awcache = 0;
assign o_axi_awprot = 0;

/* verilator lint_off UNUSED */
assign o_axi_awqos = 0; // no priority or QoS concept
assign o_axi_arqos = 0; // no priority or QoS concept
/* verilator lint_on UNUSED */

assign o_axi_arburst = INCR_BURST_TYPE;

assign o_axi_arlen = AxLEN; // each burst has (Burst_Length = AxLEN[7:0] + 1) data transfers
assign o_axi_arprot = 3'b010; // {data access, non-secure access, unprivileged access}
assign o_axi_arlock = 0; // AXI4 does not support locked transactions. 
assign o_axi_arcache = 0; // mostly used for HPS (hard processor system) such as ARM hard CPU IP

assign o_axi_arid = 0; // for this demo, there is only one AXI slave

// what situations will render data requester (AXI master) busy to receive read response ??
// such as AXI interconnect where arbitration will fail to acquire the data transfer priority
// such as the internal cache storage to store the data from external slave memory is now full
// So, let's use a random value that is $anyseq in formal verification
assign o_axi_rready = (reset) ? 1 : `ifdef FORMAL $anyseq `else (!cache_is_full) `endif; 

// The master can wait for BVALID before asserting BREADY.
// The master can assert BREADY before BVALID is asserted.
assign o_axi_bready = (reset) ? 1 : `ifdef FORMAL $anyseq `else (i_axi_bvalid) `endif; 

wire address_read_transaction_is_accepted = (o_axi_arvalid) && (i_axi_arready);

reg [C_AXI_ADDR_WIDTH-1:0] araddr; // introduces another clock cycles of delay

always @(posedge clk)
begin
	if(reset) araddr <= {{(BITWIDTH_DIFFERENCE_ADDR_AND_BURST_LENGTH){1'b0}},
						 (o_axi_arlen+1'b1)} * (1 << o_axi_arsize);

	else if(address_read_transaction_is_accepted) 
		araddr <= araddr + {{(BITWIDTH_DIFFERENCE_ADDR_AND_BURST_LENGTH){1'b0}},
							(o_axi_arlen+1'b1)} * (1 << o_axi_arsize);
end

always @(posedge clk)
begin
	if(reset) o_axi_araddr <= 0;

	// When ARVALID & ARREADY are both high the next ARADDR can be generated 
	// because the current address for the current transfer is now complete (ARVALID & ARREADY).
	else if(address_read_transaction_is_accepted) 
		o_axi_araddr <= araddr; // increments slave address to read instructions from
end


/* verilator lint_off UNUSED */
wire arm_write_param_enable; // neural network layers to start another intermediate computations
wire [C_AXI_DATA_WIDTH-1:0] arm_write_param_data; // NN params going to neural network layers

wire cache_is_empty; // no NN params to feed into the neural network layers

wire [$clog2(C_SIZE_OF_CACHE)-1:0] cache_address_for_reading;
assign cache_address_for_reading = 0; // for testing only
/* verilator lint_on UNUSED */


wire valid_read_response_does_not_contain_error_messages = i_axi_rvalid && (i_axi_rresp == 0);

wire cache_is_full; // needed since C_SIZE_OF_CACHE is always smaller than SIZE_OF_SLAVE_MEMORY


// this acts as intermediate cache (much smaller size than slave memory)
cache_controller #(.C_DATA_WIDTH(C_AXI_DATA_WIDTH), .C_SIZE_OF_CACHE(C_SIZE_OF_CACHE)) cache_mem
(
	.clk(clk), .reset(reset),
  	.i_data(i_axi_rdata),   // data coming from slave memory
  	.i_data_is_valid   		// slave data is valid
	 ((o_axi_rready && valid_read_response_does_not_contain_error_messages)),
	.i_addr(cache_address_for_reading),
	.full(cache_is_full), 
	.o_data(arm_write_param_data), 
	.o_data_is_valid(arm_write_param_enable), 
	.empty(cache_is_empty) 
);

`ifdef FORMAL

localparam ADDR_INDEX = 1;

wire [C_AXI_ADDR_WIDTH-1:0] ADDRESS_IN_REQUEST 
							= ADDR_INDEX * (o_axi_arlen+1'b1) * (1 << o_axi_arsize);

wire retry_transaction_after_nack = o_axi_bready && i_axi_bvalid && write_response_is_not_ok;

initial assume(reset);

reg first_clock_had_passed = 0;

always @(posedge clk) first_clock_had_passed <= 1;

/*
always @(posedge clk)
begin
	if(first_clock_had_passed)
	begin
		cover(o_axi_araddr >= SECOND_ADDRESS_IN_REQUEST);
		cover(!o_axi_rready);
		cover(address_read_transaction_is_accepted);
	end
end
*/

always @(posedge clk) 
begin
	if(first_clock_had_passed) 
	begin
		cover((o_axi_araddr >= ADDRESS_IN_REQUEST) 
				&& $past(retry_transaction_after_nack, (AxLEN+1)));
		//cover((o_axi_araddr >= ADDRESS_IN_REQUEST) && address_read_transaction_is_accepted);
	end
end
`endif

endmodule

axi_slave_ram.v

/*

Copyright (c) 2018 Alex Forencich

Permission is hereby granted, free of charge, to any person obtaining a copy
of this software and associated documentation files (the "Software"), to deal
in the Software without restriction, including without limitation the rights
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:

The above copyright notice and this permission notice shall be included in
all copies or substantial portions of the Software.

THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
THE SOFTWARE.

*/

// Language: Verilog 2001

`timescale 1ns / 1ps

/*
 * AXI4 RAM
 */
module axi_slave_ram #
(
`ifdef FORMAL
	// Width of address bus in bits
	parameter C_AXI_ADDR_WIDTH = 12,
	// Width of data bus in bits
	parameter C_AXI_DATA_WIDTH = 8, // related to AxSIZE
`else
	// Width of address bus in bits
	parameter C_AXI_ADDR_WIDTH = 12, // just for random test
	// Width of data bus in bits
	parameter C_AXI_DATA_WIDTH = 128, // related to AxSIZE
`endif

    // Width of wstrb (width of data bus in words)
    parameter STRB_WIDTH = (C_AXI_DATA_WIDTH/8),
    // Width of ID signal
    parameter ID_WIDTH = 1,
    // Extra pipeline register on output
    parameter PIPELINE_OUTPUT = 0
)
(
    input  wire                   clk,
    input  wire                   rst,

    input  wire [ID_WIDTH-1:0]    s_axi_awid,
    input  wire [C_AXI_ADDR_WIDTH-1:0]  s_axi_awaddr,
    input  wire [7:0]             s_axi_awlen,
    input  wire [2:0]             s_axi_awsize,
    input  wire [1:0]             s_axi_awburst,
    input  wire                   s_axi_awlock,
    input  wire [3:0]             s_axi_awcache,
    input  wire [2:0]             s_axi_awprot,
    input  wire                   s_axi_awvalid,
    output wire                   s_axi_awready,
    input  wire [C_AXI_DATA_WIDTH-1:0]  s_axi_wdata,
    input  wire [STRB_WIDTH-1:0]  s_axi_wstrb,
    input  wire                   s_axi_wlast,
    input  wire                   s_axi_wvalid,
    output wire                   s_axi_wready,
    output wire [ID_WIDTH-1:0]    s_axi_bid,
    output wire [1:0]             s_axi_bresp,
    output wire                   s_axi_bvalid,
    input  wire                   s_axi_bready,
    input  wire [ID_WIDTH-1:0]    s_axi_arid,
    input  wire [C_AXI_ADDR_WIDTH-1:0]  s_axi_araddr,
    input  wire [7:0]             s_axi_arlen,
    input  wire [2:0]             s_axi_arsize,
    input  wire [1:0]             s_axi_arburst,
    input  wire                   s_axi_arlock,
    input  wire [3:0]             s_axi_arcache,
    input  wire [2:0]             s_axi_arprot,
    input  wire                   s_axi_arvalid,
    output wire                   s_axi_arready,
    output wire [ID_WIDTH-1:0]    s_axi_rid,
    output wire [C_AXI_DATA_WIDTH-1:0]  s_axi_rdata,
    output wire [1:0]             s_axi_rresp,
    output wire                   s_axi_rlast,
    output wire                   s_axi_rvalid,
    input  wire                   s_axi_rready
);

parameter VALID_ADDR_WIDTH = C_AXI_ADDR_WIDTH - $clog2(STRB_WIDTH);
parameter WORD_WIDTH = STRB_WIDTH;
parameter WORD_SIZE = C_AXI_DATA_WIDTH/WORD_WIDTH;

// bus width assertions
initial begin
    if (WORD_SIZE * STRB_WIDTH != C_AXI_DATA_WIDTH) begin
        $error("Error: AXI data width not evenly divisble (instance %m)");
        $finish;
    end

    if (2**$clog2(WORD_WIDTH) != WORD_WIDTH) begin
        $error("Error: AXI word width must be even power of two (instance %m)");
        $finish;
    end
end

localparam [0:0]
    READ_STATE_IDLE = 1'd0,
    READ_STATE_BURST = 1'd1;

reg [0:0] read_state_reg = READ_STATE_IDLE, read_state_next;

localparam [1:0]
    WRITE_STATE_IDLE = 2'd0,
    WRITE_STATE_BURST = 2'd1,
    WRITE_STATE_RESP = 2'd2;

reg [1:0] write_state_reg = WRITE_STATE_IDLE, write_state_next;

reg mem_wr_en;
reg mem_rd_en;

reg [ID_WIDTH-1:0] read_id_reg = {ID_WIDTH{1'b0}}, read_id_next;
reg [C_AXI_ADDR_WIDTH-1:0] read_addr_reg = {C_AXI_ADDR_WIDTH{1'b0}}, read_addr_next;
reg [7:0] read_count_reg = 8'd0, read_count_next;
reg [2:0] read_size_reg = 3'd0, read_size_next;
reg [1:0] read_burst_reg = 2'd0, read_burst_next;
reg [ID_WIDTH-1:0] write_id_reg = {ID_WIDTH{1'b0}}, write_id_next;
reg [C_AXI_ADDR_WIDTH-1:0] write_addr_reg = {C_AXI_ADDR_WIDTH{1'b0}}, write_addr_next;
reg [7:0] write_count_reg = 8'd0, write_count_next;
reg [2:0] write_size_reg = 3'd0, write_size_next;
reg [1:0] write_burst_reg = 2'd0, write_burst_next;

reg s_axi_awready_reg = 1'b0, s_axi_awready_next;
reg s_axi_wready_reg = 1'b0, s_axi_wready_next;
reg [ID_WIDTH-1:0] s_axi_bid_reg = {ID_WIDTH{1'b0}}, s_axi_bid_next;
reg s_axi_bvalid_reg = 1'b0, s_axi_bvalid_next;
reg s_axi_arready_reg = 1'b0, s_axi_arready_next;
reg [ID_WIDTH-1:0] s_axi_rid_reg = {ID_WIDTH{1'b0}}, s_axi_rid_next;
reg [C_AXI_DATA_WIDTH-1:0] s_axi_rdata_reg = {C_AXI_DATA_WIDTH{1'b0}}, s_axi_rdata_next;
reg s_axi_rlast_reg = 1'b0, s_axi_rlast_next;
reg s_axi_rvalid_reg = 1'b0, s_axi_rvalid_next;
reg [ID_WIDTH-1:0] s_axi_rid_pipe_reg = {ID_WIDTH{1'b0}};
reg [C_AXI_DATA_WIDTH-1:0] s_axi_rdata_pipe_reg = {C_AXI_DATA_WIDTH{1'b0}};
reg s_axi_rlast_pipe_reg = 1'b0;
reg s_axi_rvalid_pipe_reg = 1'b0;

// (* RAM_STYLE="BLOCK" *)
reg [C_AXI_DATA_WIDTH-1:0] mem[(2**VALID_ADDR_WIDTH)-1:0];

wire [VALID_ADDR_WIDTH-1:0] s_axi_awaddr_valid = s_axi_awaddr >> (C_AXI_ADDR_WIDTH - VALID_ADDR_WIDTH);
wire [VALID_ADDR_WIDTH-1:0] s_axi_araddr_valid = s_axi_araddr >> (C_AXI_ADDR_WIDTH - VALID_ADDR_WIDTH);
wire [VALID_ADDR_WIDTH-1:0] read_addr_valid = read_addr_reg >> (C_AXI_ADDR_WIDTH - VALID_ADDR_WIDTH);
wire [VALID_ADDR_WIDTH-1:0] write_addr_valid = write_addr_reg >> (C_AXI_ADDR_WIDTH - VALID_ADDR_WIDTH);

`ifdef FORMAL

reg first_clock_had_passed = 0;

always @(posedge clk) first_clock_had_passed <= 1;

wire [1:0] f_bresp = $anyseq;

always @(posedge clk) 
begin
	if(first_clock_had_passed)
		if($past(s_axi_bvalid && !s_axi_bready)) assume($stable(f_bresp));
end

`endif

assign s_axi_awready = s_axi_awready_reg;
assign s_axi_wready = s_axi_wready_reg;
assign s_axi_bid = s_axi_bid_reg;
assign s_axi_bresp = `ifdef FORMAL f_bresp `else (2'b00) `endif; 
assign s_axi_bvalid = s_axi_bvalid_reg;
assign s_axi_arready = s_axi_arready_reg;
assign s_axi_rid = PIPELINE_OUTPUT ? s_axi_rid_pipe_reg : s_axi_rid_reg;
assign s_axi_rdata = PIPELINE_OUTPUT ? s_axi_rdata_pipe_reg : s_axi_rdata_reg;
assign s_axi_rresp = 2'b00;
assign s_axi_rlast = PIPELINE_OUTPUT ? s_axi_rlast_pipe_reg : s_axi_rlast_reg;
assign s_axi_rvalid = PIPELINE_OUTPUT ? s_axi_rvalid_pipe_reg : s_axi_rvalid_reg;

integer i, j;

initial begin
    // two nested loops for smaller number of iterations per loop
    // workaround for synthesizer complaints about large loop counts
    for (i = 0; i < 2**VALID_ADDR_WIDTH; i = i + 2**(VALID_ADDR_WIDTH/2)) begin
        for (j = i; j < i + 2**(VALID_ADDR_WIDTH/2); j = j + 1) begin
            mem[j] = 0;
        end
    end
end

wire either_AW_or_W_channel_had_accepted_transaction 
		= (s_axi_wvalid && s_axi_wready) || (s_axi_awvalid && s_axi_awready);

always @* begin
    write_state_next = WRITE_STATE_IDLE;

    mem_wr_en = 1'b0;

    write_id_next = write_id_reg;
    write_addr_next = write_addr_reg;
    write_count_next = write_count_reg;
    write_size_next = write_size_reg;
    write_burst_next = write_burst_reg;

    s_axi_awready_next = 1'b0;
    s_axi_wready_next = 1'b0;
    s_axi_bid_next = s_axi_bid_reg;
    s_axi_bvalid_next = s_axi_bvalid_reg && !s_axi_bready;

    case (write_state_reg)
        WRITE_STATE_IDLE: begin
            s_axi_awready_next = 1'b1;

            if (s_axi_awready && s_axi_awvalid) begin
                write_id_next = s_axi_awid;
                write_addr_next = s_axi_awaddr;
                write_count_next = s_axi_awlen;
                write_size_next = s_axi_awsize < $clog2(STRB_WIDTH) ? s_axi_awsize : $clog2(STRB_WIDTH);
                write_burst_next = s_axi_awburst;

                s_axi_awready_next = 1'b0;
                s_axi_wready_next = 1'b1;
                write_state_next = WRITE_STATE_BURST;
            end else begin
                write_state_next = WRITE_STATE_IDLE;
            end
        end
        WRITE_STATE_BURST: begin
            s_axi_wready_next = 1'b1;

            if (s_axi_wready && s_axi_wvalid) begin
                mem_wr_en = 1'b1;
                if (write_burst_reg != 2'b00) begin
                    write_addr_next = write_addr_reg + (1 << write_size_reg);
                end
                write_count_next = write_count_reg - 1;
                if (write_count_reg > 0) begin
                    write_state_next = WRITE_STATE_BURST;
                end else begin
                    s_axi_wready_next = 1'b0;
                    if ((s_axi_bready || !s_axi_bvalid) && either_AW_or_W_channel_had_accepted_transaction) begin
                        s_axi_bid_next = write_id_reg;
                        s_axi_bvalid_next = 1'b1;
                        s_axi_awready_next = 1'b1;
                        write_state_next = WRITE_STATE_IDLE;
                    end else begin
                        write_state_next = WRITE_STATE_RESP;
                    end
                end
            end else begin
                write_state_next = WRITE_STATE_BURST;
            end
        end
        WRITE_STATE_RESP: begin
            if ((s_axi_bready || !s_axi_bvalid) && either_AW_or_W_channel_had_accepted_transaction) begin
                s_axi_bid_next = write_id_reg;
                s_axi_bvalid_next = 1'b1;
                s_axi_awready_next = 1'b1;
                write_state_next = WRITE_STATE_IDLE;
            end else begin
                write_state_next = WRITE_STATE_RESP;
            end
        end
    endcase
end

always @(posedge clk) begin
    if (rst) begin
        write_state_reg <= WRITE_STATE_IDLE;
        s_axi_awready_reg <= 1'b0;
        s_axi_wready_reg <= 1'b0;
        s_axi_bvalid_reg <= 1'b0;
    end else begin
        write_state_reg <= write_state_next;
        s_axi_awready_reg <= s_axi_awready_next;
        s_axi_wready_reg <= s_axi_wready_next;
        s_axi_bvalid_reg <= s_axi_bvalid_next;
    end

    write_id_reg <= write_id_next;
    write_addr_reg <= write_addr_next;
    write_count_reg <= write_count_next;
    write_size_reg <= write_size_next;
    write_burst_reg <= write_burst_next;

    s_axi_bid_reg <= s_axi_bid_next;

    for (i = 0; i < WORD_WIDTH; i = i + 1) begin
        if (mem_wr_en & s_axi_wstrb[i]) begin
            mem[write_addr_valid][WORD_SIZE*i +: WORD_SIZE] <= s_axi_wdata[WORD_SIZE*i +: WORD_SIZE];
        end
    end
end

always @* begin
    read_state_next = READ_STATE_IDLE;

    mem_rd_en = 1'b0;

    s_axi_rid_next = s_axi_rid_reg;
    s_axi_rlast_next = s_axi_rlast_reg;
    s_axi_rvalid_next = s_axi_rvalid_reg && !(s_axi_rready || (PIPELINE_OUTPUT && !s_axi_rvalid_pipe_reg));

    read_id_next = read_id_reg;
    read_addr_next = read_addr_reg;
    read_count_next = read_count_reg;
    read_size_next = read_size_reg;
    read_burst_next = read_burst_reg;

    s_axi_arready_next = 1'b0;

    case (read_state_reg)
        READ_STATE_IDLE: begin
            s_axi_arready_next = 1'b1;

            if (s_axi_arready && s_axi_arvalid) begin
                read_id_next = s_axi_arid;
                read_addr_next = s_axi_araddr;
                read_count_next = s_axi_arlen;
                read_size_next = s_axi_arsize < $clog2(STRB_WIDTH) ? s_axi_arsize : $clog2(STRB_WIDTH);
                read_burst_next = s_axi_arburst;

                s_axi_arready_next = 1'b0;
                read_state_next = READ_STATE_BURST;
            end else begin
                read_state_next = READ_STATE_IDLE;
            end
        end
        READ_STATE_BURST: begin
            if (s_axi_rready || (PIPELINE_OUTPUT && !s_axi_rvalid_pipe_reg) || !s_axi_rvalid_reg) begin
                mem_rd_en = 1'b1;
                s_axi_rvalid_next = 1'b1;
                s_axi_rid_next = read_id_reg;
                s_axi_rlast_next = read_count_reg == 0;
                if (read_burst_reg != 2'b00) begin
                    read_addr_next = read_addr_reg + (1 << read_size_reg);
                end
                read_count_next = read_count_reg - 1;
                if (read_count_reg > 0) begin
                    read_state_next = READ_STATE_BURST;
                end else begin
                    s_axi_arready_next = 1'b1;
                    read_state_next = READ_STATE_IDLE;
                end
            end else begin
                read_state_next = READ_STATE_BURST;
            end
        end
    endcase
end

always @(posedge clk) begin
    if (rst) begin
        read_state_reg <= READ_STATE_IDLE;
        s_axi_arready_reg <= 1'b0;
        s_axi_rvalid_reg <= 1'b0;
        s_axi_rvalid_pipe_reg <= 1'b0;
    end else begin
        read_state_reg <= read_state_next;
        s_axi_arready_reg <= s_axi_arready_next;
        s_axi_rvalid_reg <= s_axi_rvalid_next;

        if (!s_axi_rvalid_pipe_reg || s_axi_rready) begin
            s_axi_rvalid_pipe_reg <= s_axi_rvalid_reg;
        end
    end

    read_id_reg <= read_id_next;
    read_addr_reg <= read_addr_next;
    read_count_reg <= read_count_next;
    read_size_reg <= read_size_next;
    read_burst_reg <= read_burst_next;

    s_axi_rid_reg <= s_axi_rid_next;
    s_axi_rlast_reg <= s_axi_rlast_next;

    if (mem_rd_en) begin
        s_axi_rdata_reg <= mem[read_addr_valid];
    end

    if (!s_axi_rvalid_pipe_reg || s_axi_rready) begin
        s_axi_rid_pipe_reg <= s_axi_rid_reg;
        s_axi_rdata_pipe_reg <= s_axi_rdata_reg;
        s_axi_rlast_pipe_reg <= s_axi_rlast_reg;
    end
end

endmodule

cache_controller.v

module cache_controller(clk, reset, i_addr, i_data, o_data, i_data_is_valid, o_data_is_valid, full, empty);

`ifdef FORMAL
	parameter C_DATA_WIDTH = 8; 
	parameter C_SIZE_OF_CACHE = 4;
`else
	parameter C_DATA_WIDTH = 128; 
	parameter C_SIZE_OF_CACHE = 64;
`endif

input clk, reset;
input i_data_is_valid; // input data is valid
input [C_DATA_WIDTH-1:0] i_data;
input [$clog2(C_SIZE_OF_CACHE)-1:0] i_addr; // address for reading cache content
output full;
output empty;
output reg o_data_is_valid; // output data is valid
output reg [C_DATA_WIDTH-1:0] o_data;

reg [C_DATA_WIDTH-1:0] cache [C_SIZE_OF_CACHE-1:0]; // in Xilinx vivado, this infers BRAM
reg [$clog2(C_SIZE_OF_CACHE)-1:0] cache_index;

localparam INTEGER_BITWIDTH = 32;
localparam BITWIDTH_DIFFERENCE_DATA_AND_INTEGER = (C_DATA_WIDTH > INTEGER_BITWIDTH) ? 
			C_DATA_WIDTH-INTEGER_BITWIDTH : INTEGER_BITWIDTH-C_DATA_WIDTH;

integer cache_entry_index; // address for writing cache content

always @(posedge clk)
begin
	if(reset) 
	begin
		cache_index <= 0;

		for(cache_entry_index = 0; cache_entry_index < C_SIZE_OF_CACHE; 
			cache_entry_index = cache_entry_index + 1)
		begin
			`ifdef FORMAL
				cache[cache_entry_index] <= cache_entry_index[C_DATA_WIDTH-1:0]; // acts as random initialization
			`else
				cache[cache_entry_index] <= {{(BITWIDTH_DIFFERENCE_DATA_AND_INTEGER){1'b0}}, cache_entry_index}; // acts as random initialization
			`endif
		end
	end

	else if(i_data_is_valid && !full) 
	begin
		cache[cache_index] <= i_data;
		cache_index <= cache_index + 1;
	end
end


always @(posedge clk)
begin
	if(reset) 
	begin
		o_data <= 0;
		o_data_is_valid <= 0;
	end

	else if(!empty) 
	begin
		o_data <= cache[i_addr];
		o_data_is_valid <= 1;
	end
end

localparam SKID_BUFFER_BACKPRESSURE_SPACE = 1;

assign empty = (reset) ? 1 : (cache_index == 0);
assign full = (reset) ? 0 : (cache_index == (C_SIZE_OF_CACHE[$clog2(C_SIZE_OF_CACHE)-1:0]-1));

endmodule