mii_sva_checker.sv

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

                             "coverage of TX untagged frame lengths");

        // tagged frame occurred, data or type kind
        length_type TX_TaggedFrameLength = 0;
        length_cg mii_TX_tagged_frame_length = new (
                             TX_TaggedFrameLength, 
                             "mii_TX_tagged_frame_length", 
                             "coverage of TX tagged frame lengths");

`endif
`endif

      always @(posedge TX_CLK) begin

        // A COL occurred on a symbol

        // Asserted ASAP (symbol == 0) - after SDF
        mii_TX_1COV: cover property (
          mii_cov_COL_p (TX_EN, $past(TX_SdfValid)) )
        TX_SetFrameCover(MII_TX_COL_ON_SYMBOL_0);

        // Almost late (symbol = 63)
        mii_TX_2COV: cover property (
          mii_cov_COL_p (TX_EN, (TX_NibbleCnt == 63)) )
        TX_SetFrameCover(MII_TX_COL_ALMOST_LATE);

        // Earliest late (64)
        mii_TX_3COV: cover property (
          mii_cov_COL_p (TX_EN, (TX_NibbleCnt == 64)) )
        TX_SetFrameCover(MII_TX_COL_EARLIEST_LATE);

        // Late
        mii_TX_4COV: cover property (
          mii_cov_COL_p (TX_EN, (TX_NibbleCnt > 64)) )
        TX_SetFrameCover(MII_TX_COL_LATE);

        // Also if asserted -1 symbols before end
        mii_TX_5COV: cover property (
          mii_cov_COL_last_p (TX_EN) )
        TX_SetFrameCover(MII_TX_COL_LAST);

`ifndef SYNTHESIS
`ifdef IMPLEMENTED_CG

        mii_TX_6COV: cover property (
          frame_length_p (TX_EN, TX_NoTagLengthValid, 
                          TX_NibbleCnt,  TX_UntaggedFrameLength,
                          mii_TX_untagged_frame_length ) )
        begin
          TX_SetFrameCover(MII_TX_UNTAGGED_FRAME);
        end

        mii_TX_7COV: cover property (
          frame_length_p (TX_EN, TX_qTagValid, 
                          TX_NibbleCnt, TX_TaggedFrameLength,
                          mii_TX_tagged_frame_length ) )
        begin
          TX_SetFrameCover(MII_TX_TAGGED_FRAME);
        end

