Authoring assertion IP using OpenVera assertion language

by Surrendra Dudani, Eduard Cerny, Synopsys, Inc.
Marlborough, MA, USA

Abstract:
Developing assertions from a specification is a difficult process. The availability of assertion IP is significant in reducing the verification effort and improving the design quality. We describe the basic requirements for an assertion language to be suitable for Assertion IP development, demonstrate how these requirements are met by the Open Vera Assertion (OVA) language, and outline guidelines for writing an IP in OVA. An example based on the PCI bus protocol checker is presented to illustrate the methodology.

INTRODUCTION
Developing assertions from a design specification can be a lengthy and difficult process. It requires correct interpretation of the design and an understanding of the verification environment in which assumptions regarding the inputs and operation of the design are made. This process is error prone and difficult, as the observed error can be in the design, in the test bench or in the assertion itself. As designs that are more complex are built, the verification code and assertions needed to validate these design behaviors become disproportionately larger than the designs themselves. However, once the assertions covering their behavior have been debugged, they become an important and valued Intellectual Property (IP), as they can be reused with confidence in many other designs.

The availability of assertion IP is significant in reducing the verification effort and improving the design quality. Its value comes from the fact that the assertions can passively monitor the design behavior by simply attaching them to the target design, without modifying the code representing the design. The errors indicated by the assertions point to design bugs, and the debugging information provided by the errors readily assists the designers to fix the bugs. Without needing to rewrite assertions or rules of behavior for each project, pre-built assertions from assertion IP provide powerful quality criteria for sign-off.

Over the past few years, the design community has begun addressing the reuse of design blocks from previous projects and commercially available IP designs. As larger and larger designs are built, it becomes necessary to reuse verification environment as much as possible from existing designs, including various internal and 3rd party IP blocks. To ease integration, IP blocks often rely on the use of standard interface protocols, like SPI-4, ARM AMBA, and PCI. Associated with the reusable designs, a well-designed verification environment is essential for ensuring that the integration of the IP design blocks retains the quality needed for first silicon success. The interface assertions for the standard protocols are prime reusable assertion IP [2].

There are many commercial assertion IP products available, but they are developed in proprietary languages and tools. Assembling assertions from different commercial vendors for a design is not easily attainable. As a result, the usage of such IP products has been limited, as the assertions cannot be authored, extended, or executed interchangeably between different tools. At the first sight, it seems that writing assertions for bus protocols is rather straight forward, by looking at the timing diagrams, state machines and textual specifications. However, for the Assertion IP to be usable in many designs and in different verification environments, it must be formulated in certain ways and appropriately packaged. Furthermore, the assertion language must provide richness of expression of temporal properties, and for their encapsulation and parameterization.

Hardware Description Languages (HDL) can be used for developing such assertions, but the level of abstraction is too low. Sequences of signal values have to be described using state machines that hide the original meaning of the assertion and make it more difficult to debug. If in addition such assertions are to be used on pipelined designs, many checks must overlap in time. The structure of the assertion then becomes even more complex, to the point where it starts resembling the pipelined design it is to verify. Due to this similarity between the design code and the verification code, the same errors can appear in both and thus there is great potential for not detecting design errors. Furthermore, the assertion HDL code is as difficult to debug as the original design.

Assertion languages [1, 3, 4] are much more appropriate for checker development. This is because they raise the level of abstraction and allow a direct formulation of design properties in terms of sequences and their combinations. It is then a much easier and less error-prone process. Although such languages have been used in research institutions for years, only recently a number of such languages and associated software tools have emerged as commercial products.  Standardization is also in progress by the Accellera committee.

The Open Vera Assertion language (OVA) provides the means for writing effective assertions and for packaging them into reusable Assertion IP. Such Assertion IP should be usable in the context of dynamic verification (simulation) as well as static verification (property checking). If properly instrumented it can provide information on the coverage of various functional features of the design and do it in a way that combines the coverage results from simulation and formal property checking. The functional coverage based on assertions can be combined with the classical code-coverage metrics to yield a better picture of the status of the verification, resulting in higher confidence in the quality of the design.

In the rest of the paper, we describe the basic requirements for an assertion language to be suitable for Assertion IP development, demonstrate how these requirements are met by the OVA language, and outline guidelines for writing an IP. An example based on the PCI bus protocol checker is presented to illustrate the method.  

Requirements for an assertion language
An assertion language should possess the following features:

• Basic event definition and sequencing to specify the order of events
• Time bounded sequences with references to past and future
• Complex sequences using logic connectives (such as AND and OR)
• Repetition of sequences
• Conditional sequences with conditions to trigger or hold during sequences
• User specified single or multiple signal sampling clocks
• Data storing and checking during sequences
• Encapsulation for ease of reuse
• Parameterized library of specifications
• Design context specification

