axipc.v

amba3 sva 完全验证的代码

    "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."
  )  axi_errm_awaddr_stable
     (.clk          (`AXI_OVL_CLK),
      .reset_n      (`AXI_OVL_RSTn),
      .start_event  (AWVALID & !AWREADY),
      .test_expr    (AWADDR),
      .end_event    (!(AWVALID & !AWREADY)) // Inverse of start_event
      );


  // INDEX:        - AXI_ERRM_AWBURST_STABLE
  // =====
  assert_win_unchange #(`AXI_SimError, 2, AXI_ERRM_PropertyType,
    "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."
  )  axi_errm_awburst_stable
     (.clk          (`AXI_OVL_CLK),
      .reset_n      (`AXI_OVL_RSTn),
      .start_event  (AWVALID & !AWREADY),
      .test_expr    (AWBURST),
      .end_event    (!(AWVALID & !AWREADY)) // Inverse of start_event
      );


  // INDEX:        - AXI_ERRM_AWCACHE_STABLE
  // =====
  assert_win_unchange #(`AXI_SimError, 4, AXI_ERRM_PropertyType,
    "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."
  )  axi_errm_awcache_stable
     (.clk          (`AXI_OVL_CLK),
      .reset_n      (`AXI_OVL_RSTn),
      .start_event  (AWVALID & !AWREADY),
      .test_expr    (AWCACHE),
      .end_event    (!(AWVALID & !AWREADY)) // Inverse of start_event
      );


  // INDEX:        - AXI_ERRM_AWID_STABLE
  // =====
  assert_win_unchange #(`AXI_SimError, ID_WIDTH, AXI_ERRM_PropertyType,
    "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."
  )  axi_errm_awid_stable
     (.clk          (`AXI_OVL_CLK),
      .reset_n      (`AXI_OVL_RSTn),
      .start_event  (AWVALID & !AWREADY),
      .test_expr    (AWID),
      .end_event    (!(AWVALID & !AWREADY)) // Inverse of start_event
      );


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


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


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


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


  // INDEX:        - AXI_ERRM_AWVALID_STABLE
  // =====
  assert_next #(`AXI_SimError, 1, 1, 0, AXI_ERRM_PropertyType,
    "AXI_ERRM_AWVALID_STABLE. Once AWVALID is asserted, it must remain asserted until AWREADY is high. Spec: section 3.1.1 on page 3-2."
  )  axi_errm_awvalid_stable
     (.clk         (`AXI_OVL_CLK),
      .reset_n     (`AXI_OVL_RSTn),
      .start_event (AWVALID & !AWREADY),
      .test_expr   (AWVALID)
      );


  // INDEX:        - AXI_RECS_AWREADY_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_AWREADY_MAX_WAIT. AWREADY should be asserted within MAXWAITS cycles of AWVALID being asserted."
  )  axi_recs_awready_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
                   !AWREADY &  AWVALID),
      .test_expr   (AWREADY | !AWVALID)    // 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_AWADDR_X
  // =====
  assert_never #(`AXI_SimError, AXI_ERRM_PropertyType,
    "AXI_ERRM_AWADDR_X. When AWVALID is high, a value of X on AWADDR is not permitted. Spec: section 3.1.1 on page 3-3."
  )  axi_errm_awaddr_x
     (.clk       (`AXI_OVL_CLK),
      .reset_n   (`AXI_OVL_RSTn),
      .test_expr (CheckXorZifValid(AWVALID,AWADDR)) // CheckXorZifValid returns 1'b0 or 1'bX
      );


  // INDEX:        - AXI_ERRM_AWBURST_X
  // =====
  assert_never #(`AXI_SimError, AXI_ERRM_PropertyType,
    "AXI_ERRM_AWBURST_X. When AWVALID is high, a value of X on AWBURST is not permitted. Spec: section 3.1.1 on page 3-3."
  )  axi_errm_awburst_x
     (.clk       (`AXI_OVL_CLK),
      .reset_n   (`AXI_OVL_RSTn),
      .test_expr (CheckXorZifValid(AWVALID,AWBURST)) // CheckXorZifValid returns 1'b0 or 1'bX
      );


  // INDEX:        - AXI_ERRM_AWCACHE_X
  // =====
  assert_never #(`AXI_SimError, AXI_ERRM_PropertyType,
    "AXI_ERRM_AWCACHE_X. When AWVALID is high, a value of X on AWCACHE is not permitted. Spec: section 3.1.1 on page 3-3."
  )  axi_errm_awcache_x
     (.clk       (`AXI_OVL_CLK),
      .reset_n   (`AXI_OVL_RSTn),
      .test_expr (CheckXorZifValid(AWVALID,AWCACHE)) // CheckXorZifValid returns 1'b0 or 1'bX
      );


  // INDEX:        - AXI_ERRM_AWID_X
  // =====
  assert_never #(`AXI_SimError, AXI_ERRM_PropertyType,
    "AXI_ERRM_AWID_X. When AWVALID is high, a value of X on AWID is not permitted. Spec: section 3.1.1 on page 3-3."
  )  axi_errm_awid_x
     (.clk       (`AXI_OVL_CLK),
      .reset_n   (`AXI_OVL_RSTn),
      .test_expr (CheckXorZifValid(AWVALID,AWID)) // CheckXorZifValid returns 1'b0 or 1'bX
      );


  // INDEX:        - AXI_ERRM_AWLEN_X
  // =====
  assert_never #(`AXI_SimError, AXI_ERRM_PropertyType,
    "AXI_ERRM_AWLEN_X. When AWVALID is high, a value of X on AWLEN is not permitted. Spec: section 3.1.1 on page 3-3."
  )  axi_errm_awlen_x
     (.clk       (`AXI_OVL_CLK),
      .reset_n   (`AXI_OVL_RSTn),
      .test_expr (CheckXorZifValid(AWVALID,AWLEN)) // CheckXorZifValid returns 1'b0 or 1'bX
      );


  // INDEX:        - AXI_ERRM_AWLOCK_X
  // =====
  assert_never #(`AXI_SimError, AXI_ERRM_PropertyType,
    "AXI_ERRM_AWLOCK_X. When AWVALID is high, a value of X on AWLOCK is not permitted. Spec: section 3.1.1 on page 3-3."
  )  axi_errm_awlock_x
     (.clk       (`AXI_OVL_CLK),
      .reset_n   (`AXI_OVL_RSTn),
      .test_expr (CheckXorZifValid(AWVALID,AWLOCK)) // CheckXorZifValid returns 1'b0 or 1'bX
      );


  // INDEX:        - AXI_ERRM_AWPROT_X
  // =====
  assert_never #(`AXI_SimError, AXI_ERRM_PropertyType,
    "AXI_ERRM_AWPROT_X. When AWVALID is high, a value of X on AWPROT is not permitted. Spec: section 3.1.1 on page 3-3."
  )  axi_errm_awprot_x
     (.clk       (`AXI_OVL_CLK),
      .reset_n   (`AXI_OVL_RSTn),
      .test_expr (CheckXorZifValid(AWVALID,AWPROT)) // CheckXorZifValid returns 1'b0 or 1'bX
      );


  // INDEX:        - AXI_ERRM_AWSIZE_X
  // =====
  assert_never #(`AXI_SimError, AXI_ERRM_PropertyType,
    "AXI_ERRM_AWSIZE_X. When AWVALID is high, a value of X on AWSIZE is not permitted. Spec: section 3.1.1 on page 3-3."
  )  axi_errm_awsize_x
     (.clk       (`AXI_OVL_CLK),
      .reset_n   (`AXI_OVL_RSTn),
      .test_expr (CheckXorZifValid(AWVALID,AWSIZE)) // CheckXorZifValid returns 1'b0 or 1'bX
      );


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


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

