mii_sva_checker.sv

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

// 
// -------------------------------------------------------------
//    Copyright 2004-2008 Synopsys, Inc.
//    All Rights Reserved Worldwide
// 
//    Licensed under the Apache License, Version 2.0 (the
//    "License"); you may not use this file except in
//    compliance with the License.  You may obtain a copy of
//    the License at
// 
//        http://www.apache.org/licenses/LICENSE-2.0
// 
//    Unless required by applicable law or agreed to in
//    writing, software distributed under the License is
//    distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR
//    CONDITIONS OF ANY KIND, either express or implied.  See
//    the License for the specific language governing
//    permissions and limitations under the License.
// -------------------------------------------------------------
// 

//
// SystemVerilog Assertion Checker for MII protocol
// Based on IEE Std 802.3-2002.
//

/*

If an assertion that invalidates a frame fires, it sets TX_FrameError
(resp. RX_FrameError), bits which can be accessed by the testbench.

Cover properties reports through flags TX_FrameCover
(resp. RX_FrameCover).

TX_ER and RX_ER are detected by a cover property as a coverage item.

*/

`ifndef MII_SVA_CHECKER__SV
`define MII_SVA_CHECKER__SV

(* sva_checker *)
interface mii_sva_checker (
        reset_n, TX_CLK, TX_EN, TX_ER, TXD, 
                 COL, CRS, 
                 RX_CLK, RX_DV, RX_ER, RXD,
                 mii_FullDuplex,
                 TX_FrameError, RX_FrameError,
                 TX_FrameCover, RX_FrameCover);


  parameter int severity_level              = 0;
  parameter int minFrameSize                = 64;   // in octets, see 4.4
                // Size in octets = 2 x addressSize + lengthOrTypeSize +
                // tag} + dataSize + crcSize, see 4.2.2.2, (1)
  parameter int maxFrameSize                = 1522; 
  parameter int maxUntaggedFrameSize        = 1518; // in octets, see 4.4
                // min value of Length/Type for Type interpretation
  parameter int minTypeValue                = 1536;
  parameter int mii_TX_max_attempts         = 10;
  parameter bit mii_TX_assume               = 1'b0;
  parameter bit mii_RX_assume               = 1'b0;
  parameter         msg                     = "VIOLATION";
  parameter int category                    = 0;
  parameter int coverage_level_1            = -1;
  parameter int coverage_level_2            = -1;
  parameter int coverage_level_3            = -1;

  input logic reset_n, TX_CLK, TX_EN, TX_ER;
  input logic [3:0] TXD;
  input logic COL, CRS;
  input logic RX_CLK, RX_DV, RX_ER;
  input logic [3:0] RXD;
  input bit         mii_FullDuplex;

// Example 3-11 Disabling a Monitor from an Assertion
  output mii_sva_error_size_type  TX_FrameError;
  output mii_sva_error_size_type  RX_FrameError;
  output mii_sva_cover_size_type  TX_FrameCover;
  output mii_sva_cover_size_type  RX_FrameCover;

  // constants

  localparam
    int MII_D_size = 4, // TXD / RXD size
      addressSize = 6, // 6 octets = 48 bits in compliance with 3.2.3
      lengthOrTypeSize = 2, // 2 octets = 16 bits 
      maxClientDataSize = 1500, // in octets, max MAC client Data,
      crcSize = 4, // 4 octets = 32 bit CRC
      qTagPrefixSize = 4, // in octets, length of QTag Prefix, see 3.5
      maxValidFrame = maxUntaggedFrameSize - 
                      (2 * addressSize + lengthOrTypeSize + crcSize),
                     // in octets, the max length of the MAC client data field
      slotTime = 4096, // MII_D_size, // {# of clk for collision handling, 4.4}
      preambleSize = 7, // 7 octets = 56 bits, see 4.2.5
      sfdSize = 1, // 1 octet = 8 bit start frame delimiter
      headerSize = 8, // 8 octets = 64 bits, sum of preambleSize and sfdSize
      jamSize = 4; // jam sequence 4 octets = 32 bits
  localparam assert_name = "MII_MAC_SVA_CHECKER";

  // types
  typedef logic [3:0] nibble;
  typedef logic [7:0] octet;
  typedef bit [15:0] length_type;

  localparam octet qTagHigh = 8'h81, qTagLow = 8'h00;
  localparam nibble Preamble = 4'h5, SdfH = 4'hD, SdfL = 4'h5;


  // log reporting tasks and common items
