axipc.v

amba3 sva 完全验证的代码

  // INDEX:        - AXI_ERRM_WID_STABLE
  // =====
  assert_win_unchange #(`AXI_SimError, ID_WIDTH, AXI_ERRM_PropertyType,
    "AXI_ERRM_WID_STABLE. WID must remain stable when WVALID is asserted and WREADY low. Spec: section 3.1, and figure 3-1, on page 3-2."
  )  axi_errm_wid_stable
     (.clk         (`AXI_OVL_CLK),
      .reset_n     (`AXI_OVL_RSTn),
      .start_event (WVALID & !WREADY),
      .test_expr   (WID),
      .end_event   (!(WVALID & !WREADY)) // Inverse of start_event
      );


  // INDEX:        - AXI_ERRM_WLAST_STABLE
  // =====
  assert_win_unchange #(`AXI_SimError, 1, AXI_ERRM_PropertyType,
    "AXI_ERRM_WLAST_STABLE. WLAST must remain stable when WVALID is asserted and WREADY low. Spec: section 3.1, and figure 3-1, on page 3-2."
  )  axi_errm_wlast_stable
     (.clk         (`AXI_OVL_CLK),
      .reset_n     (`AXI_OVL_RSTn),
      .start_event (WVALID & !WREADY),
      .test_expr   (WLAST),
      .end_event   (!(WVALID & !WREADY)) // Inverse of start_event
      );


  // INDEX:        - AXI_ERRM_WSTRB_STABLE
  // =====
  assert_win_unchange #(`AXI_SimError, STRB_WIDTH, AXI_ERRM_PropertyType,
    "AXI_ERRM_WSTRB_STABLE. WSTRB must remain stable when WVALID is asserted and WREADY low. Spec: section 3.1, and figure 3-1, on page 3-2."
  )  axi_errm_wstrb_stable
     (.clk         (`AXI_OVL_CLK),
      .reset_n     (`AXI_OVL_RSTn),
      .start_event (WVALID & !WREADY),
      .test_expr   (WSTRB),
      .end_event   (!(WVALID & !WREADY)) // Inverse of start_event
      );


  // INDEX:        - AXI_ERRM_WVALID_STABLE
  // =====
  assert_next #(`AXI_SimError, 1, 1, 0, AXI_ERRM_PropertyType,
    "AXI_ERRM_WVALID_STABLE. Once WVALID is asserted, it must remain asserted until WREADY is high. Spec: section 3.1.2 on page 3-4."
  )  axi_errm_wvalid_stable
     (.clk          (`AXI_OVL_CLK),
      .reset_n      (`AXI_OVL_RSTn),
      .start_event  (WVALID & !WREADY),
      .test_expr    (WVALID)
      );


  // INDEX:        - AXI_RECS_WREADY_MAX_WAIT 
  // =====
  // Note: this rule does not error if VALID goes low (breaking VALID_STABLE rule)
  assert_frame #(`AXI_SimWarning, 1, MAXWAITS, 0, AXI_RECS_PropertyType,
    "AXI_RECS_WREADY_MAX_WAIT. WREADY should be asserted within MAXWAITS cycles of WVALID being asserted."
  )  axi_recs_wready_max_wait
     (.clk         (`AXI_OVL_CLK),
      .reset_n     (`AXI_OVL_RSTn),
      .start_event (RecommendOn  &         // Parameter that can disable all  AXI_REC*_* rules
                    RecMaxWaitOn &         // Parameter that can disable just AXI_REC*_MAX_WAIT rules
                   !WREADY &  WVALID),
      .test_expr   (WREADY | !WVALID)      // READY=1 within MAXWAITS cycles (or VALID=0)
      );


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


  // INDEX:        - AXI_ERRM_WDATA_X
  // =====
  assert_never #(`AXI_SimError, AXI_ERRM_PropertyType,
    "AXI_ERRM_WDATA_X. When WVALID is high, a value of X on active byte lanes of WDATA is not permitted."
  )  axi_errm_wdata_x
     (.clk       (`AXI_OVL_CLK),
      .reset_n   (`AXI_OVL_RSTn),
      .test_expr (CheckXorZifValid(WVALID, (WDATA & WdataMask ))) // CheckXorZifValid returns 1'b0 or 1'bX
      );


  // INDEX:        - AXI_ERRM_WID_X
  // =====
  assert_never #(`AXI_SimError, AXI_ERRM_PropertyType,
    "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."
  )  axi_errm_wid_x
     (.clk       (`AXI_OVL_CLK),
      .reset_n   (`AXI_OVL_RSTn),
      .test_expr (CheckXorZifValid(WVALID,WID)) // CheckXorZifValid returns 1'b0 or 1'bX
      );


  // INDEX:        - AXI_ERRM_WLAST_X
  // =====
  assert_never #(`AXI_SimError, AXI_ERRM_PropertyType,
    "AXI_ERRM_WLAST_X. When WVALID is high, a value of X on WLAST is not permitted."
  )  axi_errm_wlast_x
     (.clk       (`AXI_OVL_CLK),
      .reset_n   (`AXI_OVL_RSTn),
      .test_expr (CheckXorZifValid(WVALID,WLAST)) // CheckXorZifValid returns 1'b0 or 1'bX
      );


  // INDEX:        - AXI_ERRM_WSTRB_X
  // =====
  assert_never #(`AXI_SimError, AXI_ERRM_PropertyType,
    "AXI_ERRM_WSTRB_X. When WVALID is high, a value of X on WSTRB is not permitted."
  )  axi_errm_wstrb_x
     (.clk       (`AXI_OVL_CLK),
      .reset_n   (`AXI_OVL_RSTn),
      .test_expr (CheckXorZifValid(WVALID,WSTRB)) // CheckXorZifValid returns 1'b0 or 1'bX
      );


  // INDEX:        - AXI_ERRM_WVALID_X
  // =====
  assert_never #(`AXI_SimError, AXI_ERRM_PropertyType,
    "AXI_ERRM_WVALID_X. When not in reset, a value of X on WVALID is not permitted."
  )  axi_errm_wvalid_x
     (.clk       (`AXI_OVL_CLK),
      .reset_n   (`AXI_OVL_RSTn),
      .test_expr (CheckXorZ(WVALID)) // CheckXorZ returns 1'b0 or 1'bX
      );


  // INDEX:        - AXI_ERRS_WREADY_X
  // =====
  assert_never #(`AXI_SimError, AXI_ERRS_PropertyType,
    "AXI_ERRS_WREADY_X. When not in reset, a value of X on WREADY is not permitted."
  )  axi_errs_wready_x
     (.clk       (`AXI_OVL_CLK),
      .reset_n   (`AXI_OVL_RSTn),
      .test_expr (CheckXorZ(WREADY)) // CheckXorZ returns 1'b0 or 1'bX
      );

