Design of SystemVerilog Assertion IP

by E. Cerny¹, J. Bergeron², M. K. Thottasseri³ and T. Anderson⁴, Synopsys, Inc.
¹Marlborough, USA; ²Ottawa, Canada; ³Bangalore, India; ⁴Mountain 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:


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:


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 macro COVER_ON.


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.  ¹

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 the TX_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.

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 and interfaces), 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.

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.


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.


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).

Fig. 8    Hierarchical protocol checker

Consider the following point-to-point protocol: Device Master asserts req and holds it until ack 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 interface deals 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 and req_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 packet and cnt) to the next protocol layer, which is called here DL (for data-link layer). The top-level interface 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 the req–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.