AXI-Verification/axi_slave_if.sv

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