Formal Verification of a Large Design

Design overview The CM10 processor is being developed by the PPG Division of
the Chameleon Project at SGS Thomson Microelectronics. The Chameleon team consists of approximately 60 design engineers and 10 verification specialists. In creating the CM10, the team adopted a design flow with four tiers of abstraction:

Currently, there is no formal verification tool that can compare level 0 C models to level 1 VHDL RTL models. Thus, the level 0 specification is simulated thoroughly to ensure correct design intent. Thereafter, formal verification is used as often in the design flow as possible (Figure 1).

Figure 1. In creating the CM10, the Chameleon team adopted a four-tier design flow using both sequential and combinational verification techniques.

Formal verification vs. simulation In traditional simulation-based verification, a design must be compared against its original specification. To make this comparison, a designer has to create a complete set of test vectors to represent all possible inputs to the design and then verify that the resulting outputs are valid. Thus, in a simulation-based verification scheme, a known "golden" set of test vectors is the standard against which the design implementation and any changes are compared. Any functionality missed by the vectors can cause the simulation to miss errors.

Often the design specification is written in a language such as C, behavioral or RTL-level VHDL. The final implementation is often a netlist. To use simulation to verify that the netlist meets the design specification, both descriptions are compiled into simulation models. The golden test vector set is applied to both as stimuli and the resulting outputs are compared. More errors can be missed at this stage because the simulation results are compared and then interpreted to find any bugs in the netlist.

In contrast to simulation, formal verification uses rigorous mathematical methods to prove that two design descriptions are equivalent for all possible sets of inputs. The process involves no test vectors, and designers do not need to interpret results. If the design descriptions are not equivalent, the formal verification tool states exactly how they differ. For these reasons, formal verification offers an easier and more effective way to accomplish many tasks that were previously handled by simulation.

Practically all formal verification starts in much the same way as simulation­by using a compilation stage. The main difference is that the designs being compared are stored as binary decision diagrams (BDDs) for formal verification. BDDs represent the complete logical functionality of the circuit (Figure 2).

Figure 2. This is an example of a binary decision diagram that would be formed for this simple
VHDL or schematic description. By tracing the branches of this binary tree, it is easy to see that
this BDD contains all the information necessary to represent the full functionality of this VHDL
circuit. By using BDDs, rigorous proofs are possible.

The toolset The Chameleon team uses VFormal from COMPASS Design Automation (San Jose, CA) as its primary formal verification tool. The design flow also includes three tools developed by the Chameleon team. Two of the tools, Shadauc and Winnow, were developed in collaboration with COMPASS. They operate on the finite state machine descriptions drawn from the design by VFormal. The third Chameleon-developed tool, Laybool, abstracts structural VHDL descriptions from SPICE-like transistor netlists using the same logical parts library as VFormal.

The way the tools are used depends on the hierarchical levels involved as well as the nature of the block that is being verified. Chameleon designers use formal verification to check the sequential properties of the level 1 RTL specification and to perform combinational checking between level 1 and the level 2 structural implementation.

Once a level 1 RTL specification is created, a combination of VFormal, Shadauc, and Winnow check the validity of the design's sequential properties. By checking in this manner, designers can verify the logical intent of the original design­a process that can even reveal changes that are necessary in the level 1 design.

Combinational verification shows that the level 1 specification matches the level 2 implementation. The technology used for implementation affects the way the verification tools are used. High-performance level 1 blocks must be implemented using full-custom or semi-custom layout techniques. If performance is not critical, straight datapath or standard cell synthesis can be used. If synthesis is used, a structural VHDL description (level 2) can be obtained directly from the synthesis tool.

In the cases of blocks that require custom layout, designers use the internal SGS logical abstraction tool Laybool to convert a transistor-level netlist into a logical dataflow VHDL description (level 2). VFormal is then used to combinationally prove that the level 2 implementations match their level 1 specifications. Using this flow makes formal verification in a mixed methodology possible; thus, custom and synthesis-based blocks can be verified in the same manner.

