axipc.v

amba3 sva 完全验证的代码

   RUSER,
   RVALID,
   RREADY,

   // Low power interface
   CACTIVE,
   CSYSREQ,
   CSYSACK
   );


//------------------------------------------------------------------------------
// INDEX:   1) Parameters
//------------------------------------------------------------------------------


  // INDEX:        - Configurable (user can set)
  // =====
  // Parameters below can be set by the user.

  // Set DATA_WIDTH to the data-bus width required
  parameter DATA_WIDTH = 64;         // data bus width, default = 64-bit

  // Select the number of channel ID bits required
  parameter ID_WIDTH = 4;          // (A|W|R|B)ID width

  // Select the size of the USER buses, default = 32-bit
  parameter AWUSER_WIDTH = 32; // width of the user AW sideband field
  parameter WUSER_WIDTH  = 32; // width of the user W  sideband field
  parameter BUSER_WIDTH  = 32; // width of the user B  sideband field
  parameter ARUSER_WIDTH = 32; // width of the user AR sideband field
  parameter RUSER_WIDTH  = 32; // width of the user R  sideband field

  // Write-interleave Depth of monitored slave interface
  parameter WDEPTH = 1;

  // Size of CAMs for storing outstanding read bursts, this should match or
  // exceed the number of outstanding read addresses accepted into the slave
  // interface
  parameter MAXRBURSTS = 16;

  // Size of CAMs for storing outstanding write bursts, this should match or
  // exceed the number of outstanding write bursts into the slave  interface
  parameter MAXWBURSTS = 16;

  // Maximum number of cycles between VALID -> READY high before a warning is
  // generated
  parameter MAXWAITS = 16;

  // OVL instances property_type parameter (0=assert, 1=assume, 2=ignore)
  parameter AXI_ERRM_PropertyType = 0; // default: assert Master is AXI compliant
  parameter AXI_RECM_PropertyType = 0; // default: assert Master is AXI compliant
  parameter AXI_AUXM_PropertyType = 0; // default: assert Master auxiliary logic checks
  //
  parameter AXI_ERRS_PropertyType = 0; // default: assert Slave is AXI compliant
  parameter AXI_RECS_PropertyType = 0; // default: assert Slave is AXI compliant
  parameter AXI_AUXS_PropertyType = 0; // default: assert Slave auxiliary logic checks
  //
  parameter AXI_ERRL_PropertyType = 0; // default: assert LP Int is AXI compliant

  // Recommended Rules Enable
  parameter RecommendOn   = 1'b1;   // enable/disable reporting of all  AXI_REC*_* rules
  parameter RecMaxWaitOn  = 1'b1;   // enable/disable reporting of just AXI_REC*_MAX_WAIT rules


  // INDEX:        - Calculated (user should not override)
  // =====
  // Do not override the following parameters: they must be calculated exactly
  // as shown below
  parameter DATA_MAX   = DATA_WIDTH-1; // data max index
  parameter STRB_WIDTH = DATA_WIDTH/8; // WSTRB width
  parameter STRB_MAX   = STRB_WIDTH-1; // WSTRB max index
  parameter STRB_1     = {{STRB_MAX{1'b0}}, 1'b1};  // value 1 in strobe width
  parameter ID_MAX     = ID_WIDTH-1;   // ID max index
  parameter ID_HI      = (1 << ID_WIDTH) - 1; // ID max value

  parameter AWUSER_MAX = AWUSER_WIDTH-1; // AWUSER max index
  parameter  WUSER_MAX =  WUSER_WIDTH-1; // WUSER  max index
  parameter  BUSER_MAX =  BUSER_WIDTH-1; // BUSER  max index
  parameter ARUSER_MAX = ARUSER_WIDTH-1; // ARUSER max index
  parameter  RUSER_MAX =  RUSER_WIDTH-1; // RUSER  max index

  // WSTRB16...WSTRB1 ID BURST[1:0] ASIZE[2:0] ALEN[3:0] LAST ADDR[3:0]
  parameter ADDRLO   = 0;                 // ADDRLO   =   0
  parameter ADDRHI   = 6;                 // ADDRHI   =   6
  parameter EXCL     = ADDRHI + 1;        // EXCL     =   7 if ADDRHI=6 (ADDRHI+1)
  parameter ALENLO   = EXCL + 1;          // ALENLO   =   8 if ADDRHI=6 (ADDRHI+2)
  parameter ALENHI   = ALENLO + 3;        // ALENHI   =  11 if ADDRHI=6 (ADDRHI+5)
  parameter ASIZELO  = ALENHI + 1;        // ASIZELO  =  12 if ADDRHI=6 (ADDRHI+6)
  parameter ASIZEHI  = ASIZELO + 2;       // ASIZEHI  =  14 if ADDRHI=6 (ADDRHI+8)
  parameter BURSTLO  = ASIZEHI + 1;       // BURSTLO  =  15 if ADDRHI=6 (ADDRHI+9)
  parameter BURSTHI  = BURSTLO + 1;       // BURSTHI  =  16 if ADDRHI=6 (ADDRHI+10)
  parameter IDLO     = BURSTHI + 1;       // IDLO     =  17 if ADDRHI=6 (ADDRHI+11)
  parameter IDHI     = IDLO+ID_MAX;       // IDHI     =  20 if ADDRHI=6 & ID_WIDTH=4
  parameter STRB1LO  = IDHI+1;            // STRB1LO  =  21 if ADDRHI=6 & ID_WIDTH=4 & STRB_MAX=7
  parameter STRB1HI  = STRB1LO+STRB_MAX;  // STRB1HI  =  28 if ADDRHI=6 & ID_WIDTH=4 & STRB_MAX=7
  parameter STRB2LO  = STRB1HI+1;         // STRB2LO  =  29 if ADDRHI=6 & ID_WIDTH=4 & STRB_MAX=7
  parameter STRB2HI  = STRB2LO+STRB_MAX;  // STRB2HI  =  36 if ADDRHI=6 & ID_WIDTH=4 & STRB_MAX=7
  parameter STRB3LO  = STRB2HI+1;         // STRB3LO  =  37 if ADDRHI=6 & ID_WIDTH=4 & STRB_MAX=7
  parameter STRB3HI  = STRB3LO+STRB_MAX;  // STRB3HI  =  44 if ADDRHI=6 & ID_WIDTH=4 & STRB_MAX=7
  parameter STRB4LO  = STRB3HI+1;         // STRB4LO  =  45 if ADDRHI=6 & ID_WIDTH=4 & STRB_MAX=7
  parameter STRB4HI  = STRB4LO+STRB_MAX;  // STRB4HI  =  52 if ADDRHI=6 & ID_WIDTH=4 & STRB_MAX=7
  parameter STRB5LO  = STRB4HI+1;         // STRB5LO  =  53 if ADDRHI=6 & ID_WIDTH=4 & STRB_MAX=7
  parameter STRB5HI  = STRB5LO+STRB_MAX;  // STRB5HI  =  60 if ADDRHI=6 & ID_WIDTH=4 & STRB_MAX=7
  parameter STRB6LO  = STRB5HI+1;         // STRB6LO  =  61 if ADDRHI=6 & ID_WIDTH=4 & STRB_MAX=7
  parameter STRB6HI  = STRB6LO+STRB_MAX;  // STRB6HI  =  68 if ADDRHI=6 & ID_WIDTH=4 & STRB_MAX=7
  parameter STRB7LO  = STRB6HI+1;         // STRB7LO  =  69 if ADDRHI=6 & ID_WIDTH=4 & STRB_MAX=7
  parameter STRB7HI  = STRB7LO+STRB_MAX;  // STRB7HI  =  76 if ADDRHI=6 & ID_WIDTH=4 & STRB_MAX=7
  parameter STRB8LO  = STRB7HI+1;         // STRB8LO  =  77 if ADDRHI=6 & ID_WIDTH=4 & STRB_MAX=7
  parameter STRB8HI  = STRB8LO+STRB_MAX;  // STRB8HI  =  84 if ADDRHI=6 & ID_WIDTH=4 & STRB_MAX=7
  parameter STRB9LO  = STRB8HI+1;         // STRB9LO  =  85 if ADDRHI=6 & ID_WIDTH=4 & STRB_MAX=7
  parameter STRB9HI  = STRB9LO+STRB_MAX;  // STRB9HI  =  92 if ADDRHI=6 & ID_WIDTH=4 & STRB_MAX=7
  parameter STRB10LO = STRB9HI+1;         // STRB10LO =  93 if ADDRHI=6 & ID_WIDTH=4 & STRB_MAX=7
  parameter STRB10HI = STRB10LO+STRB_MAX; // STRB10HI = 100 if ADDRHI=6 & ID_WIDTH=4 & STRB_MAX=7
  parameter STRB11LO = STRB10HI+1;        // STRB11LO = 101 if ADDRHI=6 & ID_WIDTH=4 & STRB_MAX=7
  parameter STRB11HI = STRB11LO+STRB_MAX; // STRB11HI = 108 if ADDRHI=6 & ID_WIDTH=4 & STRB_MAX=7
  parameter STRB12LO = STRB11HI+1;        // STRB12LO = 109 if ADDRHI=6 & ID_WIDTH=4 & STRB_MAX=7
  parameter STRB12HI = STRB12LO+STRB_MAX; // STRB12HI = 116 if ADDRHI=6 & ID_WIDTH=4 & STRB_MAX=7
  parameter STRB13LO = STRB12HI+1;        // STRB13LO = 117 if ADDRHI=6 & ID_WIDTH=4 & STRB_MAX=7
  parameter STRB13HI = STRB13LO+STRB_MAX; // STRB13HI = 124 if ADDRHI=6 & ID_WIDTH=4 & STRB_MAX=7
  parameter STRB14LO = STRB13HI+1;        // STRB14LO = 125 if ADDRHI=6 & ID_WIDTH=4 & STRB_MAX=7
  parameter STRB14HI = STRB14LO+STRB_MAX; // STRB14HI = 132 if ADDRHI=6 & ID_WIDTH=4 & STRB_MAX=7
  parameter STRB15LO = STRB14HI+1;        // STRB15LO = 133 if ADDRHI=6 & ID_WIDTH=4 & STRB_MAX=7
  parameter STRB15HI = STRB15LO+STRB_MAX; // STRB15HI = 140 if ADDRHI=6 & ID_WIDTH=4 & STRB_MAX=7
  parameter STRB16LO = STRB15HI+1;        // STRB16LO = 141 if ADDRHI=6 & ID_WIDTH=4 & STRB_MAX=7
  parameter STRB16HI = STRB16LO+STRB_MAX; // STRB16HI = 148 if ADDRHI=6 & ID_WIDTH=4 & STRB_MAX=7


//------------------------------------------------------------------------------
// INDEX:   2) Inputs (no outputs)
//------------------------------------------------------------------------------


  // INDEX:        - Global Signals
  // =====
  input                ACLK;        // AXI Clock
  input                ARESETn;     // AXI Reset


  // INDEX:        - Write Address Channel
  // =====
  input     [ID_MAX:0] AWID;
  input         [31:0] AWADDR;
  input          [3:0] AWLEN;
  input          [2:0] AWSIZE;
  input          [1:0] AWBURST;
  input          [3:0] AWCACHE;
  input          [2:0] AWPROT;
  input          [1:0] AWLOCK;
  input [AWUSER_MAX:0] AWUSER;
  input                AWVALID;
  input                AWREADY;


  // INDEX:        - Write Data Channel
  // =====
  input     [ID_MAX:0] WID;
  input   [DATA_MAX:0] WDATA;
  input   [STRB_MAX:0] WSTRB;
  input  [WUSER_MAX:0] WUSER;
  input                WLAST;
  input                WVALID;
  input                WREADY;


  // INDEX:        - Write Response Channel
  // =====
  input     [ID_MAX:0] BID;
  input          [1:0] BRESP;
  input  [BUSER_MAX:0] BUSER;
  input                BVALID;
  input                BREADY;


  // INDEX:        - Read Address Channel
  // =====
  input     [ID_MAX:0] ARID;
  input         [31:0] ARADDR;
  input          [3:0] ARLEN;
  input          [2:0] ARSIZE;
  input          [1:0] ARBURST;
  input          [3:0] ARCACHE;
  input          [2:0] ARPROT;
  input          [1:0] ARLOCK;
  input [ARUSER_MAX:0] ARUSER;
  input                ARVALID;
  input                ARREADY;


  // INDEX:        - Read Data Channel
  // =====
  input     [ID_MAX:0] RID;
  input   [DATA_MAX:0] RDATA;
  input          [1:0] RRESP;
  input  [RUSER_MAX:0] RUSER;
  input                RLAST;
  input                RVALID;
  input                RREADY;

  // INDEX:        - Low Power Interface
  // =====
  input                CACTIVE;
  input                CSYSREQ;
  input                CSYSACK;


//------------------------------------------------------------------------------
// INDEX:   3) Wire and Reg Declarations
//------------------------------------------------------------------------------

  // User signal definitions are defined as weak pull-down in the case
  // that they are unconnected.
  tri0 [AWUSER_MAX:0] AWUSER;
  tri0  [WUSER_MAX:0] WUSER;
  tri0  [BUSER_MAX:0] BUSER;
  tri0 [ARUSER_MAX:0] ARUSER;
  tri0  [RUSER_MAX:0] RUSER;

  // Low power interface signals are defined as weak pull-up in the case
  // that they are unconnected.
  tri1                CACTIVE;
  tri1                CSYSREQ;
  tri1                CSYSACK;

  // Write CAMs
  integer            WIndex;
  reg [STRB16HI:0]   WBurstCam[1:MAXWBURSTS]; // store outstanding write bursts
  reg [4:0]          WCountCam[1:MAXWBURSTS]; // number of write data stored
  reg                WLastCam[1:MAXWBURSTS];  // WLAST for outstanding writes
  reg                WAddrCam[1:MAXWBURSTS];  // flag for valid write addr
  reg                BRespCam[1:MAXWBURSTS];  // flag for valid write resp
  wire               nWOutstanding;       // flag for no write bursts oustanding
                                          // except for current valid write id

  // WDepth array
  reg [ID_HI:0]      WidInUse;     // WIDs in use for write depth check
  reg [ID_HI:0]      WidInUseNext; // Next value of WidInUse
  integer            WidDepth;

  // Read CAMs
  reg [3:0]          RLenCam[1:MAXRBURSTS];
  reg [ID_MAX:0]     RIdCam[1:MAXRBURSTS];
  reg                RExclCam[1:MAXRBURSTS];
  integer            RIndex;
  integer            RIndexNext;
  wire               RPop;
  wire               RPush;
  wire               nROutstanding; // flag for no read bursts oustanding
  reg                RIdCamDelta;   // flag indicates that RidCam has changed

  // Protocol error flags
  reg                WDataNumError;   // flag for AXI_ERRM_WDATA_NUM rule
  reg                WDataOrderError; // flag for AXI_ERRM_WDATA_ORDER rule
  reg                BrespError;      // flag for AXI_ERRS_BRESP rule
  reg                BrespExokError;  // flag for AXI_ERRS_BRESP_EXOKAY rule
  reg                StrbError;       // flag for AXI_ERRM_WSTRB rule

  // signals for checking for match in ID CAMs
  integer            AidMatch;
  integer            WidMatch;
  integer            RidMatch;
  integer            BidMatch;

  reg          [6:0] AlignMaskR; // mask for checking read address alignment
  reg          [6:0] AlignMaskW; // mask for checking write address alignment

  // signals for Address Checking
  reg         [31:0] ArAddrIncr;
  reg         [31:0] AwAddrIncr;

  // signals for Data Checking
  reg   [DATA_MAX:0] WdataMask;
  reg         [10:0] ArSizeInBits;
  reg         [10:0] AwSizeInBits;
  reg         [11:0] ArLenInBytes;
  wire         [3:0] ArLenPending;
  wire               ArExclPending;

  // Lock signals
  wire               AWLockNew; // New locked write address valid
  wire               ARLockNew; // New locked read address valid
  reg          [1:0] LockState;
  reg          [1:0] LockStateNext;
  reg     [ID_MAX:0] LockIdNext;
  reg     [ID_MAX:0] LockId;
  reg          [3:0] LockCacheNext;
  reg          [3:0] LockCache;
  reg          [2:0] LockProtNext;
  reg          [2:0] LockProt;
  reg         [31:0] LockAddrNext;
  reg         [31:0] LockAddr;

  // arrays to store exclusive access control info
  reg                ExclReadAddr[ID_HI:0]; // tracks excl read addr
  reg                ExclReadData[ID_HI:0]; // tracks excl read data
  reg         [31:0] ExclAddr[ID_HI:0];
  reg          [2:0] ExclSize[ID_HI:0];
  reg          [3:0] ExclLen[ID_HI:0];
  reg          [1:0] ExclBurst[ID_HI:0];
  reg          [3:0] ExclCache[ID_HI:0];
  reg          [2:0] ExclProt[ID_HI:0];
  reg [AWUSER_MAX:0] ExclUser[ID_HI:0];
  reg         [10:0] ExclMask; // mask to check alignment of exclusive address


//------------------------------------------------------------------------------
// INDEX:   4) Verilog Defines
//------------------------------------------------------------------------------


  // INDEX:        - Lock FSM States
  // =====
  // Lock FSM States (3-state FSM, so one state encoding is not used)
  `define AXI_AUX_ST_UNLOCKED  2'b00
  `define AXI_AUX_ST_LOCKED    2'b01
  `define AXI_AUX_ST_LOCK_LAST 2'b10
  `define AXI_AUX_ST_NOT_USED  2'b11


  // INDEX:        - Clock and Reset
  // =====
  // Can be overridden by user for a clock enable.
  //
  // Can also be used to clock OVL on negedge (to avoid race hazards with
  // auxiliary logic) by compiling with the override:
  //
  //   +define+AXI_OVL_CLK=~ACLK
  // 
  // OVL: Assertion Instances
  `ifdef AXI_OVL_CLK
  `else
     `define AXI_OVL_CLK ACLK
  `endif
  //
  `ifdef AXI_OVL_RSTn
  `else