Design Automation

A formal introduction, please Formal verification simply sounds intimidating. Many digital designers, who already feel stressed to the outer limits with increasing design complexity and impossible schedules, have little time for formalities. Who has time to think about proper specification grammar when it's 10pm and your design won't reset? It all seems so academic.

Formal verification is not just polite command syntax ("please_run 12,000 cycles.thank_you"). Actually, formal verification has nothing to do with simulating clock cycles; and that's the whole point. As designs grow in complexity, we find that ad hoc simulation runs leave more hidden errors unseen. Test vectors are longer but less complete. Formal methods provide a more thorough approach that depends more on the scientific method and less on chance.

In this article we will take a brief look at the concepts behind formal methods, summarize the EDA tools available, and then report on how they have been used in production environments. We will also probe some of the open issues present and take a quick look into the future of formal verification.

Overview of formal verification concepts Let's begin with a quick overview of some concepts and terms used in formal methods before leaping into a discussion of tools (for more in-depth coverage of formal verification theory, see "A Formal Approach" on page 12 of the January 1994 issue of ASIC & EDA ).

Formal verification methods are simply a rigorous, methodical means to prove relationships between two descriptions of behavior. The behavior may be represented in VHDL or Verilog, or it may be described using special purpose languages offering richer constructs for mathematical assertions and properties. Formal methods leverage the current growth of language-based design techniques. Because of this exhaustive analysis, formal tools do not return false positives. However, due to assumptions or missing details in a specification, false negatives and indeterminate results are likely. Formal verification tools are analogous to static timing analysis tools, in that they replace dynamic simulation with mathematics, provide exhaustive analysis in lieu of vectors, and use signal constraints to eliminate pessimism.

Formal verification can be used in three different ways within the design process. First, to verify that a specification of the design satisfies a given set of properties. Second, to formally derive an implementation from the specification (this may loosely be considered a form of behavioral synthesis; see "Behavioral Synthesis: Concept to Silicon," on page 12 of the August 1994 issue of ASIC & EDA). Third, to prove that an existing implementation matches the specification, or to confirm expected differences.

The first usage scenario is supported by a class of tools known as model checkers , which can check whether given properties always hold within a model of the behavior. The second scenario is supported by theorem provers , which use inductive reasoning at each step of decomposition to guarantee a correct by construction implementation for the specification. The third class of tools is called equivalence checkers , because they compare two revisions of the same behavior. As we will see later, some scenarios are less production-ready than others, which are still the exclusive domain of academia.

Figure 1. In all the diagrams, follow the left arc if the variable's value is 0, follow the right arc if it is a 1. For the typed decision graph an arc with a circle indicates inversion of the result from the sub-graph.

Equivalence checkers dominate in today's commercial products. Yet it is important to understand the three distinct levels of checking that have emerged. A combinational checker only proves that equivalent inputs produce equivalent outputs, but does not comprehend the dimension of time (e.g.; clocked memory elements). Strict sequential checkers can prove that equivalent inputs over time will produce equivalent outputs over time, but only if there exists a one-to-one mapping between memory elements in both descriptions (referred to as scheduling). General sequential checkers can prove whether two designs with different internal scheduling will always produce the same results (a very difficult task).

Formal methods also support multiple levels of logic abstraction. Since digital designs are conveniently represented as discrete finite state systems, most formal verifiers need support only Boolean logic. Higher-order logic (HOL), however, can support richer constructs for describing design intent, rather than just hardware implementations. HOL systems generally require much more manual intervention than today's Boolean verifiers.

Symbolic simulation is a means by which formal verifiers analyze logical paths using semantic symbols instead of specific values. One popular algorithm for doing this is called symbolic trajectory evaluation (STE), which evaluates symbolic logic over a path consisting of an arbitrary set of states. The most commonly used internal data representation is the binary decision diagram (BDD). It was quickly found that the size of a BDD is highly dependent on the ordering of the input signals, leading to special ordering algorithms. Later, the size of ordered BDDs (OBDDs) was further reduced by folding common subtrees into a graph form. Typed decision graphs (TDG) improve on the reduced, ordered BDD (ROBDD) by allowing links in the graph to invert the sense of the logic during traversal, enabling better collapsing of subtrees (see Figure 1).

If signal names differ between the I/O of two designs being compared, some form of name mapping is required for comparison. Some tools require manual mapping by the user, while others support automatic cross-mapping of names.

