Lib4U

‎"Behind every stack of books there is a flood of knowledge."

Design of SystemVerilog Assertion IP

20050310_synopsys1

by E. Cerny1, J. Bergeron2, M. K. Thottasseri3 and T. Anderson4, Synopsys, Inc.
1Marlborough, USA; 2Ottawa, Canada; 3Bangalore, India; 4Mountain View, USA

Abstract:

SystemVerilog provides an effective means for designing assertion-based Verification IP and integrating it with a testbench. This paper explores guidelines for designing such IP within the Synopsys Verification Methodology.

INTRODUCTION

Concurrent properties (assert, cover, and assume) [SVA] are an integral part of SystemVerilog [LRM]. They provide an effective way to improve observability and localization of design errors by placing functional checks at critical points inside design blocks and on internal and external interfaces. When an assertion fails during simulation, the cause of the reported error can be more easily identified than by observing external design-under-test (DUT) outputs. Assertions can also be proven or falsified using formal tools, thereby increasing confidence in the quality of the design.

In addition, property coverage provides information on how well the design has been functionally exercised during simulation. Still uncovered properties may serve as search goals to formal tools that can generate test sequences to stimulate the design and reach that goal. Using these test sequences in simulation (with the assertions enabled) helps to bring verification to completion.

Assertion and coverage properties on internal signals and interfaces of design blocks should ideally be inserted by the designers because they are the ones with intimate knowledge of the implementation details. Such assertions also have the role of “active” comments that document the implementation.

Assertion and coverage properties on external interfaces of the design are usually provided by the verification engineers. They reflect the function rather than the implementation of the design. Interface protocols are generally the main target of assertion-based checks. The end-to-end behavior is often more convenient to verify using testbench code that may involve score-boarding techniques (possibly supplemented with assertions).

Regardless where deployed, assertions and coverage for typical behaviors can be packaged in modules or interfaces for reuse as part of a basic SystemVerilog Assertion-based checker library such as the one provided with the Synopsys VCS simulator. These checkers deal with lower-level generic properties that can be seen in many designs, including various handshakes, mutual exclusion, basic arbitration, time separation of signal transitions, and signal validity windows.

Checkers for standard protocols such as PCI Express, AMBA AHB, and MII/MAC each encompass a complete set of checks and coverage points for the protocol. These are packaged as reusable SystemVerilog Assertion IP, preferably in one or more SystemVerilog interfaces. The instantiation of the checker within the external DUT interface as recommended in the SystemVerilog Verification Methodology Manual [VMM] facilitates the observation of the DUT and interactions with the testbench program.

In this paper, we discuss guidelines for implementing SystemVerilog Assertion IP. There are existing guidelines for constructing similar IP using other temporal languages such as OpenVera Assertions [OVA]. However, only SystemVerilog provides complex data types and excellent methods of interaction between assertions, the design, and the testbench. The architecture of checker IP can thus benefit from assertion and coverage control, feedback to the testbench, and uniform reporting.

It is essential that the IP be reusable with formal and hybrid formal tools (such as Magellan), both as assertions on the behavior of the DUT and as assumptions (constraints) on the environment around the DUT. This supports the “assume-guarantee” method of formal analysis. As shown in Fig. 1, properties on interface signals are used as assertions to verify the block on one side of the interface and as assumptions to verify the block on the other side.


Fig. 1    Use of assertions and assumptions

In this example, an interrupt signal running from Block A to Block B can be asserted no more frequently that every five clock cycles. When verifying Block A in formal analysis (or in simulation), this rule is treated as an assertion to guarantee that the block asserts the interrupt signal correctly. However, Block B is verified formally subject to the assumption that this rule is met and that the interrupt signal behaves correctly.

Requirements

The development of reusable SystemVerilog Assertion IP must take into account many factors, among them:

  • Encapsulation
  • Configuration of protocol and resources
  • Compile-time and run-time controls
  • Assertions vs. assumptions (constraints) in simulation and formal tools
  • Coverage collection
  • Reporting of usage errors and failures
  • Integration with testbench
  • Efficiency
  • Protection/encryption
  • Documentation

The rest of this paper concentrates on guidelines for those factors that affect the architecture of the checker and concludes with a small example illustrating a hierarchical checker.

GUIDELINES

Encapsulation

The choices are module, interface, or program. We recommend encapsulation in one or more interface constructs (as in Fig. 2) for the following reasons:

  • An interface can be instantiated or bound anywhere: in a module, interface or program.
  • It is an appropriate place to define interface protocols.
  • It can be instantiated like a module.
  • It can be passed through virtual interface constructs to instances of transactor classes in a testbench program for control and accessing information collected by the checker IP.

