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.
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.
The development of reusable SystemVerilog Assertion IP must take into account many factors, among them:
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.
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.
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
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
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.
(* sva_checker *) interface mii_sva_checker (reset_n, TX_CLK, TX_EN, TX_ER, TXD, COL,
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.
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.
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.
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.
wire TX_BlockFail = no_next_fail &&
mii_TX_1: assert property (mii_1_p(TX_resetting))
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.
vmm_log log_inst = // inst. in checker
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.
covergroup length_cg @frame_length_s;
length_cg mii_TX_frame_length = new ();
Fig. 7 Coverage of MII TX frame lengths
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
// DL layer checker with properties of
interface MultilevelChecker (
// properties of req
// interface instance to DL layer
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.
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.
|If you have any suggestion/feedback please email it to firstname.lastname@example.org|