`endif // AXI_XCHECK_OFF


//------------------------------------------------------------------------------
// INDEX:
// INDEX: AXI Rules: Write Data Channel (*_W*)
//------------------------------------------------------------------------------


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


  // INDEX:        - AXI_ERRM_WDATA_NUM
  // =====
  // This will fire in one of the following situations:
  // 1) Write data arrives and WLAST set and WDATA count is not equal to AWLEN
  // 2) Write data arrives and WLAST not set and WDATA count is equal to AWLEN
  // 3) ADDR arrives, WLAST already received and WDATA count not equal to AWLEN
  assert_always #(`AXI_SimError, AXI_ERRM_PropertyType,
    "AXI_ERRM_WDATA_NUM. The number of write data items must match AWLEN for the corresponding address. Spec: table 4-1 on page 4-3."
  )  axi_errm_wdata_num
     (.clk        (`AXI_OVL_CLK),
      .reset_n    (`AXI_OVL_RSTn),
      .test_expr  (~WDataNumError)
      );


  // INDEX:        - AXI_ERRM_WDATA_ORDER
  // =====
  assert_always #(`AXI_SimError, AXI_ERRM_PropertyType,
    "AXI_ERRM_WDATA_ORDER. The order in which addresses and the first write data item are produced must match. Spec: section 8.5 on page 8-6."
  )  axi_errm_wdata_order
     (.clk       (`AXI_OVL_CLK),
      .reset_n   (`AXI_OVL_RSTn),
      .test_expr (~WDataOrderError)
      );


  // INDEX:        - AXI_ERRM_WDEPTH
  // =====
  assert_implication #(`AXI_SimError, AXI_ERRM_PropertyType,
    "AXI_ERRM_WDEPTH. A master can interleave a maximum of WDEPTH write data bursts. Spec: section 8.5 on page 8-6."
  )  axi_errm_wdepth
     (.clk              (`AXI_OVL_CLK),
      .reset_n          (`AXI_OVL_RSTn),
      `AXI_ANTECEDENT   (WVALID & WREADY),
      .consequent_expr  (WidDepth <= WDEPTH)
      );


  // INDEX:        - AXI_ERRM_WSTRB
  // =====
  assert_always #(`AXI_SimError, AXI_ERRM_PropertyType,
    "AXI_ERRM_WSTRB. Write strobes must only be asserted for the correct byte lanes as determined from start address, transfer size and beat number. Spec: section 9.2 on page 9-3."
  )  axi_errm_wstrb
     (.clk       (`AXI_OVL_CLK),
      .reset_n   (`AXI_OVL_RSTn),
      .test_expr (~StrbError)
      );


  // INDEX:        - AXI_ERRM_WVALID_RESET
  // =====
  assert_always_on_edge #(`AXI_SimError, 1, AXI_ERRM_PropertyType,
    "AXI_ERRM_WVALID_RESET. WVALID must be low in the cycle when ARESETn first goes high. Spec: section 11.1.2 on page 11-2."
  )  axi_errm_wvalid_reset
     (.clk            (`AXI_OVL_CLK),
      .reset_n        (1'b1), // check whilst in reset
      .sampling_event (`AXI_OVL_RSTn),
      .test_expr      (!WVALID)
      );


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


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