VFormal The Chameleon designers' success with formal verification, in the Transputer project and with VFormal at Bull in France, led the team to choose this product as the primary formal verification tool for the CM10 processor. VFormal was easy to integrate with the rest of the Chameleon design flow and freed internal tool developers to work on other verification tools.

VFormal uses the same information provided by BDDs. However, the tool employs a more compact representation of BDDs called a Typed Decision Graph (TDG). The TDG is more compact because it takes advantage of some of the redundancy found in BDDs. For VFormal, the initial compilation step is finite state machine compilation (FSMC), in which state machine and combinational logic information is extracted from the design.

Once both design representations are in TDG form, VFormal generates a command file containing all the relationships that must be proven to guarantee that both circuits are functionally equivalent. Then VFormal compares both TDGs under the guidance of the command file and reports whether the two designs are functionally equivalent. If they are not equivalent, VFormal gives the exact location of the functional problem that needs to be fixed.

Because VFormal is based upon BDD technology, the tool can handle blocks of roughly 25K gates or fewer­the same complexity boundary encountered in BDD-based synthesis tools. However, like most designers, the Chameleon team uses a synthesis-based "divide and conquer" strategy, so logical complexity is not often an issue. There are even workarounds for full-parallel flash multipliers. Although designers more commonly use pipelined multipliers, full-parallel flash multipliers can also be handled by exploiting scalability­proving one of lesser width, then extrapolating the results for larger widths.

Formal verification

This definition of formal verification has two key words: rigorous and proof. The term rigorous implies a complete and thorough understanding of the logical composition. The term proof implies that there are no conditions left unchecked. When we prove something, we have left no doubts as to its validity. This is the true goal of formal verification, to leave no stone unturned when searching for possible bugs or errors.

Winnow and Shadauc The Chameleon group's in-house Winnow and Shadauc supplemental routines allow the team to do sequential verification­logical verification based upon the order of events. In a traffic light controller, for example, is it possible under any circumstances for the green lights in different directions to be on simultaneously? This sort of property-checking question is answered by using the combination of Winnow, Shadauc, and VFormal.

Winnow helps make sequential verification problems tractable by narrowing the scope of the proof (based upon using a realistic smaller set of actual possible inputs or operating conditions). Otherwise, some properties would require infinite computer resources to check. Winnow reduces the complexity of the finite state machine descriptions as much as 80 percent.

The Chameleon team uses Shadauc to check whether the finite state machine possesses the desired sequential properties. Shadauc uses two methods for finite state machine transversal: transition relation and transition function. The Chameleon team plans to integrate these methods into Winnow in the future for higher performance. At present, Shadauc can handle about twice as many state variables as SMV, a pioneering public-domain sequential verification tool developed at Carnegie-Mellon University (CMU) in Pittsburgh, PA.

SMV has also been used by the Chameleon team with sequential verifications where VHDL has limitations as a specification language, but primarily SMV was used to prove that the Winnow/Shadauc methodology is valid. SMV uses only one method of finite state machine transversal­transition relation­but SMV uses sophisticated state reordering and cache management techniques. The main drawback of SMV is its status as a university tool; there is no one to make bug fixes when needed. For this reason alone, Shadauc and Winnow are preferable, and they are therefore replacing SMV in the Chameleon design flow.

Figure 3. This is an example transistor-level abstraction performed by Laybool. The abstracted VHDL
description is in dataflow or continuous signal assignment form. VFormal can accept and use this description to compare against the original RTL specification.

Laybool Analysis of transistor networks can be exceedingly difficult (Figure 3). For instance, sequential elements such as latches can be highly complex. Using design rule knowledge can greatly speed the abstraction process, but then the abstraction is heavily dependent on technology. For these reasons, the Chameleon team chose to implement its own transistor-to-logic
abstraction tool.

This tool, called Laybool, is based on work done by Randal E. Bryant and associates of CMU (on the COSMOS system). Working from the same BDD library used by VFormal to represent logical functionality, Laybool abstracts a structural VHDL description from a SPICE-like transistor CDL netlist. The abstracted VHDL consists of continuous signal assignment statements that can be used to prove implementations against an original RTL specification.

