System Design

A Set of Formal Applications

Stratus Computer puts formal equivalence checking to work on a multiple ASIC computer system.

by Shawn Clayton, John Sweeney, Mark Tetreault, and Scott Sandler

Practical methodologies for using new EDA technologies emerge when engineers apply tools to real-world design problems. Stratus Computer Inc. (Marlboro, MA) has developed a verification process that uses formal equivalence checking to greatly reduce gate-level simulation in the ASIC development cycle. Using this technique increases our confidence that our released designs are functionally correct and at the same it saves precious verification time.

Stratus' methodology Design VERIFYer software from Chrysalis Symbolic Design Inc. (Billerica, MA) lets us check, with 100 percent certainty, whether a design implementation or revision is functionally equivalent to the "golden" version. We use the full range of equivalence checking capabilities, which include comparing one RTL model with another, comparing gate-level netlists with verified RTL models, comparing changed RTL models with gates that we know work, and comparing one gate-level model with another.

Figure 1 shows our design process. We code our design in Verilog RTL and simulate extensively to show that these models capture the intended functionality. Once we sign off this model, we have a reference that we can use for equivalence checking to verify the subsequent implementation and refinement steps. The limitation is that the set of "state points" must be the same between the two versions to be compared (see "Overview of equivalence checking"). If we make the kind of change that re-encodes a state machine or otherwise changes the set of registers and latches in the design, we need to re-validate the reference model with simulation (see Table 1 for a breakdown of the time and memory needed to perform an RTL to gate comparison).

RTL applications In practice, we rarely find differences between the RTL and the synthesized gates, just as simulation rarely finds errors here. But the differences we do find are easier to pinpoint with formal verification. These differences are typically caused by user errors in entering the RTL or in setting synthesis parameters. Just one such error could sink a design, so we consider this a crucial verification step.

Figure 1. Insertion of formal equivalence checking replaces simulation for functional verification.

In one case, the equivalence checker reported that the gates for a module were not functionally equivalent to the RTL, but it was not immediately obvious why. Examining the Verilog did not reveal the reason. Simulation confirmed that there was a difference, but not why. Given enough interactive simulation time, we could have tracked down the problem, but we found a way to use the equivalence checker to do the job faster.

The designer of this block suspected that the difference originated with a case statement. In the course of an afternoon, he was able to revise his RTL, synthesize, and verify the gates several times with formal verification. What he found was that he had used the full-case directive but did not specify all of the conditions in the case statement. This kind of subtle combination can take days to figure out. Simulation of the RTL had not uncovered the problem because simulation doesn't pay attention to the "full case" intent. The simulator and the designer interpreted the RTL one way, but the synthesis tool interpreted it differently. Formal verification revealed the error and helped us to quickly determine the cause.

Figure 2. Stratus used this method of continuous verification after each netlist change to arduously avoid gate-level simulation.

We also use formal verification to compare one RTL model with another. The introduction of "mode bits" is the type of design step where this comparison can be useful. The basic functionality of the design may be well tested and robust, but late design changes may introduce additional "modes." These changes are only intended to add new functions, not to modify the existing functionality. Rather than exhaustively simulate the old functionality to make sure that it has not been altered, we use dynamic constraints and RTL comparisons to prove that the already-verified functionality remains intact with the "mode" set in a given way. This lets us focus additional simulation on verifying the new functions, instead of re-verifying the old.

Gate-level applications When an implementation of the entire chip is functionally complete and all the modules have been verified, we must still make changes to the netlist for a variety of reasons. Timing issues must be resolved, clock logic must be added, and test logic must be inserted. Also, if small changes are needed close to release, it may be less risky and have less impact on the design's timing and on our schedule to introduce these changes at the gate level. We forego a complete resynthesis so we can retain the synthesis results that we know meet our timing and area goals. We also avoid rerunning gate-level regression simulation targeted at detecting synthesis errors.

In many projects, we synthesize our gate-level netlists without scan. Then, we insert scan later, during the physical design process. It is this post-scan netlist that drives the layout process and test-vector generation. This is the netlist that is given to the ASIC vendor.

Any late gate-level changes we make to the "golden" hierarchical netlist must also be reflected in the flattened scan netlist. To do this accurately, we use equivalence checking to make sure the flat scan netlist is functionally identical to the hierarchical netlist. Of course, this comparison requires that we disable the scan chain so the circuits appear identical. This is easy to do using the equivalence checker's constraint commands.

