axipc.sv

amba3 sva 完全验证的代码

  // =====
  property AXI_ERRM_AWLEN_STABLE;
    @(posedge `AXI_SVA_CLK)
          !($isunknown({AWVALID,AWREADY,AWLEN})) &
          `AXI_SVA_RSTn & AWVALID & !AWREADY
      ##1 `AXI_SVA_RSTn
      |-> $stable(AWLEN);
  endproperty
  axi_errm_awlen_stable: assert property (AXI_ERRM_AWLEN_STABLE) else
   $error("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.");


  // INDEX:        - AXI_ERRM_AWLOCK_STABLE
  // =====
  property AXI_ERRM_AWLOCK_STABLE;
    @(posedge `AXI_SVA_CLK)
          !($isunknown({AWVALID,AWREADY,AWLOCK})) &
          `AXI_SVA_RSTn & AWVALID & !AWREADY
      ##1 `AXI_SVA_RSTn
      |-> $stable(AWLOCK);
  endproperty
  axi_errm_awlock_stable: assert property (AXI_ERRM_AWLOCK_STABLE) else
   $error("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.");


  // INDEX:        - AXI_ERRM_AWPROT_STABLE
  // =====
  property AXI_ERRM_AWPROT_STABLE;
    @(posedge `AXI_SVA_CLK)
          !($isunknown({AWVALID,AWREADY,AWPROT})) &
          `AXI_SVA_RSTn & AWVALID & !AWREADY
      ##1 `AXI_SVA_RSTn
      |-> $stable(AWPROT);
  endproperty
  axi_errm_awprot_stable: assert property (AXI_ERRM_AWPROT_STABLE) else
   $error("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.");


  // INDEX:        - AXI_ERRM_AWSIZE_STABLE
  // =====
  property AXI_ERRM_AWSIZE_STABLE;
    @(posedge `AXI_SVA_CLK)
          !($isunknown({AWVALID,AWREADY,AWSIZE})) &
          `AXI_SVA_RSTn & AWVALID & !AWREADY
      ##1 `AXI_SVA_RSTn
      |-> $stable(AWSIZE);
  endproperty
  axi_errm_awsize_stable: assert property (AXI_ERRM_AWSIZE_STABLE) else
   $error("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.");


  // INDEX:        - AXI_ERRM_AWVALID_STABLE
  // =====
  property AXI_ERRM_AWVALID_STABLE;
    @(posedge `AXI_SVA_CLK)
          `AXI_SVA_RSTn & AWVALID & !AWREADY & !($isunknown({AWVALID,AWREADY}))
      ##1 `AXI_SVA_RSTn
      |-> AWVALID;
  endproperty
  axi_errm_awvalid_stable: assert property (AXI_ERRM_AWVALID_STABLE) else
   $error("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.");


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


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


  // INDEX:        - AXI_ERRM_AWADDR_X
  // =====
  property AXI_ERRM_AWADDR_X;
    @(posedge `AXI_SVA_CLK)
        `AXI_SVA_RSTn & AWVALID
        |-> ! $isunknown(AWADDR);
  endproperty
  axi_errm_awaddr_x: assert property (AXI_ERRM_AWADDR_X) else
   $error("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.");


  // INDEX:        - AXI_ERRM_AWBURST_X
  // =====
  property AXI_ERRM_AWBURST_X;
    @(posedge `AXI_SVA_CLK)
        `AXI_SVA_RSTn & AWVALID
        |-> ! $isunknown(AWBURST);
  endproperty
  axi_errm_awburst_x: assert property (AXI_ERRM_AWBURST_X) else
   $error("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.");


  // INDEX:        - AXI_ERRM_AWCACHE_X
  // =====
  property AXI_ERRM_AWCACHE_X;
    @(posedge `AXI_SVA_CLK)
        `AXI_SVA_RSTn & AWVALID
        |-> ! $isunknown(AWCACHE);
  endproperty
  axi_errm_awcache_x: assert property (AXI_ERRM_AWCACHE_X) else
   $error("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.");


  // INDEX:        - AXI_ERRM_AWID_X
  // =====
  property AXI_ERRM_AWID_X;
    @(posedge `AXI_SVA_CLK)
        `AXI_SVA_RSTn & AWVALID
        |-> ! $isunknown(AWID);
  endproperty
  axi_errm_awid_x: assert property (AXI_ERRM_AWID_X) else
   $error("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.");


  // INDEX:        - AXI_ERRM_AWLEN_X
  // =====
  property AXI_ERRM_AWLEN_X;
    @(posedge `AXI_SVA_CLK)
        `AXI_SVA_RSTn & AWVALID
        |-> ! $isunknown(AWLEN);
  endproperty
  axi_errm_awlen_x: assert property (AXI_ERRM_AWLEN_X) else
   $error("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.");


  // INDEX:        - AXI_ERRM_AWLOCK_X
  // =====
  property AXI_ERRM_AWLOCK_X;
    @(posedge `AXI_SVA_CLK)
        `AXI_SVA_RSTn & AWVALID
        |-> ! $isunknown(AWLOCK);
  endproperty
  axi_errm_awlock_x: assert property (AXI_ERRM_AWLOCK_X) else
   $error("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.");


  // INDEX:        - AXI_ERRM_AWPROT_X
  // =====
  property AXI_ERRM_AWPROT_X;
    @(posedge `AXI_SVA_CLK)
        `AXI_SVA_RSTn & AWVALID
        |-> ! $isunknown(AWPROT);
  endproperty
  axi_errm_awprot_x: assert property (AXI_ERRM_AWPROT_X) else
   $error("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.");


  // INDEX:        - AXI_ERRM_AWSIZE_X
  // =====
  property AXI_ERRM_AWSIZE_X;
    @(posedge `AXI_SVA_CLK)
        `AXI_SVA_RSTn & AWVALID
        |-> ! $isunknown(AWSIZE);
  endproperty
  axi_errm_awsize_x: assert property (AXI_ERRM_AWSIZE_X) else
   $error("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.");


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


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

`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
  property AXI_ERRM_WDATA_NUM;
    @(posedge `AXI_SVA_CLK)
      `AXI_SVA_RSTn & !($isunknown(WDataNumError))
      |-> ~WDataNumError;
  endproperty
  axi_errm_wdata_num: assert property (AXI_ERRM_WDATA_NUM) else
   $error("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.");


  // INDEX:        - AXI_ERRM_WDATA_ORDER
  // =====
  property AXI_ERRM_WDATA_ORDER;
    @(posedge `AXI_SVA_CLK)
      `AXI_SVA_RSTn & !($isunknown(WDataOrderError))
      |-> ~WDataOrderError;
  endproperty
  axi_errm_wdata_order: assert property (AXI_ERRM_WDATA_ORDER) else
   $error("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.");


  // INDEX:        - AXI_ERRM_WDEPTH
  // =====
  property AXI_ERRM_WDEPTH;
    @(posedge `AXI_SVA_CLK)
          !($isunknown({WVALID,WREADY,WidDepth})) &
          WVALID & WREADY
      |-> (WidDepth <= WDEPTH);
  endproperty
  axi_errm_wdepth: assert property (AXI_ERRM_WDEPTH) else
   $error("AXI_ERRM_WDEPTH. A master can interleave a maximum of WDEPTH write data bursts. Spec: section 8.5 on page 8-6.");


  // INDEX:        - AXI_ERRM_WSTRB
  // =====
  property AXI_ERRM_WSTRB;
    @(posedge `AXI_SVA_CLK)
      `AXI_SVA_RSTn & !($isunknown(StrbError))
      |-> ~StrbError;
  endproperty
  axi_errm_wstrb: assert property (AXI_ERRM_WSTRB) else
   $error("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.");


  // INDEX:        - AXI_ERRM_WVALID_RESET
  // =====
  property AXI_ERRM_WVALID_RESET;
    @(posedge `AXI_SVA_CLK)
          !(`AXI_SVA_RSTn) & !($isunknown(`AXI_SVA_RSTn))
      ##1   `AXI_SVA_RSTn
      |-> !WVALID;
  endproperty
  axi_errm_wvalid_reset: assert property (AXI_ERRM_WVALID_RESET) else
   $error("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.");


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


  // INDEX:        - AXI_ERRM_WDATA_STABLE
  // =====
  property AXI_ERRM_WDATA_STABLE;
    @(posedge `AXI_SVA_CLK)
          !($isunknown({WVALID,WREADY,WDATA})) &
          `AXI_SVA_RSTn & WVALID & !WREADY
      ##1 `AXI_SVA_RSTn
      |-> $stable(WDATA);
  endproperty
  axi_errm_wdata_stable: assert property (AXI_ERRM_WDATA_STABLE) else
   $error("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.");


  // INDEX:        - AXI_ERRM_WID_STABLE
  // =====
  property AXI_ERRM_WID_STABLE;
    @(posedge `AXI_SVA_CLK)
          !($isunknown({WVALID,WREADY,WID})) &
          `AXI_SVA_RSTn & WVALID & !WREADY
      ##1 `AXI_SVA_RSTn
      |-> $stable(WID);
  endproperty
  axi_errm_wid_stable: assert property (AXI_ERRM_WID_STABLE) else
   $error("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.");


  // INDEX:        - AXI_ERRM_WLAST_STABLE
  // =====
  property AXI_ERRM_WLAST_STABLE;
    @(posedge `AXI_SVA_CLK)
          !($isunknown({WVALID,WREADY,WLAST})) &
          `AXI_SVA_RSTn & WVALID & !WREADY
      ##1 `AXI_SVA_RSTn
      |-> $stable(WLAST);
  endproperty
  axi_errm_wlast_stable: assert property (AXI_ERRM_WLAST_STABLE) else
   $error("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.");


  // INDEX:        - AXI_ERRM_WSTRB_STABLE
  // =====
  property AXI_ERRM_WSTRB_STABLE;
    @(posedge `AXI_SVA_CLK)
          !($isunknown({WVALID,WREADY,WSTRB})) &
          `AXI_SVA_RSTn & WVALID & !WREADY
      ##1 `AXI_SVA_RSTn
      |-> $stable(WSTRB);
  endproperty
  axi_errm_wstrb_stable: assert property (AXI_ERRM_WSTRB_STABLE) else
   $error("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.");


  // INDEX:        - AXI_ERRM_WVALID_STABLE
  // =====
  property AXI_ERRM_WVALID_STABLE;
    @(posedge `AXI_SVA_CLK)
          `AXI_SVA_RSTn & WVALID & !WREADY & !($isunknown({WVALID,WREADY}))
      ##1 `AXI_SVA_RSTn
      |-> WVALID;
  endproperty
  axi_errm_wvalid_stable: assert property (AXI_ERRM_WVALID_STABLE) else
   $error("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.");