Configuration

Global controls, such as the overall enabling of assertions, coverage, and simulation-only properties, are implemented by macro symbols and using `ifdef – `endif constructs. In the Synopsys checker library, we define the following macro symbols for all checkers:

ASSERT_ON : includes assertions
COVER_ON : includes cover statements
ASSERT_GLOBAL_RESET : applies a reset to all checkers, consistent with the Open Verification Library [OVL]
SVA_CHECKER_FORMAL : excludes non-synthesizable assertions

Configuration that is specific to an instance of a checker must be selectable using interface parameters. These include variable sizing, detailed property selection, assume vs. assert, etc. The parameters are used in conditional and loop statements within generate blocks. We use the following parameters in all checkers:

severity_level : reaction to assertion failures
category : classification of the checker
coverage_level : selection of coverage items
assert_name : checker name
no_next_fail : block next failures after a failure
msg : user text message
assume : select assume rather than assert

The example in Fig. 2 illustrates the encapsulation and parameters of a Media Independent Interface [MII] checker. The attribute (* sva_checker *) identifies this interface to be a checker. This allows tools to treat it in the appropriate way for reporting purposes. The parameter mii_TX_max_retries specifies the maximum number of retransmissions that the DUT is to support before dropping the frame. The parameter coverage_level allows the user to enable individual cover points in addition to the global control using the macroCOVER_ON.

(* sva_checker *) interface mii_sva_checker
  (reset_n, TX_CLK, TX_EN, TX_ER, TXD, COL, 
       CRS, RX_CLK, RX_DV, RX_ER, RXD,
       TX_FrameError, RX_FrameError,
       TX_FrameCover, RX_FrameCover);
parameter int severity_level        = 0;
parameter int category              = 0;
parameter     msg                   = “”;
parameter bit no_next_fail          = 1;
parameter int coverage_level        = -1;
parameter bit mii_TX_assume         = 1’b0;
parameter bit mii_RX_assume         = 1’b0;
parameter int mii_TX_max_retries    = 10;
localparam assert_name = “mii_sva_checker”;
input logic reset_n, TX_CLK, TX_EN, TX_ER;
input logic COL, CRS, RX_CLK, RX_DV, RX_ER;
input logic [3:0] TXD, RXD;
output mii_sva_error_size_type 
            TX_FrameError, RX_FrameError,
            TX_FrameCover, RX_FrameCover;
.
.
.
endinterface : mii_sva_checker

Fig. 2    MII Checker interface and parameters

Assertions and Assumptions

Encapsulation by signal direction: If the protocol to be verified is multi-agent, for example multiple masters and slaves on an ARM AHB bus, we recommend encapsulating the checker of each agent type into a separate interface.  Each such checker verifies the outputs of the agent, while using the inputs in the enabling conditions of the assertions. This has two advantages:

  • The overall checker can be easily configured for any number of agents.
  • Some of the checkers can act as assertions to be verified (for example, a slave checker), and others as assumptions on inputs (for example, an AHB master checker acting through the assumptions as an abstract model of a master when verifying a slave DUT).

For point-to-point protocols, such as MII, both sides of the protocol can be enclosed in one interface, with the parameters selecting which property is an assertion and which is an assumption for the given instance of the checker (as in Fig. 2).

Use in random simulation: If the checker is used as assumptions (constraints) on the DUT environment in hybrid formal tools, the properties should not refer only to past values of DUT input signals. This is because such tools employ random simulation constrained by these sequential assumptions, and constraining past values may lead to an empty solution space (a dead end) during the simulation.  1

Protocol hierarchy: If the protocol is layered, such as is the case for PCI Express, it is preferable to follow this layered structure in the checker as well. It makes it easier to write the checker and to use the layers independently when verifying protocol layers separately. This means that some aspects of data checking may require partial assembly of the data into buffers for checking a property. However, if the checker is used as constraints it is useful to change the direction of data flow in the checker so that the data property can constrain the values and then drive them under lower–level assumptions to the DUT input ports.  A simplified version of such a checker is shown in the example at the end of this paper.

Interaction with the Testbench