`endif // AXI_XCHECK_OFF


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


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


  // INDEX:        - AXI_ERRS_BRESP
  // =====
  assert_always #(`AXI_SimError, AXI_ERRS_PropertyType,
    "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."
  )  axi_errs_bresp
     (.clk       (`AXI_OVL_CLK),
      .reset_n   (`AXI_OVL_RSTn),
      .test_expr (~BrespError)
      );


  // INDEX:        - AXI_ERRS_BRESP_ALL_DONE_EOS
  // =====
  // EOS: End-Of-Simulation check (not suitable for formal proofs).
  // Use +define+OVL_END_OF_SIMULATION=tb.EOS_signal when compiling.
`ifdef AXI_END_OF_SIMULATION
  assert_quiescent_state #(`AXI_SimError, 1, AXI_ERRS_PropertyType,
    "AXI_ERRS_BRESP_ALL_DONE_EOS. All write transaction addresses must have been matched with corresponding write response."
  )  axi_errs_bresp_all_done_eos
     (.clk          (`AXI_OVL_CLK),
      .reset_n      (`AXI_OVL_RSTn),
      .state_expr   (WIndex == 1),
      .check_value  (1'b1),
      .sample_event (1'b0)
      );
`endif


  // INDEX:        - AXI_ERRS_BRESP_EXOKAY
  // =====
  assert_always #(`AXI_SimError, AXI_ERRS_PropertyType,
    "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."
  )  axi_errs_bresp_exokay
     (.clk       (`AXI_OVL_CLK),
      .reset_n   (`AXI_OVL_RSTn),
      .test_expr (~BrespExokError)
      );


  // INDEX:        - AXI_ERRS_BVALID_RESET
  // =====
  assert_always_on_edge #(`AXI_SimError, 1, AXI_ERRS_PropertyType,
    "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."
  )  axi_errs_bvalid_reset
     (.clk            (`AXI_OVL_CLK),
      .reset_n        (1'b1), // check whilst in reset
      .sampling_event (`AXI_OVL_RSTn),
      .test_expr      (!BVALID)
      );


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


  // INDEX:        - AXI_ERRS_BID_STABLE
  // =====
  assert_win_unchange #(`AXI_SimError, ID_WIDTH, AXI_ERRS_PropertyType,
    "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."
  )  axi_errs_bid_stable
     (.clk          (`AXI_OVL_CLK),
      .reset_n      (`AXI_OVL_RSTn),
      .start_event  (BVALID & !BREADY),
      .test_expr    (BID),
      .end_event    (!(BVALID & !BREADY)) // Inverse of start_event
      );


  // INDEX:        - AXI_ERRS_BRESP_STABLE
  // =====
  assert_win_unchange #(`AXI_SimError, 2, AXI_ERRS_PropertyType,
    "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."
  )  axi_errs_bresp_stable
     (.clk          (`AXI_OVL_CLK),
      .reset_n      (`AXI_OVL_RSTn),
      .start_event  (BVALID & !BREADY),
      .test_expr    (BRESP),
      .end_event    (!(BVALID & !BREADY)) // Inverse of start_event
      );


  // INDEX:        - AXI_ERRS_BVALID_STABLE
  // =====
  assert_next #(`AXI_SimError, 1, 1, 0, AXI_ERRS_PropertyType,
    "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."
  )  axi_errs_bvalid_stable
     (.clk           (`AXI_OVL_CLK),
      .reset_n       (`AXI_OVL_RSTn),
      .start_event   (BVALID & !BREADY),
      .test_expr     (BVALID)
      );


  // INDEX:        - AXI_RECM_BREADY_MAX_WAIT 
  // =====
  // Note: this rule does not error if VALID goes low (breaking VALID_STABLE rule)
  assert_frame #(`AXI_SimWarning, 1, MAXWAITS, 0, AXI_RECM_PropertyType,
    "AXI_RECM_BREADY_MAX_WAIT. BREADY should be asserted within MAXWAITS cycles of BVALID being asserted."
  )  axi_recm_bready_max_wait
     (.clk         (`AXI_OVL_CLK),
      .reset_n     (`AXI_OVL_RSTn),
      .start_event (RecommendOn  &         // Parameter that can disable all  AXI_REC*_* rules
                    RecMaxWaitOn &         // Parameter that can disable just AXI_REC*_MAX_WAIT rules
                   !BREADY &  BVALID),
      .test_expr   (BREADY | !BVALID)      // READY=1 within MAXWAITS cycles (or VALID=0)
      );


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


  // INDEX:        - AXI_ERRM_BREADY_X
  // =====
  assert_never #(`AXI_SimError, AXI_ERRM_PropertyType,
    "AXI_ERRM_BREADY_X. When not in reset, a value of X on BREADY is not permitted."
  )  axi_errm_bready_x
     (.clk       (`AXI_OVL_CLK),
      .reset_n   (`AXI_OVL_RSTn),
      .test_expr (CheckXorZ(BREADY)) // CheckXorZ returns 1'b0 or 1'bX
      );


  // INDEX:        - AXI_ERRS_BID_X
  // =====
  assert_never #(`AXI_SimError, AXI_ERRS_PropertyType,
    "AXI_ERRS_BID_X. When BVALID is high, a value of X on BID is not permitted."
  )  axi_errs_bid_x
     (.clk       (`AXI_OVL_CLK),
      .reset_n   (`AXI_OVL_RSTn),
      .test_expr (CheckXorZifValid(BVALID,BID)) // CheckXorZifValid returns 1'b0 or 1'bX
      );


  // INDEX:        - AXI_ERRS_BRESP_X
  // =====
  assert_never #(`AXI_SimError, AXI_ERRS_PropertyType,
    "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."
  )  axi_errs_bresp_x
     (.clk       (`AXI_OVL_CLK),
      .reset_n   (`AXI_OVL_RSTn),
      .test_expr (CheckXorZifValid(BVALID,BRESP)) // CheckXorZifValid returns 1'b0 or 1'bX
      );


  // INDEX:        - AXI_ERRS_BVALID_X
  // =====
  assert_never #(`AXI_SimError, AXI_ERRS_PropertyType,
    "AXI_ERRS_BVALID_X. When not in reset, a value of X on BVALID is not permitted."
  )  axi_errs_bvalid_x
     (.clk       (`AXI_OVL_CLK),
      .reset_n   (`AXI_OVL_RSTn),
      .test_expr (CheckXorZ(BVALID)) // CheckXorZ returns 1'b0 or 1'bX
      );

`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