The supporting software must provide means for effective debugging of both the assertions and the design / testbench.

The Open Vera Assertion Language (OVA)

The OVA 1.1 language is subdivided into four levels (five in OVA 2.0, which includes LTL formulas).
The first level is Context and is used to define the scope of the assertions, and the sampling time used.  The next level Directives is used to specify what assertions are to be monitored or checked.  The third level consists of Event Expressions that describe temporal sequences in terms of Boolean Expressions that are the fourth and last level.  
Finally, the combination of OVA templates and Verilog wrapper modules provides a flexible encapsulation mechanism.

The above features are best illustrated on in example. Consider the following simple Verilog design:

module counter_8bit(rst, clk, cnt);
input rst, clk;
output [7:0] cnt;
reg    [7:0] counter;

always @(rst or posedge clk)
if (rst)
  counter <= 8'b0;
else
  counter <= counter + 1;

assign cnt = counter;
endmodule

A simple OVA assertion file that checks for an overflow on the 8-bit counter could look like this:

module counter_8bit {    //defines context
 clock negedge (clk) {    //defines clock
    //bool expressions
    bool cnt_00 : (cnt == 8'h00);
    bool cnt_ff : (cnt == 8'hff);
    //simple sequence
    event e_overflow :  cnt_ff #1 cnt_00;
  }
  // directive to signal failure when this
  // sequence occurs (forbid)
  assert a_overflow : forbid(e_overflow);
}

Any Verilog Boolean expression can be used as part of an event specification. The #1 operator is a concatenation of the two operands such that they are one clock cycle apart. Any positive integer interval can be used in this time shift operation.

The forbid directive in the assert statement fails any time the sequence e_overflow is satisfied. An attempt to evaluate the assertion is started at every tick of the sampling clock, i.e., corresponding to an implicit "Globally" top-level operator from the Linear Temporal Logic.

A positive enforcement of an assertion (in opposition to the negative forbid directive) can be obtained by using the directive check:

assert name: check(event_sequence);

In this case, event_sequence must not be satisfied for the assertion to fail in an evaluation attempt. Usually, the positive check is conditional on some Boolean expression (that can also be the outcome of matching some complex sequence of events). Conditional sequences can be written using the operator

if boolean_condition
then sequence
[else sequence] ;

The overflow example can be modified as follows to use a positive conditional check (again the implicit "Globally" operator is present):

module counter_8bit {
  clock negedge (clk) {
    bool cnt_00 : (cnt == 8'h00);
    bool cnt_ff : (cnt == 8'hff);
    event e_overflow :
      if cnt_ff then #1 !cnt_00;
  }
  // directive to signal failure when this
  // sequence does not occur
  assert a_overflow :
    check(e_overflow, "cnt overflow");
}

In this case, when the counter cnt reaches 8'hff (the if part) then on the next falling edge of the clock cnt must not be zero.

Other operators are || (OR), && (AND) of two sequences, repetition *[integer_interval], and constraints on the length or value of an expression while a sequence is in progress.

To facilitate reuse of OVA assertions, complete definitions can be encapsulated in templates. These resemble parameterized macro definitions that can be instantiated in the appropriate scope and passed actual arguments. Their contents can also be accessed from outside the instance that permits using such templates to collect common definitions to other assertions and share them.

For example, the standard OVA template library that is available with the OVA compiler and VCS simulator contains some 34 templates that check simple properties like the overflow above, but also very complex ones such as hand-shake protocols, memories, stack and various fifo's.

For example, a template in the library to verify a similar situation as in our example is defined as:

template overflow(en=1, clk, exp, min, max,
           msg = "assertion triggered") : {
  clock clk {
    event ova_e_overflow :
      (en && (exp >= max)) #1 (exp <= min);
  }
  assert ova_c_overflow :
    forbid(ova_e_overflow, msg);
}

The following instance in a scope specification will achieve the same effect as the expanded check shown earlier:

module counter_8bit {
  overflow(, negedge clk, cnt, 8'hff, 8'h00,
"cnt overflow");
} // Note the use of a default value
  // for the parameter <en>.

To facilitate the use of such templates in designs, they can be directly embedded in the Verilog modules using ova pragmas as shown below:

module counter_8bit(rst, clk, cnt);
input rst, clk;
output [7:0] cnt;
reg    [7:0] counter;
/*ova overflow( , negedge clk, cnt,
      8'hff, 8'h00,
      "cnt overflow"); */
always @(rst or posedge clk)
if (rst)
  counter <= 8'b0;
else
  counter <= counter + 1;

assign cnt = counter;
endmodule

To provide for data checking and other signal value related checks, multi-dimensional variables can also be declared, like in Verilog, and assigned using a non-blocking assignment within a sampling clock context.

Note that all names are bound automatically to the local symbols declared in the OVA code, and then to Verilog objects from the specified scope context. That also includes Verilog module parameters. In this way, the OVA checker is automatically adjusted to the size of the particular instance of the Verilog module. This can be seen in the example following the next section: The bus widths for ad and cbe_ in the OVA checkers are automatically derived from the Verilog signals which are parameterized by bus_w in the Verilog module.

Reusability features
For a checker to be easily reusable it must have the following features:

• Adaptation to a specific instance context and parameterization
• Hierarchical construction and encapsulation to hide internal structure
• User controlled failure message definition

In OVA, the above features are obtained by "template" definitions, Verilog wrapper modules and the above mentioned automatic binding of names to Verilog objects.  Furthermore, `define symbol definitions (like in Verilog) can be used in combination with other compiler directives to configure the checker according to the specific needs.

Verification IP Example
Consider an OVA reusable checker for a PCI Target device.  The top-level definition would be a Verilog wrapper module:

// Interface for Target Device
module SnpsPciOvaTargetInterface(
   clk, rst_, frame_, irdy_, devsel_,
   trdy_, stop_, perr_, par, ad, cbe_,
   idsel );
   parameter bus_w = 32;
   input clk, rst, frame_,
   input irdy_, devsel_, trdy_;
   input stop_, perr_, par; idsel;
   input [bus_w-1:0] ad;
   input [(bus_w/8 -1):0] cbe_;
endmodule

The top-level template for the checker is as follows:

`include "SnpsPci.ovah" //configuration

module SnpsPciOvaTargetInterface {
 // instantiate a template with shared
 // bool, event and var definitions between
 // Master, Target and Arbiter checkers
 // The objects declared within are
 // accessed by other templates using
 // hierarchical names SnpsPci_ObjectName
   SnpsPciBoolsAndEvents SnpsPci (
     .clk( clk), .frame_( frame_),
     .irdy_( irdy_), .ad( ad),
     .cbe_( cbe_), .devsel_( devsel_),
     .trdy_( trdy_), .stop_( stop_),
     .par( par), .perr_( perr_),
     .rst_(rst_)   );
   // Instances of templates that each
   // implements an assertion to check
   // the conformance to a particular rule
   // from the PCI Ref. 2.2 specification
   SnpsPciTP02( .clk( clk));
   // only clock, the other objects are
   // accessed via common template
   SnpsPciTP03( .clk( clk));
   
   … etc.
   
   SnpsPciTP36( .clk( clk));
// optional templates   
`ifdef SnpsPciTP04   
    SnpsPciTP04( .clk( clk));// For 32 bit
`endif
`ifdef SnpsPciTP15
    SnpsPciTP15( .clk( clk),
                 .idsel( idsel));
`endif
`ifdef SnpsPciTP34a
    SnpsPciTP34a( .clk( clk));// For 33 MHz
`endif
`ifdef SnpsPciTP34b
    SnpsPciTP34b( .clk( clk));// For 66 MHz
`endif
`ifdef SnpsPciOvaCompiler
  // do nothing
`else
   SnpsPciTP01a( .clk( clk));
   … etc.
   SnpsPciTP31( .clk( clk));
 `endif
}

The common template has the following structure:

`include "SnpsPci.ovah"
template SnpsPciBoolsAndEvents(
  clk, frame_, irdy_, ad, cbe_,
  devsel_, trdy_, stop_, par,
  perr_, rst_ ) : {
  bool reset_asserted : ( rst_ == 0);
   … etc.
  bool frame_asserted_first :
     (frame_asserted &&
         negedge frame_));
  clock posedge clk {
    event ev_start_of_transfer :
      ( (! frame_asserted) #1
        ( frame_asserted &&
        ( !irdy_asserted)));
    bool start_of_transfer :
      matched ev_start_of_transfer;
       … etc.
    event ev_retry :
      istrue( ( !bus_idle) &&
        ( !trdy_asserted))
          in( start_of_transfer
            # [1..16] ( stop_asserted &&
                       devsel_asserted &&
                       irdy_asserted));
    var [bus_w-1:0] sample_addr;
      init sample_addr = (bus_w-1)'b0;
      sample_addr <=
           (frame_asserted_first) ?
                        ad : sample_addr;
      … etc.
  }
}

Finally, a rule template can be stated as follows:

// SnpsPciTP03 :- Target never aliases
// reserved commands with other commands

template SnpsPciTP03(clk) : {
  clock posedge clk {
   event SnpsPci_ev_CoverageTP03 :
       SnpsPci_start_of_transfer &&
       SnpsPci_reserved_command;
   event SnpsPci_ev_TP03_devsel :
       if( SnpsPci_start_of_transfer &&
           SnpsPci_reserved_command)
       then #1  
         (!SnpsPci_devsel_asserted)*[4];
 }
 assert SnpsPciTP03 : check(
      SnpsPci_ev_TP03_devsel,
      "Target aliases reserved commands");
}

To use an OVA Assertion IP, the following simple steps must be followed:

• Depending on the DUT, select the appropriate subset of Verilog wrapper modules (from Layer 3).
• Instantiate the Verilog module and map its ports to signals in the DUT or on its interface. Do it as many times as needed, e.g., in a system with multiple PCI Target and / or Master devices.
• Compile the entire design files, the Verilog wrapper module files and all the ova files using the appropriate compiler - for simulation or for formal verification.
• Execute, analyze failure / coverage reports, debug, etc.

The essential aspects of the methodology for developing OVA Assertion IP as reflected in the PCI example are described in authoring guidelines.

Guidelines for authoring

The guidelines address the following topics:

• Modeling Strategy

The developer must first extract a set of behavioral properties or rules and possibly companion state machines that describe the protocol. The activity thus involves the extraction and classification of behavioral rules from the protocol specification, elimination of redundant rules, breaking rules into an equivalent set of simpler rules, and grouping into disjoint subsets each covering a specific signal direction. This separation according to signal direction is needed to determine if the rule is to be used as an assertion that has to be verified or as an assumption on the inputs to the design.

• Structure

The OVA Assertion IP is divided into 4 layers:

• Layer 0: The layer contains a "common" template with bools, events, and variables that are shared by multiple rules.
• Layer 1: The layer contains protocol templates, one per behavioral rule.
• Layer 2: The layer contains top level OVA files, associated with the corresponding Verilog wrapper modules (Layer 3) through scope context declaration. There is one such file (and wrapper module) per signals direction, containing an instance of the common template and of the individual protocol templates related to that signal direction.
• Layer 3: The Verilog wrapper modules for OVA assertions covering each signal direction are defined here. There is also an OVA header file with symbol definitions controlling the configuration of rules in the lower layers. For example, the configuration may select a different implementation of a rule (or even its exclusion) depending on the target verification tool - simulation or formal.

• Naming conventions

This part of the guidelines contains recommendation for naming all objects in the OVA Assertion IP with the following objectives:

• Identification with the source of the IP to avoid confusion with other sources (e.g., Snps prefix)
• Identification of the target of the IP (e.g., PCI)
• Identification of the role of the object (e.g., bool, event, var)
• Identification of the function in the specification (e.g., start_of_transfer)

• Coding guidelines

These guidelines represent general suggestions for expressing properties in OVA. They are not specific to assertion IP development, but generally useful recommendations for writing efficient and readable OVA-based checkers.

Applications

The applications of OVA Assertion IP are varied. The most obvious ones are checking of properties of conformance to the bus protocol specification by the device under verification (DUV), either by simulation or by static means.

Other interesting applications are also possible:

• Input assumptions: The subsets of the IP assertions are used to model assumptions on the environment. In simulation, this means that a constrained random testbench is automatically constructed for the particular bus interface, while in a formal tool the proof of assertions is conditioned by the satisfaction of the assumptions by the input sequences.
• Functional coverage: The triggering of assertions can be monitored and thus information on the coverage of the behavioral functions of the DUV can be obtained during simulation. Additional tests can be written to cover the missed functionality. The assertion-based functional coverage can be combined with classical code-based coverage to obtain a detailed picture of how much the DUV has been verified.
• Reactive testbenches: The above functional coverage can be used to construct the so-called reactive testbenches that not only apply valid random sequences but also bias them toward the insufficiently covered areas of the DUV functions.

Conclusions

We have presented:

• The need for assertion IP and its advantages
• The use of the Open Vera Assertion language to build reusable verification IP

The OVA language Version 1.1 is supported by VCS and MX VHDL simulation tool, FormalVera property checker and other 3rd party formal and emulation tools. Further development of the language and tools involves the implementation of OVA 2.x LTL formulas, better library support for OVA IP maintenance, and active development of verification IP.

As universities, in most cases, do not have verification methodology in their curricula, it is important to carry out proper user training in the effective use of assertion-based verification technology, as a powerful complement to the usual techniques.

References

1.    OVA 1.1 User Guide, VCS 7.0 documentation, Synopsys Inc., 2002.
2.    Marcio T Oliviera, Alan J. Hu, "High-Level Specification and Automatic Generation of IP Interface Monitors" Proc. of DAC'02, New Orleans, June 10-14, 2002.
3.    OpenVera Assertion language specification, Version 2.0: http://www.open-vera.com/
4.    Sugar Formal Property Language Reference Manual (Draft), Version 0.8, Accellera Committee, September 12, 2002.