Table 1
Comparison of formal verification tools
Supplier	Tool Name	Class of Tool	HDLs Supt'd	Abstraction	Auto Name Map	Library Supt
Commerical:
Abstract Hardware Ltd.	LAMBDA	Theorem Prover	L2, [VHDL]	Unscheduled RTL	N/A	(Internal)
Chrysalis	Design VERIFYer	Equivalence Chkr	Verilog, [VHDL]	Scheduled RTL	Yes	Verilog
Compass	VFormal	Equivalence Chkr	VHDL	Scheduled RTL	Yes	ASIC (VITAL)
IBM	BoolsEye	Equivalence Chkr	VHDL, Verilog	Scheduled RTL	No	BooleDozer
Universities:
UC Berkeley	HSIS	Model Checker	Verilog, CTL	Scheduled RTL	N/A	--
CMU	SMV	Model Checker	Verilog, CTL	Unscheduled RTL	N/A	--
U. Brit. Col.	HOL-Voss	Model Checker	Verilog	Unscheduled RTL	N/A	--
U. Tx Austin	NQTHM	Theorem Prover	--	--	N/A	--

The task of building canonical data structures is more complex and time consuming than traditional compilation. Fortunately, once these structures exist, actual proof becomes trivial (sometimes being performed in seconds). This is in stark contrast with traditionally long simulation run times, and becomes a cycle time advantage as subsequent verifications are made using pre-compiled reference behaviors.

Commercial tool offerings Over the last few years, a number of commercial products have emerged in the marketplace, many of which are based on techniques and algorithms borrowed from academic research efforts. Table 1 provides a brief summary of available tool offerings.

VFormal, a strict sequential equivalence checker from Compass Design Automation (San Jose, CA), is generally regarded as the first commercially available formal verifier product. VFormal is based on an advanced variation of BDD technology, known as typed decision graphs (TDG). TDGs are coupled with a special subtree pruning algorithm that helps Compass control exponential growth of data structures. "VFormal is really a logical difference engine to compare any two revisions of a design," notes Compass Fellow Erich Marschner. "Think of it as the functional equivalent of 'diff' in Unix." VFormal accepts VHDL-based designs, and recognizes the IEEE-1164 (MVL9) logic type to greatly reduce the computation required. VFormal supports designs described at the behavioral, RTL, or netlist level.

Chrysalis Symbolic Design (Andover, MA) features Design VERIFYer, a formal tool that performs equivalence checks on two revisions of sequential, HDL-based ASIC, or custom IC designs. Design VERIFYer rejects traditional academic research in favor of its own technology, named "symbolic logic"; it does not utilize BDDs for internal representation. Symbolic logic converts designs into algebraic format, then manipulates them according to the rules of algebra to prove assertions of equivalence. "While BDDs explode exponentially with increasing design size, symbolic logic only expands at a slightly greater than linear rate--making it practical to compare complex designs," says Brian O'Neill, director of applications engineering at Chrysalis.

Although Design VERIFYer's algebraic approach resembles that of theorem provers, it is not as general purpose in its handling of arbitrary cases. This limitation in scope is key in rendering this class of problem solvable, and eliminates the need for constructing proofs. Design VERIFYer compiles ASIC libraries directly from source code along with the design, or uses compiled versions once available. Designs may be described in either Verilog or, starting sometime after April, VHDL.