`include "sva_std_task.h"

// CRC calculation - may not be used as constraint in Magellan
//   Rajesh Nair, Gerry Ryan, Farivar Farzaneh, "A Symbol Based
//   Algorithm for Hardware Implementation of Cyclic Rdundancy Check
//  (CRC)", Bay Networks, Inc., IEE conf. 1997.

// update CRC for one bit of data
  function logic [31:0] CRC32_1(logic data, logic [31:0] fcs);
    int j;
    CRC32_1[0] = fcs[31] ^ data;
    for (j=1; j<=31; j++) begin
      case (j)
        1,2,4,5,7,8,10,11,12,16,22,23,26 : 
           CRC32_1[j] = fcs[j-1]^fcs[31]^data;
        default : CRC32_1[j] = fcs[j-1];
      endcase
    end
  endfunction : CRC32_1

// update CRC for a nibble worth of data
  function logic [31:0] CRC32(nibble data, logic [31:0] fcs);
    logic [31:0] fcs_tmp [0:2] = '{3{32'b0}};
    int i = 0;
    fcs_tmp[0] = CRC32_1(data[0], fcs);
    for (i=1; i<=3; i++) 
      if (i==3) CRC32 = CRC32_1(data[i], fcs_tmp[2]);
      else      fcs_tmp[i] = CRC32_1(data[i], fcs_tmp[i-1]);
  endfunction : CRC32

// reverse and complement crc signature
  function logic [31:0] complement_reverse(logic [31:0] crc);
    int i = 0;
    for (i=0; i<32; i++) 
      complement_reverse[i] = !crc[31-i];
  endfunction :  complement_reverse

// TX variables and processes
// ==========================

  // nibble buffers
  logic [31:0] TX_D_Word_r = 0;
  wire [15:0] TX_Word = {TXD, TX_D_Word_r[31:20]};
  wire [15:0] TX_RevWord = {TX_Word[7:0], TX_Word[15:8]};
  wire [31:0] TX_D_Word = {TXD, TX_D_Word_r[31:4]};

  logic past_TX_EN = 1'b0; // past value of TX_EN
  wire rose_TX_EN = !past_TX_EN && TX_EN; 
  wire fell_TX_EN = past_TX_EN && !TX_EN; 

   // nibble counters, Frame byte counters bits [15:1]
  length_type TX_NibbleCnt = 0;

  // frame size for comparison when TX_EN deasserted
  logic [15:0] TX_FrameSize = 0;
                               
  logic [31:0] TX_Fcs = 32'hffffffff; // accumulate CRC

  // flags for rreporting an error detected by an assertion to TB
  // output port
  // the bits are set in the action block and reset at the end of a frame. 
  // interframe errors are reported from the end of the preceding 
  // frame

  task TX_SetFrameError(input mii_sva_tx_error_type i);
    TX_FrameError = i | TX_FrameError;
  endtask : TX_SetFrameError

  task TX_SetFrameCover(input mii_sva_tx_cover_type i);
    TX_FrameCover = i | TX_FrameCover;
  endtask : TX_SetFrameCover

  // TX MAC variables (back off delay calculations)

  bit [4:0] TX_BackOffState  = 0;
  bit TX_Collision           = 0;
  int TX_BackOffDelay        = 0;

  // sampling clock domain
  clocking txc @(posedge TX_CLK);
    // By default input #1step
    input TX_EN, TX_ER, TXD, COL, CRS;
    input rose_TX_EN, fell_TX_EN;
    input TX_Word, TX_RevWord, TX_D_Word;
  endclocking

// Boolean markers of positions in a frame

  wire TX_SdfValid = (TX_Word[15:8] == {SdfH, SdfL}) &&
                     (TX_NibbleCnt == 0) ;
  wire TX_DestAddrValid = (TX_NibbleCnt == 16'd12);
  wire TX_SrcAddrValid = (TX_NibbleCnt == 16'd24);
  wire TX_qTagValid = (TX_NibbleCnt == 16'd28) &&
                      (TX_RevWord == {qTagHigh, qTagLow});
  wire TX_NoTagLengthValid = (TX_NibbleCnt == 16'd28) &&
       (TX_RevWord <= maxValidFrame);
  wire TX_TagLengthValid = (TX_NibbleCnt == 16'd36) &&
       (TX_RevWord <= maxValidFrame);
  wire [15:0] TX_DataLength = TX_NoTagLengthValid || TX_TagLengthValid ? 
                 TX_RevWord : 
                 16'b0;
  wire TX_NoTagTypeValid = (TX_NibbleCnt == 16'd28) &&
       (TX_RevWord >= minTypeValue) && !TX_qTagValid;
  wire TX_TagTypeValid = (TX_NibbleCnt == 16'd36) &&
       (TX_RevWord >= minTypeValue);
  wire TX_EndOfFrame = !TX_EN && past_TX_EN;

// Update nibble count, FCS calculation, data word TX_D_Word_r

  always @(txc) begin : tx_frame_counts
    if (resetting || !txc.TX_EN) begin
      TX_NibbleCnt <= 0;
      TX_D_Word_r <= 0;
      past_TX_EN <= 0;
      TX_Fcs <= 32'hffffffff; // On rising edge of TX_EN?
    end 
    else begin
      TX_D_Word_r <= txc.TX_D_Word;
      past_TX_EN <= txc.TX_EN;
      if (TX_NoTagLengthValid || TX_TagLengthValid) 
        TX_FrameSize <= TX_RevWord ;
      if ((TX_Word[15:8] == {SdfH, SdfL}) ||
          (TX_NibbleCnt > 0)) begin
        TX_NibbleCnt <= TX_NibbleCnt + 1;
        if (TX_NibbleCnt > 8) TX_Fcs <= CRC32(TX_D_Word_r[3:0], TX_Fcs);
      end
    end
  end  : tx_frame_counts

// Initialize to 0 Error and Cover flags upon reset
`ifndef SYNTHESIS
  always @(posedge TX_CLK)
    if (resetting) begin
      TX_FrameError <= 0;
      TX_FrameCover <= 0;
    end
