VHDL is a critical language for RTL design and is a major component of the $200+ million RTL simulation market¹. Many users prefer VHDL for RTL design because the language continues to provide desired characteristics in design safety, flexibility and maintainability. VHDL users have never worried about simulation mismatches caused by race conditions, nor have they had to re-write finite-state machines due to changes in the state encoding. VHDL's strong typing provides a fundamental level of assertion-based verification, as a type declaration defines certain properties about object values that can be checked during simulation.

VHDL has provided significant value for designers since 1987, but has had only one significant language revision in 1993. The state of design practice has caught up to and, in some cases, surpassed the capabilities in VHDL. Last year, the VHDL Analysis and Standardization Group (VASG) received indication from the VHDL community that it was time to enhance VHDL.

In response to the user community, VASG initiated the VHDL-200x project. VHDL-200x will result in at least two revisions of the VHDL standard. The first revision is planned to be completed next year (2004) and will include a C language interface (VHPI), a set of high user-value enhancements to improve designer productivity, and modeling capability and verification enhancements. A second revision will follow about 2 years later. The verification enhancements will provide the basis for significant improvements in design verification productivity and are the focus of this article.

Assertion-based verification

Assertion-based verification improves verification efficiency by adding behavioral specifications to a design. These specifications define requirements on design behavior that can be checked statically, using formal verification techniques, and dynamically, during simulation. They define intended design behavior, which should be demonstrated during verification, and error situations, which should not occur during verification. They provide visibility into the internal state of a design.

Two types of behavior specifications are involved: assertions, which define correct behavior or represent error conditions, and coverage monitors, which detect the occurrence of interesting behavior. Assertions, as shown in figure 1, detect errors at or near the source — in this example, "cas" failing to remain high during a refresh cycle.

Early detection facilitates debug compared to traditional black-box simulation that detects errors if and when they propagate to a primary output. In figure 1, the testbench detects an error many cycles later after the result of various operations on the corrupted data propagate to an output or register state observed by the testbench. Coverage monitors detect intended conditions or behavior patterns that occur in the system and record that information for functional coverage analysis.

Assertions help ensure interface specifications are captured along with the design. For IP, embedded assertions are delivered as part of the IP for use in verifying correct integration of the IP into the system. The designer's assumptions and decisions about the implementation can be captured as assertions, to improve maintainability and reusability. Coverage monitors document significant corner cases to be tested, and transmit design knowledge directly into the verification process improving verification productivity.

Property Specification Language (PSL)

Accellera devoted significant time and resources to develop a standard language for assertion-based verification. PSL version 1.01 was adopted as an Accellera standard in May 2003. PSL supports various styles of behavioral specification, including Linear Time Logic (LTL), Regular Expression, and Computation Tree Logic (CTL). This variety supports formal verification and simulation. The language identifies a subset that is suited for verification flows in which both simulation and formal verification work together. The Simple Subset consists of behavioral specifications in which time advances monotonically.

PSL in VHDL

Using PSL with VHDL is possible today in the form of pragmas, or structured comments, that begin with the string "—psl". But a better solution would be to add PSL declarations and statements to VHDL as first-class language constructs. In VHDL-200x, the Simple Subset of PSL will be integrated as part of VHDL.

VHDL has had assertion statements since 1987, so assertions are not new to VHDL. However, the existing VHDL assertion statements only express combinational invariants — properties defined in terms of simple Boolean expressions. PSL provides an opportunity to extend the definition of assertions to include the ability to describe sequential behavior. This dramatically increases the utility of VHDL assertions for both simulation and formal verification applications. Similarly, supporting the PSL cover directive in VHDL allows native support for coverage monitoring.

PSL enhanced assertions provide native assertion-based verification support for VHDL users. Users could specify powerful properties and assertions:

1. Unclocked, combinational invariants that prohibit/detect glitches in asynchronous control inputs.

2. Clocked, combinational invariants that check relationships among synchronous control inputs.

3. Singly-clocked, sequential assertions that describe paths through a state machine or interactions among state machines that have the same clock.

4. Multiply-clocked, sequential assertions that describe interactions between clock domains.

5. Express sequences of control conditions that make up a behavior pattern, together with various forms of implication operators.

This code says that, once a read transaction has started (a request followed by an acknowledge, with read/write bar high all the while), then it must complete (with data ready asserted after 1 to 3 cycles while read/write bar stays high, and then request is deasserted, and then acknowledge is deasserted).

6. Cover directives, which can use sequential regular expressions (or sequences), describe behavior patterns that should be observed sometime during the verification flow. For example, a coverage monitor for the read transaction mentioned above might be expressed as follows:

Enhancements to the new VHDL programming interface (VHPI) allow 3rd party tools and user created utilities to query the state and statistics of PSL assertions and cover directives. These enhancements also allow control of assertions in terms of enabling, disabling, stopping or halting simulation.

