mii_sva_checker.sv

VMM 文档加源码, synopsys公司很好的验证资料

  // When there is no collision and no TX_ER, transmitted FCS (the
  // last 4 octets of frame) must be correct.
  // property is likely not suitable for Magellan because the 
  // choice made regarding the frame length may collide with requiring 
  // !miiEN to happen and fcs be correct. 
  // The alternative is to make it depend on the length value of  
  // the frame rather than on miiEN... TBD
  property mii_12_p(miiEN, D_Word_r, Fcs_r);
    disable iff(resetting || TX_Collision  && !mii_FullDuplex)
      miiEN ##1 !miiEN |-> 
          (D_Word_r == complement_reverse(Fcs_r));
  endproperty : mii_12_p

  // Late collision happened - after 1 slot time 
  // (minFrameSize = 64 octets = 128 nibbles have been transmitted)
  // (including preamble and sdf??)
  property mii_13_p(NibbleCnt, miiEN);
    disable iff(resetting  || mii_FullDuplex)
      (NibbleCnt > minFrameSize*2) && miiEN |-> !$rose(COL);
  endproperty : mii_13_p

  // Frame is at least minFrameSize = 64 octets (not including Preamble and SDF?)
  // That is, after 128 nibbles after preamble and sdf TX_EN or RX_DV
  //  is still asserted on the next clock tick
  property mii_14_p(Collision, SdfValid, miiEN, NibbleCnt, value);
    disable iff(resetting || Collision && !mii_FullDuplex)
      SdfValid && miiEN ##1 (!miiEN)[->1] |-> (NibbleCnt > value);
  endproperty : mii_14_p

  // Frame is at most maxUntaggedFrameSize = 1518 octets w/o tag (b) 
  // and maxFrameSize = 1522 (a) with tag
  // present  (not including Preamble and SDF)
  property mii_15_p(miiEN, qTagValid, qTagLengthValid, NibbleCnt, value);
    disable iff(resetting || COL && !mii_FullDuplex)
      qTagValid ##8 qTagLengthValid
         |-> 
      (miiEN && (NibbleCnt <= value))[*1:$] ##1 !miiEN;
  endproperty : mii_15_p

  property mii_16_p(miiEN, NoTagLengthValid, NibbleCnt, value);
    disable iff(resetting || COL && !mii_FullDuplex)
      NoTagLengthValid 
         |-> 
      (miiEN && (NibbleCnt <= value))[*1:$] ##1 !miiEN;
  endproperty : mii_16_p

  // LengthType field is aligned with TX_EN or RX_DV
  // if to be interpreted as length (a) when tag 
  // (b) when no tag present. This check is done only when the length is
  // greater than 64 without tag and 60 with the tag.
  // Otherwise the pad bytes complete to that length, 
  // checked by mii_14_p.

  property mii_17_p(miiEN, qTagValid, DataLength, 
                     FrameSize, NibbleCnt);
    disable iff(resetting || COL && !mii_FullDuplex)
      (qTagValid ##8 (DataLength > minFrameSize-4) ##1 (!miiEN[->1]))
        |-> 
      (({1'b0,NibbleCnt[15:1]} - 16'd17) == FrameSize);
  endproperty : mii_17_p

  property mii_18_p(miiEN, NoTagLengthValid, DataLength, 
                     FrameSize, NibbleCnt);
    disable iff(resetting || COL && !mii_FullDuplex)
      (NoTagLengthValid && (DataLength > minFrameSize)) ##1 (!miiEN[->1])
        |-> 
      (({1'b0,NibbleCnt[15:1]} - 16'd14) == FrameSize);
  endproperty : mii_18_p

  // While RX_DV is deasserted then false carrier can be
  // indicated by RX_ER asserted and RXD == 1110.  
  property mii_RX_20_p;
    disable iff (resetting) 
      !RX_DV && RX_ER |-> RXD == 4'b1110;
  endproperty : mii_RX_20_p

  // RX_DV must be enabled no later than Start Frame Delimiter
  // (SFD). 
  // This means that 0 or more (up to 7) preamble octets could
  // also appear, followed by SFD.
  property mii_RX_7_p;
    disable iff (resetting || COL && !mii_FullDuplex) 
      !RX_DV ##1 RX_DV |->
          ##[2:16] (RX_Word[15:8] == {SdfH, SdfL});
  endproperty : mii_RX_7_p


// Shared MAC TX and RX property definition
//-----------------------------------------

  // The minimum interframe gap is 96 bit times, 
  // i.e., 24 clock ticks (with 4-bit data)
  property mac_19_p(miiEN);
    disable iff(resetting)
      miiEN ##1 !miiEN |-> !miiEN[*24];
  endproperty : mac_19_p

// MAC TX property definition
//---------------------------

  // When collision occurs during transmission, the backoff average
  // delay for next retransmission is at least that of the exponentially
  // increasing interval up to 10 retransmissions and then the upper
  // bound levels off at 1023 slot times. One slot time is 512 bits ==
  // 128 nibbles (clock ticks). This cannot be checked using assertions.
  // Used in assumptions, it constrains the retransmission to be 
  // within the exponentially increasing interval.

  property mac_TX_20_p;
    disable iff (resetting)
      !TX_EN ##1 (TX_Collision && TX_EN && (TX_BackOffState > 0))
        |->
      (TX_BackOffDelay <= (32'd128 * 
                            ((TX_BackOffState <= 5'd9) ?
                              ((32'd1 << TX_BackOffState) - 32'd1) :
                              32'd1023
                            )
                          )
      ) ;
  endproperty : mac_TX_20_p

`ifdef COVER_ON
// Coverage properties shared by TX and RX
// ---------------------------------------

//COL occurred within a frame : cover property
//  Cross coverage with symbol offset 0, 1, latest early, earliest late,
//  end of frame
//  Asserted ASAP (symbol == 0) - after SDF...?
//  Almost late (symbol = 63)
//  Earliest late (64)
//  Late
//  Also if asserted -1 symbols before end (and -n ??)

  // A COL occurred on a symbol
  // miiEN is TX_EN or RX_DV, 
  // cnt identifies position in frame based on nibble count
  // used everywhere except for last nibble
  property mii_cov_COL_p (miiEN, cnt);
    (not_resetting && miiEN && !mii_FullDuplex) throughout 
            ($rose(miiEN) ##0 (COL && cnt)[->1]);
  endproperty : mii_cov_COL_p 

  property mii_cov_COL_last_p (miiEN);
    ((not_resetting && miiEN && !mii_FullDuplex) throughout 
            ($rose(miiEN) ##0 COL[->1]))
      ##1 !miiEN ;
  endproperty : mii_cov_COL_last_p
 
  // exact min / max length packet detected, w/ and w/o tag 
  property frame_exact_length_p (miiEN, kind, cnt, frame_length);
    (not_resetting && (!COL || mii_FullDuplex)) throughout 
       (
        kind within ( $rose(miiEN) ##1 (miiEN)[*1:$] )
       )
     ##1 (!miiEN && (cnt == frame_length));
  endproperty : frame_exact_length_p

  // classification of frame length for each kind
  // untagged frame occurred, data or type kind, and
  // tagged frame occurred, data or type kind
  // covers successfully completed frames only (no COL)
  // miiEN is TX_EN or RX_DV
  // kind identifies the position of the desired frame kind

`ifndef SYNTHESIS
`ifdef IMPLEMENTED_CG

  covergroup length_cg(ref length_type cnt, 
                       input string cov_name, explanation);
    coverpoint cnt 
      {
        bins fr_length[] = {[1:1536]};
        bins fr_large = default; 
      }
    option.at_least = 1;
    option.per_instance = 1;
    option.name = cov_name;
    option.comment = explanation;
//    option.auto_bin_max = 100;
  endgroup : length_cg

  task automatic store_cnt(input length_type cnt, ref length_type v, 
                 ref length_cg cg_inst);
    v = cnt; cg_inst.sample;
  endtask : store_cnt

  property frame_length_p (miiEN, kind, cnt, frame_length, cg_inst);
    (not_resetting && (!COL || mii_FullDuplex)) throughout 
       (
        kind within ( $rose(miiEN) ##1 (miiEN)[*1:$] )
       )
     ##1 (!miiEN,  store_cnt(cnt, frame_length, cg_inst)) ;
  endproperty : frame_length_p

// cover group for interframe and back-off delay

  covergroup mac_TX_interframe_cg @(posedge TX_CLK);
    coverpoint TX_BackOffDelay iff (rose_TX_EN)
      { bins interframe_small[] = {[1:1024]};
        bins interframe_large = default;
      }
    coverpoint TX_BackOffState iff (rose_TX_EN); // 0 means no retry
//    cross TX_BackOffDelay, TX_BackOffState iff (rose_TX_EN);
    option.at_least = 1;
    option.per_instance = 1;
    option.name = "TX_Interframe gap";
    option.comment = "BackOffState==0 means no collision, normal interframe gap";
//    option.auto_bin_max = 100;
  endgroup : mac_TX_interframe_cg

`endif
`endif

  // min interframe gap
  property mac_min_interframe_p(miiEN);
    not_resetting throughout
      (miiEN ##1 !miiEN[*24] ##1 miiEN) ;
  endproperty :mac_min_interframe_p

`endif

// - Control frames : NOT SUPPORTED 
//  - Cover various pause interval - NOT SUPPORTED
//    - Interval was lengthened
//    - Interval was reset


// MII TX Assume, Assert and Cover
// =================================

`ifdef ASSERT_ON
  generate
    if(mii_TX_assume) begin : mii_TX_assumptions
`ifdef IMPLEMENTED_ASSUME
      always @(posedge TX_CLK) begin

       // Basic checks: no x or z value on any signal outside of reset
`ifndef SVA_CHECKER_FORMAL
        mii_TX_1: assume property (
                mii_1_p(TX_EN, TXD, TX_ER) );
`endif // SVA_CHECKER_FORMAL

        mii_TX_2: assume property(mii_2_p); 

        mii_TX_3: assume property(mii_TX_3_p); 

        mii_TX_4: assume property(mii_TX_4_p); 

        mii_TX_5: assume property(mii_TX_5_p); 

        mii_TX_6: assume property(mii_TX_6_p); 

        mii_TX_7: assume property(mii_TX_7_p); 

        mii_TX_8: assume property(mii_8_p(TX_SdfValid, TX_EndOfFrame, TX_NibbleCnt)); 

        mii_TX_9: assume property(mii_9_p(TX_EN, 2)); 

        mii_TX_10: assume property(mii_TX_10_p); 

        mii_TX_11: assume property(mii_TX_11_p); 

// not suitable as constraint, since it imposes it over past values
//        mii_TX_12: assume property(mii_12_p(TX_EN, TX_D_Word_r, TX_Fcs)); 

        mii_TX_13: assume property(mii_13_p(TX_NibbleCnt, TX_EN)); 

        mii_TX_14: assume property(mii_14_p(TX_Collision, TX_SdfValid, 
                                            TX_EN, TX_NibbleCnt, 
                                             (2*minFrameSize)) ); 

        mii_TX_15: assume property(
                      mii_11a_p(TX_EN, TX_qTagValid, TX_qTagLengthValid, 
                                TX_NibbleCnt, ( 2*maxFrameSize)) ); 

        mii_TX_16: assume property(
                      mii_16_p(TX_EN, TX_NoTagLengthValid, 
                                TX_NibbleCnt, (2*maxUntaggedFrameSize)) ); 

        mii_TX_17: assume property(
                      mii_17_p(TX_EN, TX_qTagValid, TX_DataLength, 
                                TX_FrameSize, TX_NibbleCnt) ); 

        mii_TX_18: assume property(
                      mii_18_p(TX_EN, TX_NoTagLengthValid, TX_DataLength, 
                                TX_FrameSize, TX_NibbleCnt) ); 
      end
`endif

    end : mii_TX_assumptions
    else begin : mii_TX_assertions
      always @(posedge TX_CLK) begin

`ifndef SVA_CHECKER_FORMAL
        mii_TX_1: assert property (
                mii_1_p(TX_EN, TXD, TX_ER) )
        else begin
          sva_checker_error ("TX signals x or z");
          TX_SetFrameError(MII_TX_x_z);
        end
`endif // SVA_CHECKER_FORMAL

        mii_TX_2: assert property(mii_2_p) 
        else begin
          sva_checker_error
            ("TC_CLK sampled CRS not asserted during collision condition");
          TX_SetFrameError(MII_TX_NO_CRS_W_COL);
        end

        mii_TX_3: assert property(mii_TX_3_p) 
        else begin
          sva_checker_error
            ("mii_TX_EN asserted when CRS is asserted");
          TX_SetFrameError(MII_TX_EN_ASSERT_WHEN_CRS);
        end

        mii_TX_4: assert property(mii_TX_4_p) 
        else begin
          sva_checker_error
            ("TX_EN == 0 and TX_ER == 1 is a reserved state");
          TX_SetFrameError(MII_TX_EN_ER_01);
        end

        mii_TX_5: assert property(mii_TX_5_p) 
        else begin
          sva_checker_error
            ("Bad Preamble octet");
          TX_SetFrameError(MII_TX_BAD_PREAMBLE);
        end

        mii_TX_6: assert property(mii_TX_6_p) 
        else begin
          sva_checker_error
            ("Bad low-order SDF nibble");
          TX_SetFrameError(MII_TX_BAD_LOW_SDF);
        end

        mii_TX_7: assert property(mii_TX_7_p) 
        else begin
          sva_checker_error
            ("Bad high-order SDF nibble");
          TX_SetFrameError(MII_TX_BAD_HIGH_SDF);
        end

        mii_TX_8: assert property(mii_8_p(TX_SdfValid, TX_EndOfFrame, TX_NibbleCnt)) 
        else begin
          sva_checker_error
            ("While TX_EN asserted there were 2N+1 nibbles");
          TX_SetFrameError(MII_TX_ODD_NIBBLES);
        end

        mii_TX_9: assert property(mii_9_p(TX_EN, 2)) 
        else begin
          sva_checker_error
            ("CRS not asserted 2 clock cycles after TX_EN");
          TX_SetFrameError(MII_TX_CRS_NOT_ASSERTED);
        end

        mii_TX_10: assert property(mii_TX_10_p) 
        else begin
          sva_checker_error
            ("TX When COL set then no 32 bit == 8 nibble jam sequence");
          TX_SetFrameError(MII_TX_NOT_A_JAM);
        end

        mii_TX_11: assert property(mii_TX_11_p) 
        else begin
          sva_checker_error
            ("TX FCS when jamming is not invalid");
          TX_SetFrameError(MII_TX_FCS_VALID_W_JAM);
        end

        mii_TX_12: assert property(mii_12_p(TX_EN, TX_D_Word_r, TX_Fcs)) 
        else begin
          sva_checker_error
            ("TX Transmitted FCS is incorrect");
          TX_SetFrameError(MII_TX_BAD_FCS);
        end

        mii_TX_13: assert property(mii_13_p(TX_NibbleCnt, TX_EN)) 
        else begin
          sva_checker_error
            ("TX Late collision occurred");
          TX_SetFrameError(MII_TX_LATE_COL);
        end

        mii_TX_14: assert property(mii_14_p(TX_Collision, TX_SdfValid,
                                            TX_EN, TX_NibbleCnt, 
                                            (2*minFrameSize)) ) 
        else begin
          sva_checker_error
            ("TX Frame is less than 64 octets");
          TX_SetFrameError(MII_TX_SHORT_FRAME);
        end

        mii_TX_15: assert property(
                      mii_15_p(TX_EN, TX_qTagValid, TX_TagLengthValid, 
                             TX_NibbleCnt, (2*maxFrameSize)) ) 
        else begin
          sva_checker_error
            ("TX Normal with qTag Frame is more than 1522 octets");
          TX_SetFrameError(MII_TX_TAGGED_FRAME_LONG);
        end

        mii_TX_16: assert property(
                      mii_16_p(TX_EN, TX_NoTagLengthValid, 
                             TX_NibbleCnt, (2*maxUntaggedFrameSize)) ) 
        else begin
          sva_checker_error
            ("TX Normal w/o qTag Frame is more than 1518 octets");
          TX_SetFrameError(MII_TX_NORMAL_FRAME_LONG);
        end

        mii_TX_17: assert property(
                      mii_17_p(TX_EN, TX_qTagValid, TX_DataLength, 
                                TX_FrameSize, TX_NibbleCnt) ) 
        else begin
          sva_checker_error
            ("TX Frame with qTag not matching Length value");
          TX_SetFrameError(MII_TX_TAGGED_BAD_LENGTH);
        end

        mii_TX_18: assert property(
                      mii_18_p(TX_EN, TX_NoTagLengthValid, TX_DataLength, 
                                TX_FrameSize, TX_NibbleCnt) ) 
        else begin
          sva_checker_error
            ("TX Normal Frame not matching Length value");
          TX_SetFrameError(MII_TX_NORMAL_BAD_LENGTH);
        end

      end
    end : mii_TX_assertions
  endgenerate

`endif // ASSERT_ON

// MII TX Covers
// -------------

`ifdef COVER_ON
        // TX Coverage statements, valid only 
        // when there is no failure of an assertion
        // -------------------
`ifndef SYNTHESIS
`ifdef IMPLEMENTED_CG

// Example 3-37 Coverage of Packet Length Using a covergroup and a sequence
        // classification of frame length for each kind
        // untagged frame occurred, data or type kind

      length_type TX_UntaggedFrameLength = 0;
      length_cg mii_TX_untagged_frame_length = new (
                             TX_UntaggedFrameLength, 
                             "mii_TX_untagged_frame_length",