BoolsEye, from IBM Microelectronics (Hopewell Junction, NY), started its history nearly 20 years ago as a mainframe-based application for Boolean equivalence checking. Recently migrated to the workstation, BoolsEye runs as part of the BooleDozer synthesis framework. It builds logic cones for combinational functions bounded by memory elements, then compares them across design revisions. BoolsEye supports stuck-at faults and post-scan insertion comparison. Both VHDL and Verilog are supported at the RTL, gate, and transistor level, with library support based on "S rules" (also used with IBM's BooleDozer). Name mapping is done manually. BoolsEye is currently available only for IBM ASIC customers, following a recent distribution channel shake-up. IBM's external sales strategy is still pending.

LAMBDA is the product of Abstract Hardware (Uxbridge, Middlesex, England), a Viewlogic subsidiary. It expands a specification down to RTL or gates while a rule-driven theorem prover ensures correctness at each step. LAMBDA splits a specification into two parts: tasks which have been designed, and tasks which remain to be designed. As the user instantiates elements, more of the (partial) design can be proven to match the original specification. The input language, L2, is a high-order language that supports Predicate Logic Calculus. Users add graphical components to a schematic window while the theorem prover works in background. For each component, a formal rule defines exactly how it can be applied. LAMBDA supports model checking, such as whether certain assertions are valid in the specification. The prover includes hundreds of (user-extensible) rules, including design rule checks.

University research tools Formal verification methods have been a popular research topic for many years. Much of the university research is funded through the Semiconductor Research Corporation (SRC) and federal government grants, with additional research occurring at major corporations (often in tandem with academic efforts). Numerous SRC member companies, for example, work directly with university software to refine the algorithms and explore suitable design methodologies. Just as prior academic research paved the way for today's formal verification products, current research is addressing more generalized verification that may foreshadow a new class of formal verification products a few years ahead.

HSIS is a prototype model checking system available from the University of California at Berkeley. With HSIS, the design (along with its environment) is input using Verilog; a set of properties to be checked are described using either Verilog or computation tree logic (CTL). The properties are augmented by a set of fairness constraints that serve to either include or exclude certain behaviors of the description, and are written separately. UC Berkeley is working on methods of abstraction to help manage state explosion, such as reducing a wide bus to just a few bits, use of hierarchy and partitioning, or replacing a description with one containing fewer constraints ("conservative non-determinism"). HSIS attempts to properly order BDD inputs, but manual re-ordering may also be required to control state explosion.

SMV is a model checker resulting from pioneering work done at Carnegie-Mellon University (CMU, Pittsburgh, PA). The SMV system uses CTL to describe the specification and properties to be checked, and supports general sequential behavior. It is ideal for describing and validating concurrency, such as bus protocols. SMV uses ROBDD technology, which was developed at CMU. While SMV does support RTL level designs, it generally performs better at lower levels of description. CMU is now extending SMV to support bounding algorithms, such as constraints on delay or a maximum number of events per time interval. This can be useful in predicting response time, system loading, or other critical design goals. CMU is also working on a VHDL compiler for SMV.

The University of Texas at Austin has developed the NQTHM theorem prover, more commonly named the Boyer-Moore system. This tool is based on a decidedly semantic view of VHDL, which it uses to advantage in reasoning about valid implementation mapping choices. This theorem prover is relatively automatic, which compensates for its less intuitive manual interaction. UT's work in Boyer-Moore logic has resulted in a spin-off company in Austin, Computation Logic, that is using the same approach.

Figure 2. Formal verification products can be used across multiple portions of existing design flows.

One of the most intriguing approaches is in work at the University of British Columbia, where symbolic trajectory evaluation and theorem proving techniques are combined to produce a model checker, named the Voss Prover, that is especially well-suited for validating data flows. Built on the earlier HOL-Voss hybrid, it has evolved into a framework for managing proofs. The key is a specialized theorem prover that can segment a large design into smaller pieces for STE-based evaluation and re-integrate the results, without the need to take the circuit apart. The BDD-based technology accepts large SPICE netlists or behavioral VHDL, since the complexity is solely a function of the properties to be checked, not circuit size. Extensions are underway to enlarge the subset of VHDL supported.

Putting formal methods to work With the preceding discussion as a backdrop, let's tackle the most important question: are these new tools up to the challenges of industrial use? To answer this question, we will have to examine how they fit within existing design flows (see Figure 2), and what some companies have found from their experiences.

Fitting Into Corporate Flows . There are many ways to use today's equivalence checking tools within existing design flows, such as pre/post-synthesis (RTL to gate), pre/post-technology mapping (gate to gate), pre/post test insertion (gate to gate), pre/post library re-targeting (gate to gate), retroactive updates to RTL model (gate to RTL), etc.

When using a model checker, your design will be tested for specific properties, rather being compared with another design. Design flow options include behavioral-level specification validation, RTL-level description validation (against same properties), post-synthesis validation (against same properties), and post-layout validation (against same properties).

The common belief that formal verifiers cannot handle full, complex ICs is only partly true. While full-chip RTL vs. gate comparisons are rare, numerous examples abound of gate vs. gate verification in the range of 200k to over 500k logic gates. However, tools that support unscheduled RTL verification are not yet able to handle even medium-large industrial designs. Once this is possible, it will leverage with behavioral synthesis technology to help both gain further acceptance.

Equivalence checkers adapt most easily into legacy design flows. Theorem provers and model checkers require specialized training in HOL languages, and require more fundamental changes to design flows. However, these changes also have the greatest potential impact on design quality and productivity.

Why formal verification is ready for commercial use

by Brian O'Neill Director of Applications Engineering, Chrysalis Symbolic Design, Inc. The best way to tell that a technology is ready for use is to find out whether the new approach is succeeding in production environments. Design VERIFYer is currently working on real projects at several customer sites. A workstation manufacturer is designing seven ASICs ranging in size from 40k-126k gates. After designing each chip using Verilog, RTL simulation, and synthesis, the designers use emulation to verify that the chips play together in the system. They use Design VERIFYer to make sure downstream changes, such as insertion of test logic and physical layout, do not alter the logic functions of each chip. A large-scale computer maker is verifying designs over 400k gates. The revisions being verified include clock-tree synthesis, adding testability by changing edge-triggered flip-flops to LSSD cells, and layout. Design VERIFYer reads existing Verilog libraries, netlists, and synthesizable design descriptions, thus smoothing integration into industrial flow.

Industrial Strength? There are countless examples where equivalence checkers have been used in industry (see the sidebar). For instance, the SMV system has been used successfully to verify the cache coherence protocol of the Encore GigaMax multiprocessor and Futurebus+ protocol. Major corporations like AT&T (Murray Hill, NJ), Convex (Richardson, TX), Digital Equipment (Marlboro, MA), Intel (Folsom, CA), and Motorola (Mesa, AZ) have been working with formal verification technology for years, both in production design work and in prototyping of their methodologies. European firms like Bull (Les Clayes-Sous-Bois, France), Philips (Eindhoven, the Netherlands), SGS-Thomson (Agrati Brianza, Italy), and Siemens (Frankfurt, Germany) as well as several Japanese companies, have been actively involved with the technology on numerous real designs.

IBM may well be the first to realize the significance of the technology. IBM has used formal methods in the design of a broad line of products, including the 3081 mainframe (1977), the 3090 mainframe (1982), and the Enterprise 9000 series mainframe computers (1990). "We have used formal methods to verify entire chips in the range of 200k to 500k logic gates," observes David Lackey, senior engineer at IBM Microelectronics. "We formally verified our thermal conduction module, which is an MCM consisting of about 100 chips." Other industry contacts report similar results: a five-day simulation is reduced to a 40 minute verification; a large design consisting of 1030 states is verified "in minutes"; and a complete post-synthesis IC is proved in 35 seconds, following a two-hour compilation.

A Shift in Design Paradigms? Formal verification doesn't necessarily require a shift in design paradigms to be useful today. However, the maximum benefit will generally be found when the tools and new methodologies supporting them are integrated into the entire design process, rather than just as an after-the-fact check. Once the tools are in place using current flows, new ways to take advantage of this technology should be explored. The benefits of discovering new design paradigms will be long-lasting, since those who have mastered equivalence checking will be at an advantage when the next generation of formal verification products appear.

Open issues in formal verification While the data above is certainly encouraging, several points should be considered. First, the methodologies are still evolving; it will require years before EDA vendors and users know how to best use these tools across the full spectrum of design applications. Second, each tool has its own set of quirks and limitations, and understanding these in advance is the best way to avoid surprises downstream. Production usage today is most commonly performed between revisions of post-synthesis (netlist) designs, with less experience at the RTL level. Also, designs that exceed the practical limit of 2200 states are likely to overflow available memory, disk, or CPU time; abstraction techniques may become essential. Third, although many tools offer automatic signal name mapping, the mapping process may take longer than the verification process, implying more care in signal naming conventions. Fourth, typical specifications are often incomplete, make implicit assumptions, or over-specify the design requirements. All of these factors can affect the results from formal tools that use them directly, which many hope will lead to more rigorous design specifications.

Formal forecasting Looking ahead, experts generally agree that there will continue to be increasing use of strict sequential equivalence checkers, with a commensurate growth in optimization as vendors and researchers understand what really matters to designers (and what does not). Many also see the introduction of general sequential verifiers within the next three years, and its natural synergy with behavioral synthesis. In addition, look to see more of today's traditional tools adapted to utilize formal methods (synthesis, test, timing analysis). A little further out, expect to see model checking mature, both as a tool technology and as a design methodology.

There is considerable disagreement over the future of high-order logic theorem provers. Proponents point to the increased focus on system behavior and ability to apply it to RTL level design. Critics argue that other formal technologies are more practical for digital designs, and that the gap from current practices to mathematical specification syntax is generally too wide.

Formal methods have already proven themselves, and have a bright future in electronic design automation. Today's commercial equivalence checking tools, leveraging from academic contributions and industry partnerships, are sufficiently robust to deliver value-added capabilities across a broad range of applications. Although proper training and preparation remain important factors in taking best advantage of the technology, most can fit smoothly into existing design flows. Perhaps a few formalities are in order, after all.

Contributing editor Steve Schulz is a member of the technical staff in Texas Instruments' Semiconductor Group.

integrated system design  April 1995