In addition to incorporating the simple subset of PSL, current language restrictions will be relaxed to help facilitate the deployment of assertion-based verification. For example, the driving value of OUT mode ports will be readable within the design or assertion code and IN mode ports can be associated with expressions that are re-evaluated whenever there is an event on a signal referenced in the expression.

Testbench and verification

Today many users resort to high-level verification languages to facilitate testbench construction and verification. However, the same users have stated that it would be easier and preferable for design and verification support to reside in a single language.

A number of areas have been identified to help improve testbench writing and verification with VHDL:

• Associative arrays
• Dynamic processes
• Queues
• FIFOs
• Lists
• Synchronization and handshaking (event objects)
• Request and wait for action
• Expected value detectors
• Access to coverage data for reactive TB
• Sparse arrays
• Random value generation with optional and dynamic weighting
• Random object initialization
• Random 2-state value resolution
• Loading and dumping memories

Associative arrays

Associative arrays allow indexing of data based on any arbitrary type. Figure 2 shows that, unlike regular arrays, associative arrays can be sparse as each index need not have an associated value.

The following is an example of how an associative array would be declared in VHDL:

Operations are predefined for associative array elements including: deleting, checking existence of, returning the number of, getting the first, next, last or previous. Also, dumping and loading an associative array is supported.

Lists

Lists are used to collect related data. Lists have a head and a tail and zero or more elements between. The order of the elements in the list depends on the application. A first-in, first-out order mimics the functionality of a FIFO. Alternatively, the data can be sorted on a key. The following is an example of lists.

A number of predefined list operations are provided. These include delete, insert, length, sort, unique, reverse, exists, and index.

The working group is evaluating a proposal for adding type genericity that could impact the implementation of associative arrays and lists. Type genericity is analogous to template classes in C++² and type generics in Ada³. With parameterization on types, abstract data types (such as associative arrays and lists) would be defined in packages as "parameterized" types with associated operations. In addition to abstract data types, type generics can be exploited to define more general and reusable design blocks.

Dynamic processes

Two proposals for dynamically creating concurrent processes (threads of sequential statements) are being evaluated. The first is the well-known fork-join statement. The fork-join construct defines the concept of a sequential block that is a sequential statement. Each sequential block within a fork-join is executed concurrently with each other. Sequential statement execution proceeds when the fork-join reaches the end condition specified.

The second proposal would introduce dynamic, declared processes to VHDL. This proposal is based on work from the SUAVE project. Under this proposal, processes would be declared similar to the declaration of a subprogram. They could then be activated (multiple active instances would be possible) and terminated dynamically. It is possible that both proposals may be adopted.

Hierarchical signal access

Although strict scope and visibility rules provide maintainability and reusability benefits, they also hinder white-box testing and stimulating techniques. As a result, simulator vendors have created their own proprietary packages containing signal probing and forcing functions. A standard package of probing and forcing functionality will be derived from technology donations already received.

Formatted IO: hwrite, hread, owrite, oread, to_string, to_hstring, to_ostring

The addition of over-loadable, standard routines to write or read formatted values such as hexadecimal or octal will reduce I/O while allowing input and output values that are easier to read and maintain. Additional functions will be provided to convert values into formatted strings to be used with I/O or assertion messages.

Just the tip of the iceberg

Although we have focused on the verification enhancements in the first revision, many additional enhancements are in process or planned for VHDL-200x. Language changes to improve tool, especially simulation, performance will improve verification productivity. The importance of design productivity is reflected in enhancements to reduce coding, raise abstraction levels and facilitate more modeling styles, such as asynchronous designs. When the VHDL-200x project is completed, VHDL will retain its leadership at the forefront of advanced design and verification languages while improving designer, verification engineer and tool productivity.

Acknowledgements

The following people contributed to this article and are providing leadership in the VHDL-200x effort: Eric Marschner of Cadence, Jim Lewis of SynthWorks, J. Bhasker of eSilicon and Peter Ashenden of Ashenden Design.

Stephen Bailey chairs the IEEE 1076 (VHDL Analysis and Standardization) working group. His EDA career has taken him in many directions, from writing code that implements simulators to applications engineering and marketing. As a technical marketing engineer at Model Technology, he values the close customer interaction as it provides great insight for enhancing languages as well as EDA tools. Prior to joining the EDA industry, he developed embedded software systems and software design tools after receiving his BS and MS in computer science.

References

1 Gartner Dataquest 2002 EDA Forecast, CAE, RTL Simulation Market Forecast
2 Programming Languages -- C++, INCITS/ISO/IEC 14882, American National Standard (INCITS-Adopted ISO/IEC Standard), 15 Sep 1998.
3 Information Technology -- Programming Langauges -- Ada, INCITS/ISO/IEC 8652, American National Standard (INCITS-Adopted ISO/IEC Standard), 1 May 1995.