Each checker must operate either as an independent monitor, for instance with formal tools, or as part of a testbench. In the latter case, the checker is part of a testbench monitor and it is not necessary to duplicate the verification of the interface protocol. However, the testbench monitor must be aware of failures detected by the assertion-based checker. The SystemVerilog language provides a number of mechanisms for this interaction. The following system is adopted in the SystemVerilog VMM methodology:

  • The checker(s) are instantiated inside the interfaces associated with the DUT.
  • The DUT module and its interface(s) are instantiated in a top-level module.
  • The testbench program connects to the DUT using virtual interfaces in the transactor classes by associating them with the interface instances in the top level module. The testbench can thus access the checker instances and their assertions, variables, and ports. This hierarchy is illustrated in Fig. 3 for an Ethernet core.
  • Each assert property statement sets a flag in its action block if it fails. Each cover property sets a flag when it matches, for example the output ports in Fig. 2.
  • The testbench monitor associated with the checker observes the flags. Whenever one of the assertion flags is set, it can decide to drop the observed data, report an error, etc. Should the testbench decide to proceed with the simulation, it may then clear the flags using a task clear provided in the checker or disable the assertions using $assertoff and continue. When one of the coverage flags is set, the testbench may decide to disable the coverage or take some reactive action.

Additionally, upon failure of an assertion, the flags can be used to disable all other assertions and coverage until the testbench clears the flags. This feature is enabled using a parameter of the checker, for example no_next_fail in Fig. 2.


Fig. 3    Ethernet core testbench and checkers

A portion of the checker code is shown in Fig. 4: mii_sva_tx_error_type is an enumerated type that sets the corresponding bit of the failure in the TX_FrameError vector using theTX_SetFrameError task. In each TX property, the signal TX_resetting contains a reduction OR over all the error flags used within the disable iff construct in all assertions and coverage statements. Therefore, once any assertion fails, all other assertions that should evaluate afterwards are disabled until the flags are clear.

wire TX_BlockFail = no_next_fail && 
                   (|TX_FrameError);
wire TX_resetting = TX_BlockFail || 
                    !reset_n;

task TX_SetFrameError(
    input mii_sva_tx_error_type i);
    TX_FrameError = i | TX_FrameError;
endtask : TX_SetFrameError
.
.
.
property mii_1_p(resetting);
  disable iff (resetting) COL |-> CRS;
endproperty : mii_1_p

mii_TX_1: assert property (mii_1_p(TX_resetting)) 
  else begin
    sva_std_error(“failure explanation”);
    TX_SetFrameError(MII_TX_NO_CRS_W_COL);
  End
.
.
.

Fig. 4    Disabling assertions by failures

Reporting

For easy interpretation of results and information management, it is important to maintain uniform reporting formats and controls. The SystemVerilog VMM introduces a class and methods for reporting all messages in a uniform way. The user can easily select severity levels, decide which messages should be passed to the user and which should be filtered out, and define the global format of all messages. Since SystemVerilog integrates testbench constructs (such as classes) and design constructs (such as modules andinterfaces), the log class is also used in checkers for outputting all messages.

