axipc.sv

amba3 sva 完全验证的代码

  `endif
  //
  `ifdef AXI_AUX_RSTn
  `else
     `define AXI_AUX_RSTn ARESETn
  `endif


//------------------------------------------------------------------------------
// INDEX:   5) Initialize simulation
//------------------------------------------------------------------------------
  initial
    begin

       // INDEX:        - Format for time reporting
       // =====
       // Format for time reporting
       $timeformat(-9, 0, " ns", 0);


       // INDEX:        - Indicate version of AxiPC
       // =====
       $display("AXI_INFO: Running AxiPC version BP062-BU-01000-r0p0-00rel0 (SVA implementation)");


       // INDEX:        - Warn if any/some recommended rules are disabled
       // =====
       if (~RecommendOn)
         // All AXI_REC*_* rules disabled
         $display("AXI_WARN: All recommended AXI rules have been disabled by the RecommendOn parameter");
       else if (~RecMaxWaitOn)
         // Just AXI_REC*_MAX_WAIT rules disabled
         $display("AXI_WARN: Five recommended MAX_WAIT rules have been disabled by the RecMaxWaitOn parameter");


       // INDEX:        - Warn if any/some channel rules are ignored
       // =====
       if (AXI_ERRM_PropertyType > 0) $display("AXI_WARN: The AXI_ERRM_PropertyType parameter is currently not used by the SVA version");
       if (AXI_RECM_PropertyType > 0) $display("AXI_WARN: The AXI_RECM_PropertyType parameter is currently not used by the SVA version");
       if (AXI_AUXM_PropertyType > 0) $display("AXI_WARN: The AXI_AUXM_PropertyType parameter is currently not used by the SVA version");
       //
       if (AXI_ERRS_PropertyType > 0) $display("AXI_WARN: The AXI_ERRS_PropertyType parameter is currently not used by the SVA version");
       if (AXI_RECS_PropertyType > 0) $display("AXI_WARN: The AXI_RECS_PropertyType parameter is currently not used by the SVA version");
       if (AXI_AUXS_PropertyType > 0) $display("AXI_WARN: The AXI_AUXS_PropertyType parameter is currently not used by the SVA version");
       //
       if (AXI_ERRL_PropertyType > 0) $display("AXI_WARN: The AXI_ERRL_PropertyType parameter is currently not used by the SVA version");

    end


//------------------------------------------------------------------------------
// INDEX:
// INDEX: AXI Rules: Write Address Channel (*_AW*)
//------------------------------------------------------------------------------


//------------------------------------------------------------------------------
// INDEX:   1) Functional Rules
//------------------------------------------------------------------------------


  // INDEX:        - AXI_ERRM_AWADDR_BOUNDARY
  // =====
  // 4kbyte boundary: only bottom twelve bits (11 to 0) can change
  //
  // Only need to check INCR bursts since:
  //
  //   a) FIXED bursts cannot violate the 4kB boundary by definition
  //
  //   b) WRAP bursts always stay within a <4kB region because of the wrap
  //      address boundary.  The biggest WRAP burst possible has length 16,
  //      size 128 bytes (1024 bits), so it can transfer 2048 bytes. The
  //      individual transfer addresses wrap at a 2048 byte address boundary,
  //      and the max data transferred in also 2048 bytes, so a 4kB boundary
  //      can never be broken.
  property AXI_ERRM_AWADDR_BOUNDARY;
    @(posedge `AXI_SVA_CLK)
          !($isunknown({AWVALID,AWBURST,AWADDR})) &
          AWVALID & (AWBURST == `AXI_ABURST_INCR)
      |-> (AwAddrIncr[31:12] == AWADDR[31:12]);
  endproperty
  axi_errm_awaddr_boundary: assert property (AXI_ERRM_AWADDR_BOUNDARY) else
   $error("AXI_ERRM_AWADDR_BOUNDARY. A write burst cannot cross a 4kbyte boundary. Spec: section 4.1 on page 4-2.");


  // INDEX:        - AXI_ERRM_AWADDR_WRAP_ALIGN
  // =====
  property AXI_ERRM_AWADRR_WRAP_ALIGN;
    @(posedge `AXI_SVA_CLK)
          !($isunknown({AWVALID,AWBURST,AWADDR})) &
          AWVALID & (AWBURST == `AXI_ABURST_WRAP)
      |-> ((AWADDR[6:0] & AlignMaskW) == AWADDR[6:0]);
  endproperty
  axi_errm_awadrr_wrap_align: assert property (AXI_ERRM_AWADRR_WRAP_ALIGN) else
   $error("AXI_ERRM_AWADDR_WRAP_ALIGN. A write transaction with burst type WRAP must have an aligned address. Spec: section 4.4.3 on page 4-6.");


  // INDEX:        - AXI_ERRM_AWBURST
  // =====
  property AXI_ERRM_AWBURST;
    @(posedge `AXI_SVA_CLK)
          !($isunknown({AWVALID,AWBURST})) &
          AWVALID
      |-> (AWBURST != 2'b11);
  endproperty
  axi_errm_awburst: assert property (AXI_ERRM_AWBURST) else
   $error("AXI_ERRM_AWBURST. When AWVALID is high, a value of 2'b11 on AWBURST is not permitted. Spec: table 4-3 on page 4-5.");


  // INDEX:        - AXI_ERRM_AWCACHE
  // =====
  property AXI_ERRM_AWCACHE;
    @(posedge `AXI_SVA_CLK)
          !($isunknown({AWVALID,AWCACHE})) &
          AWVALID & ~AWCACHE[1]
      |-> (AWCACHE[3:2] == 2'b00);
  endproperty
  axi_errm_awcache: assert property (AXI_ERRM_AWCACHE) else
   $error("AXI_ERRM_AWCACHE. When AWVALID is high, if AWCACHE[1] is low then AWCACHE[3] and AWCACHE[2] must also be low. Spec: table 5-1 on page 5-3.");


  // INDEX:        - AXI_ERRM_AWLEN_WRAP
  // =====
  property AXI_ERRM_AWLEN_WRAP;
    @(posedge `AXI_SVA_CLK)
          !($isunknown({AWVALID,AWBURST,AWLEN})) &
          AWVALID & (AWBURST == `AXI_ABURST_WRAP)
      |-> (AWLEN == `AXI_ALEN_2 ||
           AWLEN == `AXI_ALEN_4 ||
           AWLEN == `AXI_ALEN_8 ||
           AWLEN == `AXI_ALEN_16);
  endproperty
  axi_errm_awlen_wrap: assert property (AXI_ERRM_AWLEN_WRAP) else
   $error("AXI_ERRM_AWLEN_WRAP. A write transaction with burst type WRAP must have length 2, 4, 8 or 16. Spec: section 4.4.3 on page 4-6.");


  // INDEX:        - AXI_ERRM_AWLOCK
  // =====
  property AXI_ERRM_AWLOCK;
    @(posedge `AXI_SVA_CLK)
          !($isunknown({AWVALID,AWLOCK})) &
          AWVALID
      |-> (AWLOCK != 2'b11);
  endproperty
  axi_errm_awlock: assert property (AXI_ERRM_AWLOCK) else
   $error("AXI_ERRM_AWLOCK. When AWVALID is high, a value of 2'b11 on AWLOCK is not permitted. Spec: table 6-1 on page 6-2.");


  // INDEX:        - AXI_ERRM_AWLOCK_END
  // =====
  property AXI_ERRM_AWLOCK_END;
    @(posedge `AXI_SVA_CLK)
          !($isunknown({AWVALID,ARVALID,ARLOCK,AWLOCK})) &
          ((LockState == `AXI_AUX_ST_LOCK_LAST) &   // waiting for unlocking transfer to complete
           AWVALID                                  // new valid write address
          )
      |-> ((nROutstanding & nWOutstanding) &        // main check: no other burst outstanding (final RLAST seen or BRESP transferred)
           ~(ARVALID & (ARLOCK[1] != AWLOCK[1]))    // extra check: no new address valid, unless of same LOCK type (simultaneous ARVALID transfer)
          );
  endproperty
  axi_errm_awlock_end: assert property (AXI_ERRM_AWLOCK_END) else
   $error("AXI_ERRM_AWLOCK_END. A master must wait for an unlocked transaction at the end of a locked sequence to complete before issuing another write address. Spec: section 6.3 on page 6-7.");


  // INDEX:        - AXI_ERRM_AWLOCK_ID
  // =====
  property AXI_ERRM_AWLOCK_ID;
    @(posedge `AXI_SVA_CLK)
          !($isunknown({AWVALID,AWID})) &
          ((LockState == `AXI_AUX_ST_LOCKED) & // in locked sequence
           AWVALID                             // valid write address
          )
      |-> (AWID == LockId);
  endproperty
  axi_errm_awlock_id: assert property (AXI_ERRM_AWLOCK_ID) else
   $error("AXI_ERRM_AWLOCK_ID. A sequence of locked transactions must use a single ID. Spec: section 6.3 on page 6-7.");


  // INDEX:        - AXI_ERRM_AWLOCK_LAST
  // =====
  property AXI_ERRM_AWLOCK_LAST;
    @(posedge `AXI_SVA_CLK)
          !($isunknown({AWVALID,ARVALID,AWLOCK})) &
          ((LockState == `AXI_AUX_ST_LOCKED) &        // in locked sequence
           (AWVALID & (AWLOCK != `AXI_ALOCK_LOCKED))  // valid unlocked write address
          )
      |-> (nROutstanding & nWOutstanding & ~ARVALID); // no other burst outstanding
  endproperty
  axi_errm_awlock_last: assert property (AXI_ERRM_AWLOCK_LAST) else
   $error("AXI_ERRM_AWLOCK_LAST. A master must wait for all locked transactions to complete before issuing an unlocked write address. Spec: section 6.3 on page 6-7.");


  // INDEX:        - AXI_ERRM_AWLOCK_START
  // =====
  property AXI_ERRM_AWLOCK_START;
    @(posedge `AXI_SVA_CLK)
          !($isunknown({AWVALID,ARVALID,AWLOCK,ARLOCK})) &
          ((LockState == `AXI_AUX_ST_UNLOCKED) &      // in unlocked sequence
           (AWVALID & (AWLOCK == `AXI_ALOCK_LOCKED))  // valid locked write address
          )
      |-> ((nROutstanding & nWOutstanding) &          // no other burst outstanding
           ~(ARVALID & (ARLOCK != `AXI_ALOCK_LOCKED)) // no new address valid, unless also locked
          );
  endproperty
  axi_errm_awlock_start: assert property (AXI_ERRM_AWLOCK_START) else
   $error("AXI_ERRM_AWLOCK_START. A master must wait for all outstanding transactions to complete before issuing a write address which is the first in a locked sequence. Spec: section 6.3 on page 6-7.");


  // INDEX:        - AXI_ERRM_AWSIZE
  // =====
  // Deliberately keeping AwSizeInBits logic outside of assertion, to
  // simplify formal-proofs flow.
  property AXI_ERRM_AWSIZE;
    @(posedge `AXI_SVA_CLK)
          !($isunknown({AWVALID,AWSIZE})) &
          AWVALID
      |-> (AwSizeInBits <= DATA_WIDTH);
  endproperty
  axi_errm_awsize: assert property (AXI_ERRM_AWSIZE) else
   $error("AXI_ERRM_AWSIZE. The size of a write transfer must not exceed the width of the data port. Spec: section 4.3 on page 4-4.");


  // INDEX:        - AXI_ERRM_AWVALID_RESET
  // =====
  property AXI_ERRM_AWVALID_RESET;
    @(posedge `AXI_SVA_CLK)
          !(`AXI_SVA_RSTn) & !($isunknown(`AXI_SVA_RSTn))
      ##1   `AXI_SVA_RSTn
      |-> !AWVALID;
  endproperty
  axi_errm_awvalid_reset: assert property (AXI_ERRM_AWVALID_RESET) else
   $error("AXI_ERRM_AWVALID_RESET. AWVALID must be low in the cycle when ARESETn first goes high. Spec: section 11.1.2 on page 11-2.");


  // INDEX:        - AXI_RECM_AWLOCK_BOUNDARY
  // =====
  // 4kbyte boundary: only bottom twelve bits (11 to 0) can change
  property   AXI_RECM_AWLOCK_BOUNDARY;
    @(posedge `AXI_SVA_CLK)
          !($isunknown({AWVALID,AWADDR})) &
          (RecommendOn                       & // Parameter that can disable all AXI_REC*_* rules
           (LockState == `AXI_AUX_ST_LOCKED) & // locked sequence
           AWVALID                             // valid write address
          )
      |-> ((AWADDR[31:12] == LockAddr[31:12]));
  endproperty
  axi_recm_awlock_boundary: assert property (AXI_RECM_AWLOCK_BOUNDARY) else
   $warning("AXI_RECM_AWLOCK_BOUNDARY. It is recommended that all locked transaction sequences are kept within the same 4KB address region. Spec: section 6.3 on page 6-7.");


  // INDEX:        - AXI_RECM_AWLOCK_CTRL 
  // =====
  property   AXI_RECM_AWLOCK_CTRL;
    @(posedge `AXI_SVA_CLK)
          !($isunknown({AWVALID,AWPROT,AWCACHE})) &
          (RecommendOn                       & // Parameter that can disable all AXI_REC*_* rules
           (LockState == `AXI_AUX_ST_LOCKED) & // locked sequence
           AWVALID                             // valid write address
          )
      |-> ((AWPROT == LockProt) & (AWCACHE == LockCache));
  endproperty
  axi_recm_awlock_ctrl: assert property (AXI_RECM_AWLOCK_CTRL) else
   $warning("AXI_RECM_AWLOCK_CTRL. It is recommended that a master should not change AxPROT or AxCACHE during a sequence of locked accesses. Spec: section 6.3 on page 6-7.");


  // INDEX:        - AXI_RECM_AWLOCK_NUM
  // =====
  property   AXI_RECM_AWLOCK_NUM;
    @(posedge `AXI_SVA_CLK)
           !($isunknown({AWVALID,AWLOCK})) &
          (RecommendOn                       & // Parameter that can disable all AXI_REC*_* rules
           (LockState == `AXI_AUX_ST_LOCKED) & // locked sequence
           AWVALID                             // write address
          )
      |-> (AWLOCK != `AXI_ALOCK_LOCKED);   // not starting another locked write transaction
  endproperty
  axi_recm_awlock_num: assert property (AXI_RECM_AWLOCK_NUM) else
   $warning("AXI_RECM_AWLOCK_NUM. It is recommended that locked transaction sequences are limited to two transactions. Spec: section 6.3 on page 6-7.");


//------------------------------------------------------------------------------
// INDEX:   2) Handshake Rules
//------------------------------------------------------------------------------


  // INDEX:        - AXI_ERRM_AWADDR_STABLE
  // =====
  property AXI_ERRM_AWADDR_STABLE;
    @(posedge `AXI_SVA_CLK)
          !($isunknown({AWVALID,AWREADY,AWADDR})) &
          `AXI_SVA_RSTn & AWVALID & !AWREADY
      ##1 `AXI_SVA_RSTn
      |-> $stable(AWADDR);
  endproperty
  axi_errm_awaddr_stable: assert property (AXI_ERRM_AWADDR_STABLE) else
   $error("AXI_ERRM_AWADDR_STABLE. AWADDR must remain stable when AWVALID is asserted and AWREADY low. Spec: section 3.1, and figure 3-1, on page 3-2.");


  // INDEX:        - AXI_ERRM_AWBURST_STABLE
  // =====
  property AXI_ERRM_AWBURST_STABLE;
    @(posedge `AXI_SVA_CLK)
          !($isunknown({AWVALID,AWREADY,AWBURST})) &
          `AXI_SVA_RSTn & AWVALID & !AWREADY
      ##1 `AXI_SVA_RSTn
      |-> $stable(AWBURST);
  endproperty
  axi_errm_awburst_stable: assert property (AXI_ERRM_AWBURST_STABLE) else
   $error("AXI_ERRM_AWBURST_STABLE. AWBURST must remain stable when AWVALID is asserted and AWREADY low. Spec: section 3.1, and figure 3-1, on page 3-2.");


  // INDEX:        - AXI_ERRM_AWCACHE_STABLE
  // =====
  property AXI_ERRM_AWCACHE_STABLE;
    @(posedge `AXI_SVA_CLK)
          !($isunknown({AWVALID,AWREADY,AWCACHE})) &
          `AXI_SVA_RSTn & AWVALID & !AWREADY
      ##1 `AXI_SVA_RSTn
      |-> $stable(AWCACHE);
  endproperty
  axi_errm_awcache_stable: assert property (AXI_ERRM_AWCACHE_STABLE) else
   $error("AXI_ERRM_AWCACHE_STABLE. AWCACHE must remain stable when AWVALID is asserted and AWREADY low. Spec: section 3.1, and figure 3-1, on page 3-2.");


  // INDEX:        - AXI_ERRM_AWID_STABLE
  // =====
  property AXI_ERRM_AWID_STABLE;
    @(posedge `AXI_SVA_CLK)
          !($isunknown({AWVALID,AWREADY,AWID})) &
          `AXI_SVA_RSTn & AWVALID & !AWREADY
      ##1 `AXI_SVA_RSTn
      |-> $stable(AWID);
  endproperty
  axi_errm_awid_stable: assert property (AXI_ERRM_AWID_STABLE) else
   $error("AXI_ERRM_AWID_STABLE. AWID must remain stable when AWVALID is asserted and AWREADY low. Spec: section 3.1, and figure 3-1, on page 3-2.");


  // INDEX:        - AXI_ERRM_AWLEN_STABLE