The strategy shown in Figure 2 lets us concentrate our simulation at the RTL level, where we can run many more vectors than at the gate level. Then, we use the equivalence checker to compare full-chip netlists comprising several hundreds of thousands of gates in a fraction of the time needed to simulate a useful number of vectors at the gate level. On one of our recent designs of about 160 kgates, "builds" take about 60 minutes for the full hierarchical chip and 150 minutes for the flattened scan netlist. The "compare" takes about 134 minutes, for a total turnaround time of about six hours on an HP 9000/755.

Inventing new applications Some bugs that we find during prototype testing need to be fixed in the sample ICs so we can continue system testing. We can use a focused ion beam (FIB) machine to repair the die, but we only get one shot. The instructions for the machine must be perfect. Equivalence checking lets us make sure that we don't make a mistake (see Figure 3).

Table 1
Memory and run-time requirements
Block	Gate Count	Build RTL	Build Gates	Compare RTL-Gates
A	96 kgates	156 Mbytes 0:29	162 Mbytes 0:32	353 Mbytes 4:19
B	40 kgates	82 Mbytes 0:11	96 Mbytes 0:15	215 Mbytes 2:38
C	98 kgates	147 Mbytes 0:29	161 Mbytes 0:33	299 Mbytes 1:36

Table 1. Memory requirements and run times for RTL-to-gate comparisons on a few major functional blocks in a multiprocessor memory I/O controller design.

To prepare instructions for FIB, we first make the necessary changes to a netlist by hand. This produces a revised netlist that is functionally different from the existing ICs--it behaves as we want the chips to behave after repair. Second, we create a list of FIB instructions that should produce the same changes. Third, we follow these instructions to change another copy of the netlist. This netlist should be functionally identical to the first netlist that we changed. We use equivalence checking to completely compare these two netlists. If they are functionally equivalent, then we know the FIB instructions are correct. If not, we then rework the instructions and repeat the process until we know the FIB will produce the desired result.

Figure 3. Stratus use formal equivalence checking to ensure that focused Ion beam (FIB) instructions are perfect before repairing a prototype ASIC.

We have also been evaluating the use of equivalence checking to improve our hardware emulation. We have long believed that we would get better emulator performance if we could synthesize a special netlist using simple primitives, instead of the vendor library. But we were concerned that we might not be emulating the exact logic functions that the ASICs would implement. With equivalence checking, we can be sure that the emulation model matches the netlist we're releasing to the vendor.

Instead of trying to fit the vendor-specific netlist into the emulator, we separately synthesize a technology-independent version, which is much easier to load and faster to run. We use the equivalence checker to compare the two netlists. When they are the same, we proceed with emulation, knowing that we're emulating the right functionality.

Equivalence checking evolution As we have developed our methodology for using formal equivalence checking, limitations of the current tools have become evident. As is the case with all electronic design automation tools, we want more from formal verification.

We need better performance on large RTL blocks and on comparisons where the hierarchy differs in the RTL and the gates. We really want to compare a full chip netlist to the corresponding RTL model. While the ability of equivalence checkers to compare RTL with gates has improved dramatically during the past year, more is required. The current generation of equivalence checking software can compare RTL to gates for blocks up to about 100 kgates, when the hierarchy matches. We expect ongoing development in this area to improve the size and hierarchical complexity of the logic that the tools can handle.

Another area in which we need improvement is comparison of large, complex arithmetic circuits. These circuits have always posed special problems for formal comparison algorithms. While we've seen improvements that make the tools practical, more advances are needed.

Re-timing of logic across state bits poses a problem for current equivalence checkers. We want to be able to formally verify functional equivalence, even when they have moved logic from one side of a state bit to another.

Debugging tools The most important area for immediate improvement is better debugging tools for times when the comparison reveals differences. The equivalence checker provides reports that list which signals are different as well as information about the reason for the difference. But the causes of differences can be subtle and obscure, and we have often had to resort to simulation to find the exact cause of a bug.

We are currently beta testing a new tool called Design EXPLORE that works with Design VERIFYer to provide interactive debugging. This tool uses information from the comparison run and lets us interact with the symbolic representation of our logic to investigate the source of errors. We can look at the equations for the signals that could not be proven equivalent and use symbolic constraints to reduce the equations to just the portion that contains the different logic. We can then use this information about the equations to find the part of the source that generated the logic, and correct the problem.

