axipc.v

amba3 sva 完全验证的代码

     `define AXI_OVL_RSTn ARESETn
  `endif
  // 
  // AUX: Auxiliary Logic
  `ifdef AXI_AUX_CLK
  `else
     `define AXI_AUX_CLK ACLK
  `endif
  //
  `ifdef AXI_AUX_RSTn
  `else
     `define AXI_AUX_RSTn ARESETn
  `endif


  // INDEX:        - OVL Version Specific Macros
  // =====
  `ifdef AXI_USE_OLD_OVL
     // Old OVL library from April 2003
     // ===============================
     // severity_level
     `define AXI_SimFatal   0
     `define AXI_SimError   1
     `define AXI_SimWarning 2
     //
     // assert_implication typo
     `define AXI_ANTECEDENT .antecendent_expr
     //
     // assert_quiescent_state switch for EOS
     `ifdef  ASSERT_END_OF_SIMULATION
        `define AXI_END_OF_SIMULATION `ASSERT_END_OF_SIMULATION
     `endif
  `else
     // Accellera V1.0 and later
     // ========================
     `include "std_ovl_defines.h"
     // severity_level
     `define AXI_SimFatal   `OVL_FATAL
     `define AXI_SimError   `OVL_ERROR
     `define AXI_SimWarning `OVL_WARNING
     //
     // assert_implication with correct spelling
     `define AXI_ANTECEDENT .antecedent_expr
     //
     // assert_quiescent_state switch for EOS
     `ifdef     OVL_END_OF_SIMULATION
        `define AXI_END_OF_SIMULATION `OVL_END_OF_SIMULATION
     `endif
     //
     // Disable for X-checking
     `ifdef     OVL_XCHECK_OFF
        `define AXI_XCHECK_OFF
     `endif
  `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");


       // 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 > 1) $display("AXI_WARN: All AXI_ERRM_* rules have been ignored by the AXI_ERRM_PropertyType parameter");
       if (AXI_RECM_PropertyType > 1) $display("AXI_WARN: All AXI_RECM_* rules have been ignored by the AXI_RECM_PropertyType parameter");
       if (AXI_AUXM_PropertyType > 1) $display("AXI_WARN: All AXI_AUXM_* rules have been ignored by the AXI_AUXM_PropertyType parameter");
       //
       if (AXI_ERRS_PropertyType > 1) $display("AXI_WARN: All AXI_ERRS_* rules have been ignored by the AXI_ERRS_PropertyType parameter");
       if (AXI_RECS_PropertyType > 1) $display("AXI_WARN: All AXI_RECS_* rules have been ignored by the AXI_RECS_PropertyType parameter");
       if (AXI_AUXS_PropertyType > 1) $display("AXI_WARN: All AXI_AUXS_* rules have been ignored by the AXI_AUXS_PropertyType parameter");
       //
       if (AXI_ERRL_PropertyType > 1) $display("AXI_WARN: All AXI_ERRL_* rules have been ignored by the AXI_ERRL_PropertyType parameter");

    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.
  assert_implication #(`AXI_SimError, AXI_ERRM_PropertyType,
    "AXI_ERRM_AWADDR_BOUNDARY. A write burst cannot cross a 4kbyte boundary. Spec: section 4.1 on page 4-2."
  )  axi_errm_awaddr_boundary
     (.clk              (`AXI_OVL_CLK),
      .reset_n          (`AXI_OVL_RSTn),
      `AXI_ANTECEDENT   (AWVALID & (AWBURST == `AXI_ABURST_INCR)),
      .consequent_expr  (AwAddrIncr[31:12] == AWADDR[31:12])
      );


  // INDEX:        - AXI_ERRM_AWADDR_WRAP_ALIGN
  // =====
  assert_implication #(`AXI_SimError, AXI_ERRM_PropertyType,
    "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."
  )  axi_errm_awaddr_wrap_align
     (.clk              (`AXI_OVL_CLK),
      .reset_n          (`AXI_OVL_RSTn),
      `AXI_ANTECEDENT   (AWVALID & (AWBURST == `AXI_ABURST_WRAP)),
      .consequent_expr  ((AWADDR[6:0] & AlignMaskW) == AWADDR[6:0])
      );


  // INDEX:        - AXI_ERRM_AWBURST
  // =====
  assert_implication #(`AXI_SimError, AXI_ERRM_PropertyType,
    "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."
  )  axi_errm_awburst
     (.clk              (`AXI_OVL_CLK),
      .reset_n          (`AXI_OVL_RSTn),
      `AXI_ANTECEDENT   (AWVALID),
      .consequent_expr  (AWBURST != 2'b11)
      );


  // INDEX:        - AXI_ERRM_AWCACHE
  // =====
  assert_implication #(`AXI_SimError, AXI_ERRM_PropertyType,
    "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."
  )  axi_errm_awcache
     (.clk              (`AXI_OVL_CLK),
      .reset_n          (`AXI_OVL_RSTn),
      `AXI_ANTECEDENT   (AWVALID & ~AWCACHE[1]),
      .consequent_expr  (AWCACHE[3:2] == 2'b00)
      );


  // INDEX:        - AXI_ERRM_AWLEN_WRAP
  // =====
  assert_implication #(`AXI_SimError, AXI_ERRM_PropertyType,
    "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."
  )  axi_errm_awlen_wrap
     (.clk              (`AXI_OVL_CLK),
      .reset_n          (`AXI_OVL_RSTn),
      `AXI_ANTECEDENT   (AWVALID & (AWBURST == `AXI_ABURST_WRAP)),
      .consequent_expr  (AWLEN == `AXI_ALEN_2 ||
                         AWLEN == `AXI_ALEN_4 ||
                         AWLEN == `AXI_ALEN_8 ||
                         AWLEN == `AXI_ALEN_16)
      );


  // INDEX:        - AXI_ERRM_AWLOCK
  // =====
  assert_implication #(`AXI_SimError, AXI_ERRM_PropertyType,
    "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."
  )  axi_errm_awlock
     (.clk              (`AXI_OVL_CLK),
      .reset_n          (`AXI_OVL_RSTn),
      `AXI_ANTECEDENT   (AWVALID),
      .consequent_expr  (AWLOCK != 2'b11)
      );


  // INDEX:        - AXI_ERRM_AWLOCK_END
  // =====
  assert_implication #(`AXI_SimError, AXI_ERRM_PropertyType,
    "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."
  )  axi_errm_awlock_end
     (.clk              (`AXI_OVL_CLK),
      .reset_n          (`AXI_OVL_RSTn),
      `AXI_ANTECEDENT   ((LockState == `AXI_AUX_ST_LOCK_LAST)    // waiting for unlocking transfer to complete
                         & AWVALID                               // new valid write address
                        ),
      .consequent_expr  (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)
                        )
      );


  // INDEX:        - AXI_ERRM_AWLOCK_ID
  // =====
  assert_implication #(`AXI_SimError, AXI_ERRM_PropertyType,
    "AXI_ERRM_AWLOCK_ID. A sequence of locked transactions must use a single ID. Spec: section 6.3 on page 6-7."
  )  axi_errm_awlock_id
     (.clk              (`AXI_OVL_CLK),
      .reset_n          (`AXI_OVL_RSTn),
      `AXI_ANTECEDENT   ((LockState == `AXI_AUX_ST_LOCKED) // in locked sequence
                          & AWVALID                        // valid write address
                        ),
      .consequent_expr  (AWID == LockId)
      );


  // INDEX:        - AXI_ERRM_AWLOCK_LAST
  // =====
  assert_implication #(`AXI_SimError, AXI_ERRM_PropertyType,
    "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."
  )  axi_errm_awlock_last
     (.clk              (`AXI_OVL_CLK),
      .reset_n          (`AXI_OVL_RSTn),
      `AXI_ANTECEDENT   ((LockState == `AXI_AUX_ST_LOCKED)           // in locked sequence
                         & (AWVALID & (AWLOCK != `AXI_ALOCK_LOCKED)) // valid unlocked write address
                        ),
      .consequent_expr  (nROutstanding & nWOutstanding & ~ARVALID)   // no other burst outstanding
      );


  // INDEX:        - AXI_ERRM_AWLOCK_START
  // =====
  assert_implication #(`AXI_SimError, AXI_ERRM_PropertyType,
    "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."
  )  axi_errm_awlock_start
     (.clk              (`AXI_OVL_CLK),
      .reset_n          (`AXI_OVL_RSTn),
      `AXI_ANTECEDENT   ((LockState == `AXI_AUX_ST_UNLOCKED)          // in unlocked sequence
                         & (AWVALID & (AWLOCK == `AXI_ALOCK_LOCKED))  // valid locked write address
                        ),
      .consequent_expr  (nROutstanding & nWOutstanding                // no other burst outstanding
                         & ~(ARVALID & (ARLOCK != `AXI_ALOCK_LOCKED)) // no new address valid, unless also locked
                        )
      );


  // INDEX:        - AXI_ERRM_AWSIZE
  // =====
  // Deliberately keeping AwSizeInBits logic outside of OVL instance, to
  // simplify formal-proofs flow.
  assert_implication #(`AXI_SimError, AXI_ERRM_PropertyType,
    "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."
  )  axi_errm_awsize
     (.clk              (`AXI_OVL_CLK),
      .reset_n          (`AXI_OVL_RSTn),
      `AXI_ANTECEDENT   (AWVALID),
      .consequent_expr  (AwSizeInBits <= DATA_WIDTH)
      );


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


  // INDEX:        - AXI_RECM_AWLOCK_BOUNDARY
  // =====
  // 4kbyte boundary: only bottom twelve bits (11 to 0) can change
  assert_implication #(`AXI_SimWarning, AXI_RECM_PropertyType,
    "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."
  )  axi_recm_awlock_boundary
     (.clk              (`AXI_OVL_CLK),
      .reset_n          (`AXI_OVL_RSTn),
      `AXI_ANTECEDENT   (RecommendOn                         // Parameter that can disable all AXI_REC*_* rules
                         & (LockState == `AXI_AUX_ST_LOCKED) // locked sequence
                         & AWVALID                           // valid write address
                        ),
      .consequent_expr  ((AWADDR[31:12] == LockAddr[31:12]))
      );


  // INDEX:        - AXI_RECM_AWLOCK_CTRL 
  // =====
  assert_implication #(`AXI_SimWarning, AXI_RECM_PropertyType,
    "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."
  )  axi_recm_awlock_ctrl
     (.clk              (`AXI_OVL_CLK),
      .reset_n          (`AXI_OVL_RSTn),
      `AXI_ANTECEDENT   (RecommendOn                         // Parameter that can disable all AXI_REC*_* rules
                         & (LockState == `AXI_AUX_ST_LOCKED) // locked sequence
                         & AWVALID                           // valid write address
                        ),
      .consequent_expr  ((AWPROT == LockProt) & (AWCACHE == LockCache))
      );


  // INDEX:        - AXI_RECM_AWLOCK_NUM
  // =====
  assert_implication #(`AXI_SimWarning, AXI_RECM_PropertyType,
    "AXI_RECM_AWLOCK_NUM. It is recommended that locked transaction sequences are limited to two transactions. Spec: section 6.3 on page 6-7."
  )  axi_recm_awlock_num
     (.clk              (`AXI_OVL_CLK),
      .reset_n          (`AXI_OVL_RSTn),
      `AXI_ANTECEDENT   (RecommendOn                         // Parameter that can disable all AXI_REC*_* rules
                         & (LockState == `AXI_AUX_ST_LOCKED) // locked sequence
                         & AWVALID                           // write address
                        ),
      .consequent_expr  (AWLOCK != `AXI_ALOCK_LOCKED)        // not starting another locked write transaction
      );


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


  // INDEX:        - AXI_ERRM_AWADDR_STABLE
  // =====
  assert_win_unchange #(`AXI_SimError, 32, AXI_ERRM_PropertyType,