However, the checkers may also be used outside the SystemVerilog VMM context; so the Synopsys library also provides reporting using a $display statement, similar to the OVL approach. For this reason, message output is hidden in tasks in the sva_std_task.h file that is referenced with a `include in each checker. The task call sva_std_error(“failure explanation”) in 0 is an example of using this approach. The default structure of the task is to report via the VMM log is shown in Fig. 5, but the user can edit the file and change it to another form, such as an OVL-style message.

vmm_log log_inst = // inst. in checker
   new(“mii_sva_checker”, $psprintf(“%m”));

task sva_std_error(
  input string err_msg = “”);//user message
                  
 vmm_error(log_inst, 
   $psprintf(“Failure : category : %0d %s”, 
              category, err_msg));
endtask

Fig. 5    VMM log instance and error reporting task

Coverage

Coverage in the checkers can be collected using cover property, covergroup, or a combination thereof. Furthermore, sampling in a covergroup can be triggered by a SystemVerilog sequence or by an event sent from the action block of a cover property. We discourage using assert property for functional coverage because it has a different intent and provides a different kind of information.

Cover properties are generally useful to detect the occurrence of specific sequences of events, but are a poor mechanism for covering data or delay values (although it can be done within generate loops in a rather inefficient way).

For example, to detect (cover) the fact that a collision occurred on the last nibble of an MII TX frame, one can use the cover property in Fig. 6.

mii_TX_cov_COL_last: cover property (
 @(posedge TX_CLK) 
    1’b1 ##1 ((!TX_resetting && TX_EN) 
          throughout 
            ($rose(TX_EN) ##0 COL[->1]))
      ##1 !TX_EN ) ;

Fig. 6    MII TX coverage on collision at last nibble

However, covering different lengths of a frame is better achieved using a cover group as shown in 0. In this code, cnt is a local variable that counts the number of nibbles in the frame, and store_TX_Lngth is a task that converts the count to octets and stores it in a static variable TX_FrameLngth. This variable is sampled by the covergroup instance when the sequence frame_length_s is triggered.

int TX_FrameLngth = 0;
task store_TX_Lngth(int x);
  TX_FrameLngth = x; 
endtask : store_TX_Lngth

covergroup length_cg @frame_length_s;
  coverpoint TX_FrameLngth;
  option.per_instance = 1;
  type_option.strobe = 1;
endgroup : length_cg

sequence frame_length_s;
  int cnt;
  @(posedge TX_CLK) 1’b1 ##1 
  ( (not_resetting && !COL) throughout  
    ($rose(TX_EN, cnt=1) ##0 
    (TX_EN, cnt++)[*0:$]) )
  ##1 
  (!TX_EN, store_TX_Lngth(cnt)) 
endsequence : frame_length_s

length_cg mii_TX_frame_length = new ();

Fig. 7    Coverage of MII TX frame lengths

CHECKER EXAMPLE

The example in Fig. 8 is a fragment of a hierarchical checker showing how layers of a protocol can be implemented as layers in the checker. The checker can be used both as assertions and assumptions (constraints).

// interface linking PL and DL layers
// assembles / disassembles “packets”
// to / from DL layer
interface PL_DL_link(rst, clk, ack, data );
  parameter 
    bit ack_assume = 0, req_assume = 0;
  input logic rst, clk, ack;
  inout [7:0] data;
// variables for the DL layer
  logic [1:0][7:0] packet;
  logic cnt = 0; // only 2 octets
  default clocking p_clk  
    @(posedge clk);
// count 2 data octets 
  always @p_clk 
    cnt <= rst ? 0 : p_clk.ack ? 
                       !cnt : cnt;  
  generate
    if (ack_assume) begin : drive
// disassemble packet into octets
      assign data = rst ? 
        0 : ack ? 
        (cnt ? packet[1] : packet[0]) :
        0;
// stable packet during disassembly
      assume_data_2: assume property  
        ( disable iff (rst)
          (1’b1 ##1 !$fell(cnt)) 
            |-> $stable(packet)
         );
    end : drive
    else begin : verify
// assertion on data, assemble packet
      always @p_clk
        packet[cnt] <= p_clk.rst ?
           0 : p_clk.ack ? 
                 p_clk.data :
                  packet[cnt];
    end : verify
  endgenerate
endinterface
    
// DL layer checker with properties of 
// “data link” layer
interface DL_checker 
  parameter bit ack_assume = 0;
  ( PL_DL_link PL_DL );
  property p_data_1;
    @(posedge PL_DL.p_clk) 
    disable iff (PL_DL.rst)
      (1’b1 ##1 $fell(PL_DL.cnt)) 
         |-> (data_property);
  endproperty

  generate
    if (ack_assume) begin : drive
// assumption on data
      adt1: assume property (p_data_1);
    end : drive
    else begin : verify
// assertion on data
      adt1: assert property (p_data_1) else 
     checker_error(“data_property failed”);
    end : verify    
  endgenerate
endinterface
    
interface MultilevelChecker (
  rst, clk, req, ack, data );
  parameter bit ack_assume = 0;
  input logic rst, clk, req, ack;
  inout [7:0] data;

// properties of req
  property p_req1; // stable req
    @(posedge clk) disable iff (rst)
      $rose(req) |-> req[*1:$] ##0 ack;
  endproperty
  property p_req2; // req Return-to-Zero
    @(posedge clk)  disable iff (rst)
      ack |-> ##1 ((!req)[*1:5]);
  endproperty
// properties of ack
  property p_ack1; // pulse only
    @(posedge clk) disable iff (rst)
      ack |-> ##1 !ack;
  endproperty
  property p_ack2; // no ack w/o req
    @(posedge clk) disable iff (rst)
      !req |-> !ack;
  endproperty
  property p_ack3; // ack latency
    @(posedge clk) disable iff (rst)
      $rose(req) |-> ##[1:5] ack;
  endproperty

  generate
    if (ack_assume) begin : drive_ack
      aa1: assume property (p_ack1);
      aa2: assume property (p_ack2);
      aa3: assume property (p_ack3);
    end : drive_ack
    else begin : verify_ack
      aa1: assert property (p_ack1) else 
       checker_error(“…”);
      aa2: assert property (p_ack2) …; 
      aa3: assert property (p_ack3) …;
    end : verify_ack
    if (req_assume) begin : drive_req
      ar1: assume property (p_req1);
      ar2: assume property (p_req2);  
    end : drive_req
    else begin : verify_req
      ar1: assert property (p_req1) …;
      ar2: assert property (p_req2) …;  
    end : verify_req
  endgenerate
    
// interface instance to DL layer
  PL_DL_link #(ack_assume)
    PL_DL_link_i(rst, clk, ack, data);
// DL layer checker DL properties
  DL_checker  #(ack_assume)
    DL_checker_i (PL_DL_link_i);
endinterface

Fig. 8    Hierarchical protocol checker

Consider the following point-to-point protocol: Device Master asserts req and holds it untilack is received from Slave. At that point, data is placed by Slave on 8-bit wide data and is valid for one clock cycle—the duration of ack. req must stay high until and including ack is asserted, and then req must be deasserted for at least one cycle. ack cannot be asserted unless req is asserted.  The data can be of any length and may, on each of its components, satisfy some higher-level properties. In addition, data should be made available to the testbench if so desired. For simplicity, we limit data to 2 octets and its value must satisfy some property data_property.

The multi-layer protocol checker in Fig. 8 has the following structure. The top-level interfacedeals with the low-level protocol, called here PL (for physical layer), and contains assertions on req and ack. The top-level interface contains an instance of another interface that does the packet assembly into (for assertions on data) or disassembly (for assumptions on data) from a variable called packet. The choice is controlled by the parameters ack_assume andreq_assume: ack_assume determines whether properties of ack and data should be assumed or asserted, while req_assume determines whether properties of req should be assumed or asserted.

The interface PL_DL_link presents the two pertinent pieces of information (variables packetand cnt) to the next protocol layer, which is called here DL (for data-link layer). The top-levelinterface contains an instance of the data-link layer interface. The assembled data in packet and synchronization variable cnt can be accessed by the testbench by providing reference to the checker interface instance.

The example in Fig. 8 is missing the log class instance, coverage statements (such as thereq–ack latencies), control over enabling assertions and coverage, reset options, and other details. Nevertheless, it illustrates the flexibility of SystemVerilog for designing protocol checker IP.

CONCLUSIONS

We have outlined the main concerns when designing SystemVerilog Assertion IP, provided examples of guidelines governing the design of such IP, and illustrated a hierarchical checker by using a small example.

Future work will include resolving IP protection and other issues related to the distribution of this kind of verification IP.

References

[LRM] SystemVerilog 3.1a Language Reference Manual, Accellera, May 2004.

[MII] IEEE Standard 802.3-2002, IEEE, March 2002.

[OVA] E. Cerny, S. Dudani, “Authoring Assertion IP using OpenVera Assertion Language,” Proceedings of the International Workshop on IP-Based System-on-Chip Design, October 2002.

[OVL] Open Verification Library Assertion Monitor Reference Manual, Accellera, June 2003.

[SVA] T. Fitzpatrick, “Assertions in SystemVerilog: A Unified Language for More Efficient Verification,” http://www.synopsys.com/products/simulation/assert_sverilog_wp.pdf, October 2003.

[VMM] J. Bergeron, E. Cerny, A. Hunter, A. Nightingale, SystemVerilog Verification Methodology Manual, to be published in 2005.

A tool may be able to handle constraints over past values, but possibly at the cost of reduced performance.

Source:

http://www.design-reuse.com/articles/9875/design-of-systemverilog-assertion-ip.html

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

Information

This entry was posted on March 30, 2013 by in Electronic & Computer Engineering, IC Design & Fabrication, Science & Technology.
Virtual Fashion Technology

Virtual Fashion Education

toitocuaanhem

"chúng tôi chỉ là tôi tớ của anh em, vì Đức Kitô" (2Cr 4,5b)

VentureBeat

News About Tech, Money and Innovation

digitalerr0r

Modern art using the GPU

Theme Showcase

Find the perfect theme for your blog.

lsuvietnam

Learn to Learn

Gocomay's Blog

Con tằm đến thác vẫn còn vương tơ

Toán cho Vật lý

Khoa Vật lý, Đại học Sư phạm Tp.HCM - ĐT :(08)-38352020 - 109

Maths 4 Physics & more...

Blog Toán Cao Cấp (M4Ps)

Bucket List Publications

Indulge- Travel, Adventure, & New Experiences

Lib4U

‎"Behind every stack of books there is a flood of knowledge."

The WordPress.com Blog

The latest news on WordPress.com and the WordPress community.

%d bloggers like this: