axipc.sv

amba3 sva 完全验证的代码

  // INDEX:        - AXI_RECS_WREADY_MAX_WAIT 
  // =====
  // Note: this rule does not error if VALID goes low (breaking VALID_STABLE rule)
  property   AXI_RECS_WREADY_MAX_WAIT;
    @(posedge `AXI_SVA_CLK)
      `AXI_SVA_RSTn & !($isunknown({WVALID,WREADY})) &
      RecommendOn                              & // Parameter that can disable all AXI_REC*_* rules
      RecMaxWaitOn                             & // Parameter that can disable just AXI_REC*_MAX_WAIT rules
                         ( WVALID & !WREADY) 
      |-> ##[1:MAXWAITS] (!WVALID |  WREADY);  // READY=1 within MAXWAITS cycles (or VALID=0)
  endproperty
  axi_recs_wready_max_wait: assert property (AXI_RECS_WREADY_MAX_WAIT) else
   $warning("AXI_RECS_WREADY_MAX_WAIT. WREADY should be asserted within MAXWAITS cycles of WVALID being asserted.");  


//------------------------------------------------------------------------------
// INDEX:   3) X-Propagation Rules
//------------------------------------------------------------------------------
`ifdef AXI_XCHECK_OFF
`else  // X-Checking on by default


  // INDEX:        - AXI_ERRM_WDATA_X
  // =====
  property AXI_ERRM_WDATA_X;
    @(posedge `AXI_SVA_CLK)
        `AXI_SVA_RSTn & WVALID & !($isunknown(WdataMask))
        |-> ! $isunknown(WDATA & WdataMask);
  endproperty
  axi_errm_wdata_x: assert property (AXI_ERRM_WDATA_X) else
   $error("AXI_ERRM_WDATA_X. When WVALID is high, a value of X on active byte lanes of WDATA is not permitted.");


  // INDEX:        - AXI_ERRM_WID_X
  // =====
  property AXI_ERRM_WID_X;
    @(posedge `AXI_SVA_CLK)
        `AXI_SVA_RSTn & WVALID
        |-> ! $isunknown(WID);
  endproperty
  axi_errm_wid_x: assert property (AXI_ERRM_WID_X) else
   $error("AXI_ERRM_WID_X. When WVALID is high, a value of X on WID is not permitted. Spec: section 3.1.2 on page 3-4.");


  // INDEX:        - AXI_ERRM_WLAST_X
  // =====
  property AXI_ERRM_WLAST_X;
    @(posedge `AXI_SVA_CLK)
        `AXI_SVA_RSTn & WVALID
        |-> ! $isunknown(WLAST);
  endproperty
  axi_errm_wlast_x: assert property (AXI_ERRM_WLAST_X) else
   $error("AXI_ERRM_WLAST_X. When WVALID is high, a value of X on WLAST is not permitted.");


  // INDEX:        - AXI_ERRM_WSTRB_X
  // =====
  property AXI_ERRM_WSTRB_X;
    @(posedge `AXI_SVA_CLK)
        `AXI_SVA_RSTn & WVALID
        |-> ! $isunknown(WSTRB);
  endproperty
  axi_errm_wstrb_x: assert property (AXI_ERRM_WSTRB_X) else
   $error("AXI_ERRM_WSTRB_X. When WVALID is high, a value of X on WSTRB is not permitted.");


  // INDEX:        - AXI_ERRM_WVALID_X
  // =====
  property AXI_ERRM_WVALID_X;
    @(posedge `AXI_SVA_CLK)
        `AXI_SVA_RSTn
        |-> ! $isunknown(WVALID);
  endproperty
  axi_errm_wvalid_x: assert property (AXI_ERRM_WVALID_X) else
   $error("AXI_ERRM_WVALID_X. When not in reset, a value of X on WVALID is not permitted.");


  // INDEX:        - AXI_ERRS_WREADY_X
  // =====
  property AXI_ERRS_WREADY_X;
    @(posedge `AXI_SVA_CLK)
        `AXI_SVA_RSTn
        |-> ! $isunknown(WREADY);
  endproperty
  axi_errs_wready_x: assert property (AXI_ERRS_WREADY_X) else
   $error("AXI_ERRS_WREADY_X. When not in reset, a value of X on WREADY is not permitted.");

`endif // AXI_XCHECK_OFF


//------------------------------------------------------------------------------
// INDEX:
// INDEX: AXI Rules: Write Response Channel (*_B*)
//------------------------------------------------------------------------------


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


  // INDEX:        - AXI_ERRS_BRESP
  // =====
  property AXI_ERRS_BRESP;
    @(posedge `AXI_SVA_CLK)
      `AXI_SVA_RSTn & !($isunknown(BrespError))
      |-> ~BrespError;
  endproperty
  axi_errs_bresp: assert property (AXI_ERRS_BRESP) else
   $error("AXI_ERRS_BRESP. A slave must only give a write response after the last write data item is transferred. Spec: section 3.3 on page 3-7, and figure 3-5 on page 3-8.");


  // INDEX:        - AXI_ERRS_BRESP_ALL_DONE_EOS
  // =====
  // EOS: End-Of-Simulation check (not suitable for formal proofs).
  // Use +define+AXI_END_OF_SIMULATION=tb.EOS_signal when compiling.
`ifdef AXI_END_OF_SIMULATION
  property AXI_ERRS_BRESP_ALL_DONE_EOS;
    @(posedge `AXI_SVA_CLK)
          !($isunknown(`AXI_END_OF_SIMULATION)) &
          `AXI_SVA_RSTn
      ##1 `AXI_SVA_RSTn & $rose(`AXI_END_OF_SIMULATION)
      |-> (WIndex == 1);
  endproperty
  axi_errs_bresp_all_done_eos: assert property (AXI_ERRS_BRESP_ALL_DONE_EOS) else
   $error("AXI_ERRS_BRESP_ALL_DONE_EOS. All write transaction addresses must have been matched with corresponding write response.");
`endif


  // INDEX:        - AXI_ERRS_BRESP_EXOKAY
  // =====
  property AXI_ERRS_BRESP_EXOKAY;
    @(posedge `AXI_SVA_CLK)
      `AXI_SVA_RSTn & !($isunknown(BrespExokError))
      |-> ~BrespExokError;
  endproperty
  axi_errs_bresp_exokay: assert property (AXI_ERRS_BRESP_EXOKAY) else
   $error("AXI_ERRS_BRESP_EXOKAY. An EXOKAY write response can only be given to an exclusive write access. Spec: section 6.2.3 on page 6-4.");


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


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


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


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


  // INDEX:        - AXI_ERRS_BVALID_STABLE
  // =====
  property AXI_ERRS_BVALID_STABLE;
    @(posedge `AXI_SVA_CLK)
          `AXI_SVA_RSTn & BVALID & !BREADY & !($isunknown({BVALID,BREADY}))
      ##1 `AXI_SVA_RSTn
      |-> BVALID;
  endproperty
  axi_errs_bvalid_stable: assert property (AXI_ERRS_BVALID_STABLE) else
   $error("AXI_ERRS_BVALID_STABLE. Once BVALID is asserted, it must remain asserted until BREADY is high. Spec: section 3.1.3 on page 3-4.");


  // INDEX:        - AXI_RECM_BREADY_MAX_WAIT 
  // =====
  // Note: this rule does not error if VALID goes low (breaking VALID_STABLE rule)
  property   AXI_RECM_BREADY_MAX_WAIT;
    @(posedge `AXI_SVA_CLK)
      `AXI_SVA_RSTn & !($isunknown({BVALID,BREADY})) &
      RecommendOn                              & // Parameter that can disable all AXI_REC*_* rules
      RecMaxWaitOn                             & // Parameter that can disable just AXI_REC*_MAX_WAIT rules
                         ( BVALID & !BREADY) 
      |-> ##[1:MAXWAITS] (!BVALID |  BREADY);  // READY=1 within MAXWAITS cycles (or VALID=0)
  endproperty
  axi_recm_bready_max_wait: assert property (AXI_RECM_BREADY_MAX_WAIT) else
   $warning("AXI_RECM_BREADY_MAX_WAIT. BREADY should be asserted within MAXWAITS cycles of BVALID being asserted.");


//------------------------------------------------------------------------------
// INDEX:   3) X-Propagation Rules
//------------------------------------------------------------------------------
`ifdef AXI_XCHECK_OFF
`else  // X-Checking on by default


  // INDEX:        - AXI_ERRM_BREADY_X
  // =====
  property AXI_ERRM_BREADY_X;
    @(posedge `AXI_SVA_CLK)
        `AXI_SVA_RSTn
        |-> ! $isunknown(BREADY);
  endproperty
  axi_errm_bready_x: assert property (AXI_ERRM_BREADY_X) else
   $error("AXI_ERRM_BREADY_X. When not in reset, a value of X on BREADY is not permitted.");


  // INDEX:        - AXI_ERRS_BID_X
  // =====
  property AXI_ERRS_BID_X;
    @(posedge `AXI_SVA_CLK)
        `AXI_SVA_RSTn & BVALID
        |-> ! $isunknown(BID);
  endproperty
  axi_errs_bid_x: assert property (AXI_ERRS_BID_X) else
   $error("AXI_ERRS_BID_X. When BVALID is high, a value of X on BID is not permitted.");


  // INDEX:        - AXI_ERRS_BRESP_X
  // =====
  property AXI_ERRS_BRESP_X;
    @(posedge `AXI_SVA_CLK)
        `AXI_SVA_RSTn & BVALID
        |-> ! $isunknown(BRESP);
  endproperty
  axi_errs_bresp_x: assert property (AXI_ERRS_BRESP_X) else
   $error("AXI_ERRS_BRESP_X. When BVALID is high, a value of X on BRESP is not permitted.  Spec: section 3.1.3 on page 3-4.");


  // INDEX:        - AXI_ERRS_BVALID_X
  // =====
  property AXI_ERRS_BVALID_X;
    @(posedge `AXI_SVA_CLK)
        `AXI_SVA_RSTn
        |-> ! $isunknown(BVALID);
  endproperty
  axi_errs_bvalid_x: assert property (AXI_ERRS_BVALID_X) else
   $error("AXI_ERRS_BVALID_X. When not in reset, a value of X on BVALID is not permitted.");

`endif // AXI_XCHECK_OFF


//------------------------------------------------------------------------------
// INDEX:
// INDEX: AXI Rules: Read Address Channel (*_AR*)
//------------------------------------------------------------------------------


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


  // INDEX:        - AXI_ERRM_ARADDR_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_ARADDR_BOUNDARY;
    @(posedge `AXI_SVA_CLK)
          !($isunknown({ARVALID,ARBURST,ARADDR})) &
          ARVALID & (ARBURST == `AXI_ABURST_INCR)
      |-> (ArAddrIncr[31:12] == ARADDR[31:12]);
  endproperty
  axi_errm_araddr_boundary: assert property (AXI_ERRM_ARADDR_BOUNDARY) else
   $error("AXI_ERRM_ARADDR_BOUNDARY. A read burst cannot cross a 4kbyte boundary. Spec: section 4.1 on page 4-2.");


  // INDEX:        - AXI_ERRM_ARADDR_WRAP_ALIGN
  // =====
  property AXI_ERRM_ARADDR_WRAP_ALIGN;
    @(posedge `AXI_SVA_CLK)
          !($isunknown({ARVALID,ARBURST,ARADDR})) &
          ARVALID & (ARBURST == `AXI_ABURST_WRAP)
      |-> ((ARADDR[6:0] & AlignMaskR) == ARADDR[6:0]);
  endproperty
  axi_errm_araddr_wrap_align: assert property (AXI_ERRM_ARADDR_WRAP_ALIGN) else
   $error("AXI_ERRM_ARADDR_WRAP_ALIGN. A read transaction with burst type WRAP must have an aligned address. Spec: section 4.4.3 on page 4-6.");


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


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


  // INDEX:        - AXI_ERRM_ARLEN_WRAP
  // =====
  property AXI_ERRM_AR