Survey compares formal verification tools

Survey compares formal verification tools
By Lars Philipson, Lunds Tekniska Hogskola, EEdesign
November 30, 2001 (4:31 p.m. EST)
URL: http://www.eetimes.com/story/OEG20011128S0037

Editor's note: This survey of formal property checking and equivalence checking tools was undertaken by Lars Philipson, professor at Lunds Tekniska Hogskola university in Lund, Sweden. It was published in Swedish in the Elektronik i Norden magazine in November 2001. The following English-language version has been made available to EEdesign by Philipson and Elektronik i Norden. Tables following the article, compiled by Philipson, compare features of property checking (also called "model checking") and equivalence checking tools.

The complexity of today's designs has grown to a point were verification is the major bottleneck. Formal verification has arrived just in time to avoid a crisis. By using mathematical methods it is now becoming possible, during certain circumstances, to prove that a design is correct without applying huge sets of test vectors or an elaborate test bench.

The traditional road to verification goes through a time consu ming process of simulation using large sets of input data. Still, because of the astronomical number of possible input sequences, only a tiny fraction of the chip's functionality can be verified in this way. Formal verification is static; it verifies all possible combinations without using a single test vector. It can be compared to static timing analysis, where timing can be analyzed without applying any input signals. Formal verification is static functional analysis. The design is verified against a reference specifying the correct behavior. Obtaining such a reference becomes the remaining challenge.

One reason why verification has become a major issue for deep submicron technologies is that late modifications are often necessary. These may include timing adjustments, test structure insertions, and clock tree modifications. Most of these changes are done more or less manually directly in a gate-level netlist, and may potentially change the behavior of the chip. A re-verification of the netlist is ther efore necessary. This is typically a job for formal verification, and it is done in a matter of hours.

Formal verification comes in two flavors. The first, called equivalence checking, compares one version of the design against another. Typically a gate netlist is compared to an RTL model. In this case the RTL model is used as the golden version that has to be verified separately. This is where the second type of formal verification, model checking or property checking, comes into the picture.

Much of the ordinary behavior of the chip must still be verified by simulation, but most of the difficult cases can be checked by formal verification. Using a separate language, which may be an extension of the RTL language, a set of required properties may be defined. These are typically expressed in the time domain, specifying what is happening during a number of clock cycles involving both state variables and combinational logic. For instance, it may be specified that two bus masters never may be active at t he same time. By using property checking, such a property can be guaranteed to hold at all times.

The theory and algorithms for formal verification have been around at universities for a long time, but only recently commercial tools have become available. An ASIC designer may easily be confused by the terminology used by vendors trying to sell their products, partly because the underlying theory was never part of the engineering curriculum.

Survey of commercial tools
In this survey, all commercially available equivalence checkers and property checkers known to the author are included, subject to the following restrictions.

Only tools specifically addressing hardware verification (not system verification tools, such as the tools from Esterel and Telelogic)

Only commercially available and supported tools

No university or research tools

These selection criteria led to the exclusion of the following borderline cases.

Formal solving engines only (Prover Technolog y)
Not really commercially available (IBM Haifa)
Semiformal tools (e.g. Verisity and 0-In)

Data acquisition was done at the Design Automation Conference in June when appointments were made with specialists from all the vendors for interview and demos. The interviews were based on a pre-established form and all data was entered in a database. Later, all vendors reviewed the data, and all product related information is now made available through this survey.

Overall, 10 companies were identified having in total 4 equivalence checkers and 8 property checkers. The following list shows offerings from the four leading EDA vendors in these areas.

Company

Avant! - Equivalence checker & Property checker
Cadence - Property checker
Mentor - Equivalence checker
Synopsys - Equivalence checker

Then there are a number of smaller companies specializing in formal tools, all established within the last four years. Typically these specialize in property verification. Thus, the big companies have taken over equivalence checking as a mature technology and new start-ups are breaking the ground for property checking. Offerings from smaller companies are shown below.

Company