`endif
`endif

       // detect TX_ER asserted during a frame
        mii_TX_8COV: cover property ( 
               !TX_EN ##1 (TX_EN[*1:$]) ##0 TX_ER )
           TX_SetFrameCover(MII_TX_ER_DETECTED);

      // detect reset during a frame
        mii_TX_9COV: cover property ( 
               !TX_EN ##1 (TX_EN[*1:$]) ##0 resetting )
           TX_SetFrameCover(MII_TX_RESET_DETECTED);
      end
`endif // COVER_ON

// MAC TX assume, assert and cover
// ===============================

  // When collision occurs during transmission, the backoff
  // delay for next retransmission in within 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).

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

        mac_TX_19: assume property(mac_19_p(TX_EN));

        mac_TX_20: assume property(mac_TX_20_p);
      end
`endif
    end : mac_TX_assume_interframe
    else begin : mac_TX_assert_interframe
      always @(posedge TX_CLK) begin

        mac_TX_19: assert property(mac_19_p(TX_EN)) 
        else begin
          sva_checker_error
            ("TX Interframe gap is less than 96 bit times");
          TX_SetFrameError(MAC_TX_SHORT_INTERFR_GAP);
        end

/* not useful as assertion
        mii_TX_20: assert property(mac_TX_20_p) 
        else begin
          sva_checker_error
            ("Back_off delay is greater than max limit");
          TX_SetFrameError(MAC_TX_BIG_RETRANS_GAP);
        end
*/
      end
    end : mac_TX_assert_interframe
  endgenerate
`endif

// MAC TX Coverage
// ---------------

`ifdef COVER_ON

`ifndef SYNTHESIS
`ifdef IMPLEMENTED_CG

  // sample interframe gap length and also the back-off state
  // and their cross product
  // bins with TX_BackOffState == 0 indicate normal interframe gap
  // TX_BackOffState > 0 indicates the retransmission number
  // together with the back-off delay

    mac_TX_interframe_cg mac_TX_interframe = new ();

`endif
`endif

    always @(posedge TX_CLK) begin : tx_cover

        // The minimum interframe gap is 96 bit times, 
        // i.e., 24 clock ticks (with 4-bit data)

        mii_TX_8COV: cover property (mac_min_interframe_p(TX_EN))
          TX_SetFrameCover(MII_TX_MIN_INTERFRAME);
    end : tx_cover

`endif // COVER_ON


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

`ifdef ASSERT_ON

// Example 3-57 Selection of Assume or Assert in MII/MAC Checker
  generate

    if(mii_RX_assume) begin : mii_RX_assumptions

`ifdef IMPLEMENTED_ASSUME
      always @(posedge RX_CLK) begin
       // Basic checks: no x or z value on any signal outside of reset
`ifndef SVA_CHECKER_FORMAL
        mii_RX_1: assume property (
                mii_1_p(RX_DV, RXD, RX_ER) );
`endif

        mii_RX_2: assume property(mii_2_p); 

        mii_RX_7: assume property(mii_RX_7_p); 

        mii_RX_8: assume property(mii_8_p(RX_SdfValid, RX_EndOfFrame, RX_NibbleCnt)); 

        mii_RX_9: assume property(mii_9_p(RX_DV, 2)); 

// not suitable as a constraint since it applies it over past values
//        mii_RX_12: assume property(mii_12_p(RX_DV, RX_D_Word_r, RX_Fcs)); 

        mii_RX_13: assume property(mii_13_p(RX_NibbleCnt, RX_DV));


        mii_RX_14: assume property(mii_14_p(RX_Collision, RX_SdfValid, 
                                            RX_DV, RX_NibbleCnt, 
                                            2*minFrameSize)); 

        mii_RX_15: assume property(
                      mii_15_p(RX_DV, RX_qTagValid, RX_qTagLengthValid, 
                                RX_NibbleCnt, 2*maxFrameSize) ); 

        mii_RX_16: assume property(
                      mii_16_p(RX_DV, RX_NoTagLengthValid, 
                                RX_NibbleCnt, 2*maxUntaggedFrameSize) ); 

        mii_RX_17: assume property(
                      mii_17_p(RX_DV, RX_qTagValid, RX_DataLength, 
                                RX_FrameSize, RX_NibbleCnt) );

        mii_RX_18: assume property(
                      mii_18_p(RX_DV, RX_NoTagLengthValid, RX_DataLength, 
                                RX_FrameSize, RX_NibbleCnt) ); 

        mii_RX_20: assume property(mii_RX_20_p);  
      end
`endif

    end : mii_RX_assumptions
    else begin : mii_RX_assertions
      always @(posedge RX_CLK) begin

`ifndef SVA_CHECKER_FORMAL
        mii_RX_1: assert property (
                mii_1_p(RX_DV, RXD, RX_ER) )
        else begin
          RX_SetFrameError(MII_RX_BAD_OR_NO_SDF);
          sva_checker_error
            ("RX signals x or z");
        end
`endif

        mii_RX_2: assert property(mii_2_p) 
        else begin
          sva_checker_error
            ("RX_CLK sampled CRS not asserted during collision condition");
          RX_SetFrameError(MII_RX_CRS_NOT_W_COL);
        end

       mii_RX_7: assert property(mii_RX_7_p) 
        else begin
          sva_checker_error
            ("RX Bad or no SDF");
          RX_SetFrameError(MII_RX_BAD_OR_NO_SDF);
        end

        mii_RX_8: assert property(mii_8_p(RX_SdfValid, RX_EndOfFrame, RX_NibbleCnt)) 
        else begin
          sva_checker_error
            ("RX While RX_DV asserted there were 2N+1 nibbles");
          RX_SetFrameError(MII_RX_ODD_NIBBLES);
        end

        mii_RX_9: assert property(mii_9_p(RX_DV, 2)) 
        else begin
          sva_checker_error
            ("CRS not asserted 2 clock cycles after RX_DV");
          RX_SetFrameError(MII_RX_CRS_NOT_ASSERTED);
        end

        mii_RX_12: assert property(mii_12_p(RX_DV, RX_D_Word_r, RX_Fcs)) 
        else begin
          sva_checker_error
            ("RX Received FCS is incorrect");
          RX_SetFrameError(MII_RX_BAD_FCS);
        end

        mii_RX_13: assert property(mii_13_p(RX_NibbleCnt, RX_DV)) 
        else begin
          sva_checker_error
            ("RX Late collision occurred");
          RX_SetFrameError(MII_RX_LATE_COL);
        end

        mii_RX_14: assert property(mii_14_p(RX_Collision, RX_SdfValid, 
                                            RX_DV, RX_NibbleCnt, 
                                            2*minFrameSize) ) 
        else begin
          sva_checker_error
            ("RX Frame is less than minFrameSize octets");
          RX_SetFrameError(MII_RX_SHORT_FRAME);
        end

        mii_RX_15: assert property(
                      mii_15_p(RX_DV, RX_qTagValid, RX_TagLengthValid, 
                                RX_NibbleCnt, 2*maxFrameSize) ) 
        else begin
          sva_checker_error
            ("RX Normal with qTag Frame is more than maxFrameSize octets");
          RX_SetFrameError(MII_RX_TAGGED_FRAME_LONG);
        end

        mii_RX_16: assert property(
                      mii_16_p(RX_DV, RX_NoTagLengthValid, 
                                RX_NibbleCnt, 2*maxUntaggedFrameSize) ) 
        else begin
          sva_checker_error
            ("RX Normal w/o qTag Frame is more than maxUntaggedFrameSize octets");
          RX_SetFrameError(MII_RX_NORMAL_FRAME_LONG);
        end

        mii_RX_17: assert property(
                      mii_17_p(RX_DV, RX_qTagValid, RX_DataLength, 
                                RX_FrameSize, RX_NibbleCnt) ) 
        else begin
          sva_checker_error
            ("RX Frame with qTag not matching Length value");
          RX_SetFrameError(MII_RX_TAGGED_BAD_LENGTH);
        end

        mii_RX_18: assert property(
                      mii_18_p(RX_DV, RX_NoTagLengthValid, RX_DataLength, 
                                RX_FrameSize, RX_NibbleCnt) ) 
        else begin
          sva_checker_error
            ("RX Normal Frame not matching Length value");
          RX_SetFrameError(MII_RX_NORMAL_BAD_LENGTH);
        end

        mii_RX_20: assert property(mii_RX_20_p) 
        else begin
          sva_checker_error
            ("RX_DV == 0 and RX_ER == 1 with other than RXD == 1110");
          RX_SetFrameError(MII_RX_DV_ER_D_01_NOT1110);
        end

      end
    end : mii_RX_assertions
  endgenerate
`endif // ASSERT_ON

// MII RX Cover statements
// -----------------------

`ifdef COVER_ON

`ifndef SYNTHESIS
`ifdef IMPLEMENTED_CG

      // classification of frame length for each kind
      // untagged frame occurred, data or type kind
      length_type RX_UntaggedFrameLength = 0;
      length_cg mii_RX_untagged_frame_length = new (
                             RX_UntaggedFrameLength, 
                             "mii_RX_untagged_frame_length", 
                             "coverage of RX untagged frame lengths");
      // tagged frame occurred, data or type kind
      length_type RX_TaggedFrameLength = 0;
      length_cg mii_RX_tagged_frame_length = new (
                             RX_TaggedFrameLength, 
                             "mii_RX_tagged_frame_length", 
                             "coverage of RX tagged frame lengths");

`endif
`endif

      // RX Coverage statements, valid only 
      // when there is no failure of an assertion

      always @(posedge RX_CLK) begin

        // A COL occurred on a symbol
        // Asserted ASAP (symbol == 0) - after SDF
        mii_RX_1COV: cover property (
          mii_cov_COL_p (RX_DV, $past(RX_SdfValid)) )
        RX_SetFrameCover(MII_RX_COL_ON_SYMBOL_0);

        // Almost late (symbol = 63)
        mii_RX_2COV: cover property (
          mii_cov_COL_p (RX_DV, (RX_NibbleCnt == 63)) )
        RX_SetFrameCover(MII_RX_COL_ALMOST_LATE);

        // Earliest late (64)
        mii_RX_3COV: cover property (
          mii_cov_COL_p (RX_DV, (RX_NibbleCnt == 64)) )
        RX_SetFrameCover(MII_RX_COL_EARLIEST_LATE);

        // Late
        mii_RX_4COV: cover property (
          mii_cov_COL_p (RX_DV, (RX_NibbleCnt > 64)) )
        RX_SetFrameCover(MII_RX_COL_LATE);

        // Also if asserted -1 symbols before end
        mii_RX_5COV: cover property (
          mii_cov_COL_last_p (RX_DV) )
        RX_SetFrameCover(MII_RX_COL_LAST);

`ifdef IMPLEMENTED_CG

        mii_RX_6COV: cover property (
          frame_length_p (RX_DV, RX_NoTagLengthValid, 
                          RX_NibbleCnt, RX_UntaggedFrameLength,
                          mii_RX_untagged_frame_length) )
        begin
          RX_SetFrameCover(MII_RX_UNTAGGED_FRAME);
        end

        mii_RX_7COV: cover property (
          frame_length_p (RX_DV, RX_qTagValid, 
                          RX_NibbleCnt, RX_TaggedFrameLength,
                          mii_RX_tagged_frame_length) )
        begin
          RX_SetFrameCover(MII_RX_TAGGED_FRAME);
        end

`endif

       // detect RX_ER asserted during a frame
        mii_RX_8COV: cover property ( 
           not_resetting throughout
             ( !RX_DV ##1 (RX_DV[*1:$]) ##0 RX_ER ))
           RX_SetFrameCover(MII_RX_ER_DETECTED);

      // detect resetting during a frame
        mii_RX_9COV: cover property ( 
               !RX_DV ##1 (RX_DV[*1:$]) ##0 resetting )
           RX_SetFrameCover(MII_RX_RESET_DETECTED);

      // false carrier detected
        mii_RX_13COV: cover property (
           not_resetting && 
             (!RX_DV && RX_ER && (RXD == 4'b1110)) )
           RX_SetFrameCover(MII_RX_FALSE_CARRIER);           
     end

`endif // COVER_ON

// MAC RX assume, assert and cover
// ===============================

`ifdef ASSERT_ON
  generate
    if(mii_RX_assume) begin : mac_RX_assume_interframe

`ifdef IMPLEMENTED_ASSUME
      always @(posedge RX_CLK) begin
        mac_RX_19: assume property(mac_19_p(RX_DV));
      end
`endif

    end : mac_RX_assume_interframe
    else begin : mac_RX_assert_interframe
      always @(posedge RX_CLK) begin

        mac_RX_19: assert property(mac_19_p(RX_DV)) 
        else begin
          sva_checker_error
            ("RX Interframe gap is less than 96 bit times");
          RX_SetFrameError(MII_RX_SHORT_INTERFR_GAP);
        end

      end
    end : mac_RX_assert_interframe
  endgenerate

`endif // ASSERT_ON

`ifdef COVER_ON
  always @(posedge RX_CLK)
    mac_RX_2COV: cover property (mac_min_interframe_p(RX_DV));
`endif

endinterface : mii_sva_checker

`endif