Conclusion We have found that formal equivalence checking saves us time and improves our confidence of releasing functionally correct ICs. While we previously felt confident about the verification we achieved with simulation, we realized that as our designs got larger, the number of vectors and the time needed to simulate them would increase much faster. This "vector crisis" would make it harder and harder to be really sure that the functionality was correct.

Overview of equivalence checking

Equivalence checkers use mathematical methods to formally compare one version of a design with another, checking that the logic functions in one are equivalent to the functions in the other. Equivalence checking is more thorough than simulation because equivalence checkers only consider logic function. To use equivalence checking, one of the designs must already have been verified. This design serves as the specification, or reference, against which the other design is verified. To prepare each design for comparison, equivalence checking software must first compile the design descriptions into a mathematical representation on which the comparison algorithms operate. The result is a set of logic equations for the design, which are stored in a form that the software can use to make the comparison. Real-world designs are too large and complex to be verified using only a set of equations for the primary outputs. Instead, the compilation software breaks the design into smaller equations. All of the state bits in the design, in addition to the primary inputs and outputs, are the terminals for these smaller equations. The internal representation stores an equation for each primary output and for each state bit. The logic represented by each equation is referred to as a logic cone (see figure). Each state point and primary output in a design defines the end of a cone of logic. Each cone is driven by primary inputs and other state points. Clock logic and feedback are included in the equations for these cones. To make the comparison, the equivalence checking software must know how signals in each design correspond to one another. This is called "mapping." Some equivalence checkers require that users supply the mapping information, or the equivalence checkers rely on signal names being identical in the two designs. The Design VERIFYer software from Chrysalis has a special algorithm that it uses to automatically determine the mapping, even when the signal names are different--as they are when comparing RTL with gates, or comparing two gate-level designs that were synthesized independently. Comparing the two equations for two cones is straightforward once the mapping is established. When comparison of all the cones is complete, an equivalence checker writes a report that identifies whether the logic for all the signals compared successfully. If differences were found, it identifies in the report which signals could not be proven equivalent, and it gives as much information as it can about why there is a problem. Users read these reports to determine whether they can proceed with the next design steps, or whether they must debug the differences. To be compared by current equivalence checkers, two designs must be very close in their structure, particularly primary outputs, primary inputs, and state bits. This relation need not be exact; the tools can handle many-to-many correspondence and inversion of polarity between the circuits. If the designs differ too greatly, too many differences will be reported. This makes debugging difficult because differences tend to propagate during comparison. One real difference can make several other signals appear to be different. The software compiles RTL-, gate-, and switch-level models into the same mathematical form, so the comparison can succeed as long as the inputs, outputs, and state bits line up. The tools can even compare designs that are only partially equivalent. This is done by setting "constraints." Constraints apply values to a small number of inputs or internal signals to set up the conditions under which the functions are equivalent. For example, a constraint that sets a scan-enable bit inactive makes the scan version of a design look equivalent to the non-scan version. Representing logic cones. Each state point and primary output in a design is driven by primary inputs and other state points. Clock logic and feedback are included in the equations for these cones.

With formal equivalence checking, we find that we can be certain about changes that previously would have introduced risk, such as FIB repairs to precious prototype ASICs. At the same time, we have saved weeks of simulation time because formal verification checks our designs in just a few hours. With formal equivalence checking, we are able to focus simulation effort on the RTL. This lets us run many more vectors and check additional "corner cases," instead of re-running regression simulation at the gate level.

Products

Stratus Computers' products include Continuum Continuous Processing Systems based on the Hewlett-Packard PA-RISC microprocessor and the Intel I860 microprocessor for critical on-line computing. The company employs both cell-based and gate array technology ranging from 0.8 µm down to 0.5 µm, and from 50 up to 250 kgates. Formal verification was recently used in the development of two fault-tolerant multiprocessor memory-I/O interface chips and a fault tolerant PCI/system bridge chip for current and future Continuum Products, including the new Continuum Series 400. The Series 400, like the other members of the Continuum family, features a redundant hardware architecture along with self-checking and self-diagnosing logic.

Shawn Clayton is a verification engineer of hardware design at Stratus Computer Inc. (Marlboro, MA)

John Sweeney is the design verification manager at Stratus Computer.

Mark Tetreault is a senior design engineer at Stratus Computer.

Scott Sandler is a product marketing manager at Chyrsalis Symbolic Design Inc. (Billerica, MA).

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

integrated system design  November 1996