`endif

// MAC TX processes
// ================

// compute max backoff delay
  always @(txc) begin 
    if (!not_resetting) begin
      TX_BackOffState <= 0; // counts number of retransmissions
      TX_Collision <= 0; // collision occured in a frame
      TX_BackOffDelay <=0; // counter of interframe cycles
    end
    else begin
      // remember if COL occured until beginning of next frame
      if (txc.rose_TX_EN) TX_Collision <= 1'b0;
      if (txc.TX_EN && txc.COL) TX_Collision <= 1'b1;
      // maintain number of retransmissions
      // and count cycle in interframe gap
      if (txc.fell_TX_EN) begin
        if (TX_Collision && (TX_BackOffState < mii_TX_max_attempts))
             TX_BackOffState <=  TX_BackOffState + 1;
        else TX_BackOffState <= 0;
        TX_BackOffDelay <= 1;
      end else
        if (!txc.TX_EN) TX_BackOffDelay <= TX_BackOffDelay + 1;
    end
  end


// RX variables and processes
//===========================

  logic [31:0] RX_D_Word_r = 0;
  wire [15:0] RX_Word = {RXD, RX_D_Word_r[31:20]};
  wire [15:0] RX_RevWord = {RX_Word[7:0], RX_Word[15:8]};
  wire [31:0] RX_D_Word = {RXD, RX_D_Word_r[31:4]};

  logic past_RX_DV = 1'b0; // pas value of RX_DV 
  wire rose_RX_DV = !past_RX_DV && RX_DV;
  wire fell_RX_DV = past_RX_DV &&!RX_DV; 

  // nibble counters, Frame byte counters bits [15:1]
  length_type RX_NibbleCnt = 0;

  // frame size for comparison when RX_DV deasserted
  logic [15:0] RX_FrameSize = 0;
                               
  logic [31:0] RX_Fcs = 32'hffffffff; // accumulate CRC

  // flags for reporting an error detected by an assertion to TB
  // similar to TX

  task RX_SetFrameError(input mii_sva_rx_error_type i);
    RX_FrameError = i | RX_FrameError;
  endtask : RX_SetFrameError

  task RX_SetFrameCover(input mii_sva_rx_cover_type i);
    RX_FrameCover = i | RX_FrameCover;
  endtask : RX_SetFrameCover

  bit RX_Collision           = 0; // memorize collision occured

  // sampling clock domain
  clocking rxc @(posedge RX_CLK);
    // By default input #1step
    input RX_DV, RX_ER, RXD, COL, CRS;
    input rose_RX_DV, fell_RX_DV;
    input RX_Word, RX_RevWord, RX_D_Word;
  endclocking

// Boolean markers of positions in a frame

  wire RX_SdfValid = (RX_Word[15:8] == {SdfH, SdfL}) &&
                     (RX_NibbleCnt == 0) ;
  wire RX_DestAddrValid = (RX_NibbleCnt == 16'd12);
  wire RX_SrcAddrValid = (RX_NibbleCnt == 16'd24);
  wire RX_qTagValid = (RX_NibbleCnt == 16'd28) &&
                      (RX_RevWord == {qTagHigh, qTagLow});
  wire RX_NoTagLengthValid = (RX_NibbleCnt == 16'd28) &&
       (RX_RevWord <= maxValidFrame);
  wire RX_TagLengthValid = (RX_NibbleCnt == 16'd36) &&
       (RX_RevWord <= maxValidFrame);
  wire [15:0] RX_DataLength = RX_NoTagLengthValid || RX_TagLengthValid ? 
                 RX_RevWord : 
                 16'b0;
  wire RX_NoTagTypeValid = (RX_NibbleCnt == 16'd28) &&
       (RX_RevWord >= minTypeValue) && !RX_qTagValid;
  wire RX_TagTypeValid = (RX_NibbleCnt == 16'd36) &&
       (RX_RevWord >= minTypeValue);
  wire RX_EndOfFrame = !RX_DV && past_RX_DV;

// Update nibble count, FCS calculation, data word RX_D_Word_r

  always @(rxc) begin : rx_frame_counts
    if (resetting || !rxc.RX_DV) begin
      RX_NibbleCnt <= 0;
      RX_D_Word_r <= 0;
      past_RX_DV <= 0;
      RX_Fcs <= 32'hffffffff; 
      RX_Collision <= 0;
    end 
    else begin
      if (rose_RX_DV) RX_Collision <= 0;
      if (rxc.RX_DV && rxc.COL) RX_Collision <= 1;
      RX_D_Word_r <= rxc.RX_D_Word;
      past_RX_DV <= rxc.RX_DV;
      if (RX_NoTagLengthValid || RX_TagLengthValid) 
        RX_FrameSize <= RX_RevWord ;
      if ((RX_Word[15:8] == {SdfH, SdfL}) ||
          (RX_NibbleCnt > 0)) begin
        RX_NibbleCnt <= RX_NibbleCnt + 1;
        if (RX_NibbleCnt > 8) RX_Fcs <= CRC32(RX_D_Word_r[3:0], RX_Fcs); 
      end
    end
  end  : rx_frame_counts

// Initialize to 0 Error and Cover flags upon reset
`ifndef SYNTHESIS
  always @(posedge RX_CLK)
    if (resetting) begin
      RX_FrameError <= 0;
      RX_FrameCover <= 0;
    end