Laybool can recognize precharge conditions, handle pass-gate logic, and provide some degree of bi-directional port capability. Because Laybool currently has difficulty recognizing cache RAM, the Chameleon team is considering pattern matching as an alternative. Additionally, Laybool needs to be upgraded to accommodate latches with scan inside the feedback loop and better handling of bidirectional ports.

Sequential verification The CM10 bus and some of the cache structures were so complex that verification by simulation would have been nearly impossible. Since formal verification has complete coverage by definition, these complex blocks can be thoroughly tested without the need to run exhaustive test vectors (Figure 4).

Figure 4. The sequential flow is used to prove properties
with respect to the ordering or sequence of events.

---

As mentioned earlier, different properties were verified in different ways. One of the design's combinational assertions (Grant_snd) was written in VHDL and checked with VFormal alone. Another sequential assertion (Ack_rcv, Valid_rcv) was also written in VHDL and involved VFormal as well as Chameleon's Shadauc and Winnow routines. Yet another sequential property (Req_snd) could not be expressed as a VHDL assertion because the property depended on specific state sequences. Thus, this property had to be written in CTL (the language accepted by SMV) and checked by using SMV, Winnow, and VFormal. In all cases, VFormal was used to create the BDD database (finite state machine) file used by the verification tools.

The CM10 bus was exhaustively formally verified against a complete specification of six sequential properties. Five out of the six properties were checked using a combination of VFormal, Winnow, Shadauc, and SMV. The sixth property was verified using simulation. In the five properties verified using sequential verification, four proved to be true and one false. In the property found to be false, VFormal found that the bus could remain locked up for a transaction that never happened. This bug was fixed by the design team.

Sequential verification has both advantages and disadvantages. One major advantage is that designs can be revised and tested early and thoroughly at the RTL level before implementation has begun. Sequential verification is also fully exhaustive and covers all possible input patterns. The biggest drawback is that it often requires large computational resources. Even so, formal verification's demands are always lower than exhaustive simulation.

Figure 5. Combinational verification is used to prove that the
custom layout is functionally equivalent to its RTL specification.

---

Combinational verification In the Chameleon flow, combinational verification is used to compare level 2 structural VHDL against level 1 RTL VHDL (Figure 5). From the layout database, Dracula extracts a CDL netlist, and Laybool automatically recognizes and extracts logical functions by understanding the CMOS transistor-level netlists. Once the logical abstraction is done, VFormal proves level 1 against level 2. For some blocks in which the logical complexity is overwhelming, hardware acceleration is used in place of formal verification. The output of Laybool is also acceptable to an external emulator, which is useful to test the instruction set of the CM10 and to develop software routines.

The following is an example of a block that was verified combinationally by VFormal alone. For a 64-bit parallel adder, VFormal's finite state machine compilation extraction time was roughly 15 minutes. The time taken to create the proof command file was 10 minutes. The actual time needed to prove equivalence of level 1 with level 2 was 4 minutes, and the proof was successful in proving that there were no discrepancies between the two descriptions.

A versatile verification strategy The Chameleon team used a variety of approaches to formally verify the equivalence of the CM10 processor design descriptions at multiple levels, without the overhead of exhaustive simulation. Winnow's problem reduction capability, Shadauc's logical comparison capability, and VFormal's ability to work with outside tools combined to give the Chameleon team wide-ranging verification resources. These tools provided the ability to check sequential properties of circuits, thereby allowing the team to exhaustively verify some of their original RTL design specifications. Finally, the logical abstraction capability of Laybool enabled the team to use the same formal verification methodology for both custom and synthesis-based blocks (mixed methodology).

Dino Caporossi is the product manager for VFormal, COMPASS Design Automation's formal verification product. He previously designed advanced prototype ASICs, ICs, and circuit boards for DSP systems in a variety of DOD and non-defense-related applications.

Geoff Barrett of SGS-Thomson Microelectronics Ltd. is a consultant verification engineer managing the development of internal formal verification tools for the Chameleon project.

To voice an opinion on this or any Integrated System Design article, please e-mail your message to michael@asic.com.

integrated system design  January 1996