| 
				
				
				
				 | 
			
			 | 
			@@ -1,204 +0,0 @@ | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			interface axi_slave_if (input bit clk, resetn);
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			 ///////////////////write address channel
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			 input  logic  awvalid; /// master is sending new address 
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			 output logic awready; /// slave is ready to accept request
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			 input  logic  [3:0] awid; ////// unique ID for each transaction
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			 input  logic  [3:0] awlen; ////// burst length AXI3 : 1 to 16, AXI4 : 1 to 256
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			 input  logic  [2:0] awsize; ////unique transaction size : 1,2,4,8,16 ...128 bytes
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			 input  logic  [31:0] awaddr; ////write adress of transaction
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			 input  logic  [1:0] awburst; ////burst type : fixed , INCR , WRAP
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			 
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			 /////////////////////write data channel
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			 input  logic  wvalid; //// master is sending new data
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			 output logic  wready; //// slave is ready to accept new data 
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			 input  logic  [3:0] wid; /// unique id for transaction
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			 input  logic  [31:0] wdata; //// data 
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			 input  logic  [3:0] wstrb; //// lane having valid data
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			 input  logic  wlast, //// last transfer in write burst
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			 ///////////////write response channel
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			 input  logic  bready; ///master is ready to accept response
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			 output logic  bvalid; //// slave has valid response
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			 output logic  [3:0] bid; ////unique id for transaction
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			 output logic  [1:0] bresp; /// status of write transaction
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			 ////////////// read address channel
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			 output logic  reg arready; //read address ready signal from slave
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			 input  logic  [3:0] arid; //read address id
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			 input  logic  [31:0] araddr; //read address signal
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			 input  logic  [3:0] arlen; //length of the burst
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			 input  logic  [2:0] arsize; //number of bytes in a transfer
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			 input  logic  [1:0] arburst;//burst type - fixed, incremental, wrapping
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			 input  logic  arvalid; //address read valid signal
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			///////////////////read data channel
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			output logic  [3:0] rid; //read data id
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			output logic  [31:0]rdata; //read data from slave
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			output logic  [1:0] rresp; //read response signal
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			output logic   rlast; //read data last signal
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			output logic   rvalid; //read data valid signal
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			input  logic   rready
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			//========================== ASSERTIONS========================
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			// WRITE ADDRESS CHANNEL************************************************************************************************************
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			//1st.(When awvalid is asserted then it remains asserted until awready is HIGH)
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			property AXI_AWVALID_AWREADY;  
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			       @(posedge clk) awvalid |-> (awvalid throughout (awready[->1]));
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			endproperty
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			A1:assert property (AXI_AWVALID_AWREADY); 
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			    else `uvm_error("ASSERTION","Failure AXI_AWVALID_AWREADY");
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			//2nd.(BURST can not cross a 4KB Boundary)
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			property w_burst_boundary; 
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			       @(posedge clk) (awvalid && awready) |-> (((2**awsize)*(awlen+1)) < 4096) ;
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			endproperty 
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			A2:assert property (w_burst_boundary)
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			    else `uvm_error("ASSERTION","Failure w_burst_boundary");
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			//3rd.(all write address channel remains stable after AWVALID is asserted)
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			     property AXI_AWVALID_STABLE;
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			        @(posedge clk) $rose(awvalid)|->($stable(awid)&& $stable(awaddr)
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			                                        &&$stable(awlen)&& $stable(awsize) 
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			                                        &&$stable(awburst))throughout awready[->1];
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			    endproperty
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			  A3:assert property (AXI_AWVALID_STABLE)
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			        else `uvm_error("ASSERTION","Failure AXI_AWVALID_STABLE");
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			//4th.(AWLEN value is 1,3,7,15 for Wrapping type Burst)
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			   property AWLEN_WRAP_BURST;
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			    @(posedge clk) disable iff(!resetn) (awburst==2'b10) |->(awlen==1|awlen==3||awlen==7||awlen==15);
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			   endproperty
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			    A4:assert property (AWLEN_WRAP_BURST)
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			    else `uvm_error("ASSERTION","Failure AWLEN_WRAP_BURST");
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			//5th.(AWBURST val cant be 2'b11)
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			   property AWBURST_CANT_2b11; 
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			      @(posedge clk) (awvalid && awready) |-> (awburst != 2'b11);
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			   endproperty
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			  A5:assert property (AWBURST_CANT_2b11)
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			    else  `uvm_error("ASSERTION","Failure AWBURST_CANT_2b11");
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			//WRITE DATA CHANNEL**************************************************************************************************************
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			//1st.
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			  property AXI_WVALID_WREADY;
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			  @(posedge clk) wvalid |-> (wvalid throughout (wready[->1])) ;
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			  endproperty
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			 A6: assert property (AXI_WVALID_WREADY)  
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			    else `uvm_error("ASSERTION","Failure AXI_WVALID_WREADY");
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			//2nd. Property to check whether all write address channel remains stable after WVALID is asserted
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			    property AXI_WVALID_WREADY;
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			        @(posedge clk) $rose(wvalid) |-> (  $stable(wid) 
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			                                            && $stable(wdata)
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			                                            && $stable(wstrb)
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			                                            && $stable(wlast)) throughout wready[->1];
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			    endproperty
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			A7:assert property (AXI_WVALID_STABLE)
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			     else `uvm_error("ASSERTION","Failure AXI_WVALID_STABLE");
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			//WRITE RESPONSE CHANNEL****************************************************************************************************************
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			//1st.
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			  property AXI_BVALID_BREADY;
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			  @(posedge clk) bvalid|-> (bvalid throughout (bready[->1])) ;
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			  endproperty
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			  A8:assert property (AXI_BVALID_BREADY)  
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			     else `uvm_error("ASSERTION","Failure AXI_BVALID_BREADY");
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			//2nd.to check whether all write address channel remains stable after BVALID is asserted
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			    property AXI_BVALID_STABLE;
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			      @(posedge clk) $rose(bvalid)|->($stable(bid)&& $stable(bresp))throughout bready[->1];
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			    endproperty
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			  A9:assert property (AXI_BVALID_STABLE)
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			    else `uvm_error("ASSERTION","Failure AXI_BVALID_STABLE");
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			//READ ADDRESS CHANNEL***********************************************************************************************
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			//1st.
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			  property AXI_ARVALID_ARREADY;
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			       @(posedge clk) arvalid |-> (arvalid throughout (arready[->1])) ;
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			  endproperty
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			  B1:assert property AXI_ARVALID_ARREADY; 
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			    else`uvm_error("ASSERTION","Failure AXI_ARVALID_ARREADY");
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			//2nd.(BURST can not cross a 4KB Boundary)
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			  property r_burst_boubadary;  
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			       @(posedge clk) (arvalid && arready) |-> (((2**arsize)*(arlen+1)) < 4096);
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			  endproperty
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			 B2:assert property (r_burst_boubadary)
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			    else `uvm_error("ASSERTION","Failure r_burst_boubadary");
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			//3rd.(ARLEN value is 1,3,7,15 for Wrapping type Burst)
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			  property ARLEN_WRAP_BURST;
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			    @(posedge clk) disable iff (!resetn) (arburst==2'b10) |-> (arlen==1 || arlen==3 || arlen==7 || arlen==15);
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			  endproperty
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			 B3:assert property (ARLEN_WRAP_BURST)
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			    else `uvm_error("ASSERTION","Failure ARLEN_WRAP_BURST");
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			//4th.(arburst val cant be 2'b11)
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			  property ARBURST_CANT_2b11; //
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			    @(posedge clk) (arvalid && arready) |-> (arburst != 2'b11);
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			  endproperty
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			 B4:assert property (ARBURST_CANT_2b11)
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			    else `uvm_error("ASSERTION","Failure ARBURST_CANT_2b11");
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			//5th. Property to check whether all write address channel remains stable after ARVALID is asserted
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			    property  AXI_ARVALID_STABLE;
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			          @(posedge clk) $rose(arvalid) |-> ( $stable(arid)   
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			                                            &&$stable(araddr)
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			                                            &&$stable(arlen)
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			                                            &&$stable(arsize) 
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			                                            &&$stable(arburst)) throughout arready[->1];
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			    endproperty
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			 B5:assert property (AXI_ARVALID_STABLE)
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			    else `uvm_error("ASSERTION","Failure AXI_ARVALID_STABLE");
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			//READ DATA CHANNEL***********************************************************************************************************
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			/1st.
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			  property AXI_RVALID_RREADY;
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			       @(posedge clk) rvalid |-> (rvalid throughout (rready[->1])); 
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			  endproperty
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			 B6:assert property (AXI_RVALID_RREADY)  
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			    else `uvm_error("ASSERTION","Failure AXI_RVALID_RREADY");
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			//2nd.to check whether all write address channel remains stable after RVALID is asserted
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			    property AXI_RVALID_STABLE;
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			        @(posedge clk) $rose(rvalid) |-> (  $stable(rid) 
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			                                            && $stable(rdata)
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			                                            && $stable(rresp)
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			                                            && $stable(rlast)) throughout rready[->1];
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			    endproperty
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			 B7:assert property (AXI_RVALID_STABLE)
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			    else`uvm_error("ASSERTION","Failure AXI_RVALID_STABLE");
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			   
 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			endinterface
 |