`endif


// MII Property definitions, TX and RX
// ===================================

  // as a rule, the last nibble received is taken directly from the
  // port, only previous nibbles and bytes are taken from
  // Nibble buffers if needed. 

`ifndef SVA_CHECKER_FORMAL
  property mii_1_p(miiEN, miiD, miiER);
    disable iff(resetting)
      ((miiEN ^ miiEN) == 0) &&
      ((miiD ^ miiD) == 0) &&
      ((miiER ^ miiER) == 0) &&
      ((COL ^ COL) == 0) &&
      ((CRS ^ CRS) == 0) ;
  endproperty :  mii_1_p
`endif

  // CRS remains asserted during collision condition COL. 
  property mii_2_p;
    disable iff (resetting || mii_FullDuplex) 
      !COL ##1 COL[*1:$] |-> CRS;
  endproperty : mii_2_p

// Example 3-12 Using Flags to Disable Other Assertions  
// TX_EN can become asserted only when CRS is deasserted
  property mii_TX_3_p; 
    disable iff (resetting || (|TX_FrameError) || mii_FullDuplex) 
      CRS && !RX_DV || $rose(RX_DV) ##4 1'b1 |-> !$rose(TX_EN);
  endproperty : mii_TX_3_p

  // TX_EN == 0 and TX_ER == 1 is a reserved state
  property mii_TX_4_p;
    disable iff (resetting)
      not (!TX_EN && TX_ER);
  endproperty : mii_TX_4_p

  // TX_EN is asserted with the first nibble of Preamble, 
  // there are 7 preamble bytes, followed by SDF.
  property mii_TX_5_p;
    disable iff (resetting || COL && !mii_FullDuplex)
      $rose(TX_EN) |-> (TXD == Preamble)[*14];
  endproperty : mii_TX_5_p

  property mii_TX_6_p; // First low order nibble of SDF
    disable iff (resetting || COL && !mii_FullDuplex) 
      $rose(TX_EN)  |-> ##14 TXD == SdfL;
  endproperty : mii_TX_6_p

  property mii_TX_7_p; // Second high order nibble of SDF
    disable iff (resetting || COL && !mii_FullDuplex) 
      $rose(TX_EN)  |-> ##15 TXD == SdfH;
  endproperty : mii_TX_7_p

  //  When there is no collision, between frame enable asserted 
  // and then deasserted there must be 2N nibbles
  property mii_8_p(SdfValid,EndOfFrame, NibbleCnt);
    disable iff (resetting || COL && !mii_FullDuplex)
      SdfValid ##1 EndOfFrame[->1] |-> NibbleCnt[0];
  endproperty : mii_8_p

  // CRS is asserted Kt = 2 clock cycles after TX_EN or RX_DV is 
  // asserted and remains asserted while TX_EN or RX_DV is asserted.
  property mii_9_p(miiEN, delay);
    disable iff (resetting || mii_FullDuplex)
      !miiEN ##1 miiEN |-> ##delay (CRS[*1:$]) ##1 !miiEN;
  endproperty : mii_9_p

  // During transmission when CRS is set then a 32 bit == 8 nibble jam
  // sequence is transmitted and then TX_EN is deasserted
  property mii_TX_10_p;
    disable iff (resetting || mii_FullDuplex)
      TX_EN  throughout (!COL ##1 COL)  |-> 
          TX_EN[*(2*jamSize):2*jamSize+4] ##1 !TX_EN; 
  endproperty : mii_TX_10_p

  // The resulting FCS when jamming must be invalid.
  // property is likely not be suitable for Magellan
  property mii_TX_11_p;
    disable iff (resetting || mii_FullDuplex)
      (TX_EN && (TX_NibbleCnt != 0) && TX_Collision) ##1 !TX_EN |-> 
          (TX_D_Word_r != complement_reverse(TX_Fcs));
  endproperty : mii_TX_11_p