@HDL - Property checker
Averant - Property checker
Real Intent - Property checker
Valiosys - Property checker
Verplex - Equivalence checker & Property checker
Veritable - Property checker

For this survey, all vendors got the opportunity to quote at the most five strong points of their tools compared to the competitors. It is interesting to note that capacity and performance and ease of use were ranked high by most of the companies. This indicates that these factors are regarded being the most competitive.

Strong Point -- Number of Answers -- Average Rank

Capacity &
performance ------------ 9 ------------- 1.9

Ease of use ------------ 7 ------------- 2.0

Explaining the tables
In the PDF tables below, most of the relevant features of the products are summarized in blocks representing the major aspects of these tools. For instance, in the debugging category, all the different views provided by the tools are listed. Input formats are itemized in three groups: RTL, netlist, and libaries. All tools can take Verilog, nine can also take VHDL and six can take both these languages mixed. When it comes to netlists, four tools accept Spice format after layout netlist extraction. Almost all tools run under both Solaris and HP-UX while Linux comes third.

For property checkers, abilities to support reduction are important. These tools need to reduce the problem in order to reduce run-time without losing the relevance of the result. Sometimes this is done automatically, sometimes in an interactive mode. One type of reduction is decomposition of the design or of the properties. Abstraction means, for instance, that you can use a single line of code to represent a bus. White-box to black-box reduction means that a model of the blocks' behavior at the pins replaces the details of its interior.

Under the user interaction category, features such as cross probing, color coding, and schematic reduction are mentioned, along with the capabilities of saving the session for later completion and speed-up based on earlier runs. This last feature is particularly important for property checkers that may require substantial run times.

For equivalence checkers, capabilities of comparison-point mapping are important. All tools use a range of methods in sequence, such as matching based on names, structure, topology, and function. The user can supply name rules to aid in the process. By using Boolean analysis or ATPG techniques a residue of unmapped points often can be resolved. As a last resort, explicit mapping can be made by hand.

Product Descriptions
@HDL
Brand new property checker from a young company. The tool can generate timing diagrams for properties and switch from property checking to random simulation. It can handle constraint propagation through behavioral RTL constructs and has multiple clock support. It's one of the two tools in the survey that does not state capacity and performance or ease of use as a strong point.

Black Tie
Relatively new property checking tool from a company that has been in the business of equivalence checkers for some time. In addition to user specified properties it also has built-in automatic checks.

ConFormal LEC
This is a mature product with most bells and whistles that you expect from an equivalence checker. It also has integrated transistor extraction for checking of final layout.

Design Verifyer
Equivalence checker that originates from Chrysalis has eight years of consistent performance enhancements. It has been through a large database of customer examples.

Design Verity Check
This property checker is only a year old and still has relatively few of the standard features. The current version only accepts Verilog.

Formal Check
A property checker that originates from Bell Labs, first released in 1997, and by now a mature product. To define properties it uses simulatable component definitions in the HDL library.

Formality
For this equivalence checker the same flow is used for formal verification and for simulation. It is a mature product that supports user defined constraints.

Formal Pro
This equivalence checker is rather straightforward and looks like a mature product even if it is not two years old. It does automatic loop solving.

Formal Model Checker
A property checker using mature technology released in 1997. One of the two tools in the survey that does not state capacity and performance or ease of use as a strong point. Avant! also has two specialized property checkers, One Hot Checker and Clock Domain Checker.

ImPROVE HDL
This very new property checker originates from the University of Caen in France and still lacks most of the usual graphi cal user interface features. It specifies properties and constraints in a single language and also has built-in rules.

Solidify
A property checker with incremental capabilities and built-in rules but relatively little debug support. It uses a Verilog based language for property specification.

Verix
Property checker that for now only supports Verilog and uses simulatable property specifications integrated in the RTL model. It supports hierarchical verification and provides speed-up based on earlier runs.

Click here for PDF table comparing property checking tools.

Click here for PDF table comparing equivalence checking tools.