Design Automation

Turning to Formal Verification

Cray Research learns firsthand about the current capabilities of formal methods.

by Scott Schroeder

Cray Research develops highly complex next-generation systems for applications in the high-end technical computing market. The design challenges we face are common to companies developing advanced systems: greater complexity, larger gate counts, vastly higher densities, and reduced time to market. Also like other companies, we've been discovering that our traditional design methodologies are no longer practical. In fact, with our next-generation ASIC designs running at a million gates or more, we may be feeling the crunch more severely than most.

One major area of concern has been functional verification, where we have made an organizational commitment to explore alternatives to current methodologies. We've created a dedicated logic design verification group within the Development Division that is responsible for various aspects of logical verification, including traditional simulation techniques and emerging formal methods.

Our efforts have led us to become a beta site for formal verification tools, including Chrysalis's equivalence checker, Design Verifyer, and Bell Labs Design Automation's model checker, FormalCheck. After several years of using these tools, our hands-on experience has given us some insight into both the limitations of formal methods and the enormous and exciting potential benefits.

Strained methodologies Cray began designing and implementing massively parallel processing systems in the late 1980's and early 1990's. As we refined the architecture for this type of system, we had to develop more robust and more general cache coherence mechanisms. However, the new mechanisms placed a great strain on our simulation-only design verification methodology and so became the impetus to explore other solutions.

At the time, our verification methodology consisted mostly of a combination of event- and cycle-based simulation. For the smallest logic units, event-based simulation provided the fastest run times and the highest flexibility when creating test beds (for end-to-end simulation) and behavioral codes (for side-by-side simulation). At the other end of the scale, cycle-based simulation (with an in-house implementation tuned to Cray supercomputers) was the most efficient for very large system configurations.

Much of this methodology is still effective, and we plan to keep those parts intact for the foreseeable future. But as our designs have grown in complexity, certain problems with simulation that have always been present have become more significant.

First, simulation requires a great deal of time to set up test beds, checkers and behavioral models, and assertions, leaving very little time for us to understand the expected properties of a design. We estimate, for example, that only 20 to 30 percent of the time it took to verify the Cray T3E system was spent understanding the behavior of the design itself; the rest was spent getting at that behavior with simulation vectors and properly detecting if an error was exposed. Such a lopsided effort was the handwriting on the wall for us. We understood that growing design size and architectural complexity would give us progressively less time to understand fundamental behaviors.

Second, simulation vectors are necessarily redundant at times and incomplete at others. It's easier and less costly to compensate for such inefficiencies on simpler circuits, where the ratio of gates and architectural interactions to design verification engineers is lower. But on the more complex, higher gate-count circuits currently under development, the ratio is tilting strongly against the engineers. On these circuits, the inefficiencies of simulation can mean dramatically higher costs, longer run times, and nagging doubts.

Figure 1. FormalCheck's modular architecture enables the tool's capabilities to be extended in the future.

Confronted with these challenges, we began to look for new solutions. Prior to our merger with Silicon Graphics Inc. (SGI), we became aware of work it had done to formally verify the cache coherency protocol for its Origen2000 system. SGI had a solid success story, and the verification work for the Cray T3E showed us what was in store if we failed to address the problem, so we began to explore formal methods for ourselves.

Equivalence checking Our first experience with formal verification was Design Verifyer, an equivalence checker from Chrysalis Symbolic Design. Equivalence-checking algorithms have been tuned to address one question--Is the current design equivalent to an earlier reference design?--making the technology effective only for verifying needed postsynthesis design changes. At Cray, we've used the tool to automate three checks: verifying the equivalence of an RTL design against its derived postsynthesis gate list; comparing two gate-level implementations after the ASIC vendor's scan insertion work; and verifying that any engineering change orders made after the chip has been released have been identically reflected in both the RTL and gate-level design files.

Although the tool has been effective at reducing the tedium of regression-testing all those changes, it should be made clear what equivalence checking does and does not do. Equivalence checking fills a hole in the design verification engineer's tool set, but its results are very focused. Its highly refined algorithms leave out some of the stickiest problems, like verifying an initial RTL implementation against the original specification or comparing a modified RTL model with an earlier version. We've also had trouble getting the tool to work with the size circuits we develop. We've worked extensively with Chrysalis to solve this problem, but it is still requiring effort to improve the "time to solution" for any given equivalence check. Run times, mapping algorithms, GUI interface improvement, and user expertise will all need improvements for this technology to increase its effectiveness.

Model checking The limitations of equivalence checking and the continued problems with simulation forced us to look into model checking, also a formal method but much broader in scope. Unlike equivalence checking, model checking can verify any behavior a chip might exhibit against a specification or other reference, provided it is posed to the tool in the form of a logical query. That makes it better able to handle the RTL verification issues we are most concerned about.

Investigation of this technology at several levels of Cray ultimately led us to a beta program for FormalCheck, a productized version from Lucent Technologies' Bell Labs Design Automation (BLDA) of the model-checking engine developed by what was then AT&T's Bell Labs (see Figure 1). Contact was made in early 1996, with a beta program established at Cray in June of that year.

We chose FormalCheck for several reasons. First, it appears to be one of the easiest formal tools to use on the market today. It accepts both VHDL and Verilog, and it includes a query template library to simplify posing queries to the tool. Second, there is very little doubt that the underlying technology is sound. The Bell Labs name carries a great deal of credibility, and with over a decade of research behind it, FormalCheck's Cospan verification engine appears to live up to that reputation. It's as robust and stable as any we've found. On the business side, it also appears that BLDA has made a complete commitment to the technology and is prepared to do whatever it takes in terms of customer support and changes to the tool to make it a successful product.

Figure 2. FormalCheck displays the results of an exhaustive analysis of the arbiter's input 1 request.

Our strategy with model checking was to start with fairly simple Verilog designs and gradually develop our expertise and familiarity with the tool. We focused on a project that was in development as the follow-on to the Origen 2000. The ASIC in this design was a data communications routing chip with more than a million gates. We focused the verification on the multiprocessor synchronization controller and the central arbitration unit, which arbitrated a number of input channels to one of a number of output channels.

We attacked the arbitration unit by looking first at a medium-sized submodule that contained the actual arbitration control logic. The module contained a rank of registers at its inputs and performed all other computations using combinational logic.

We had some trouble with the circuit until we recognized that it was largely combinational logic. We were able to get FormalCheck to run by modifying the design and queries slightly, and ultimately it found several bugs in the logic that would have cost a great deal more in dollars, time, and manpower had we been forced to fix them later in the design cycle (see Figure 2). This sort of preemptive debugging is a great benefit of model checking.

Understanding needed It was also during this verification that it became clear that we needed a detailed understanding of the circuit to make our queries effective (we wrote 392 queries to verify the module, most of them generated from perl scripts after we understood how to automate the query-writing process). Unlike the case with simulation, we spent most of our time and effort understanding the design (see Figure 3). Furthermore, we discovered that small, tight queries help keep run times low and that the increased number of queries opens the door to using parallelism to further reduce the time for large verifications.

The tool, then, was a success on the first submodule, but it has been more difficult to use when applied to the larger arbitration block. A circuit of such complexity requires comparably more complex query generation, and we finally decided to set up a training session with BLDA. Their help has allowed us to write better queries, but the run times ultimately haven't been fast enough for the larger circuit.

Figure 3. FormalCheck's intuitive query facility simplifies the capture of complex design intents, such as the arbiter's input 1 request.

To solve this problem, we recently switched to a dedicated Ultra-SPARC 2 for much faster run times, and we envision using SGI systems by the end of the year for an even more dramatic increase in speed. FormalCheck also has certain features that have helped keep run times much lower than they might be. It includes automatic reduction algorithms that eliminate portions of the circuit that can't affect the verification outcome. Ignoring those portions can often significantly reduce the state space to be verified. In addition, circuits like the arbitration block that are dominated by control functions are naturally more attractive for a model checker. Control functions are highly dependent on previous input sequences, and FormalCheck's algorithms take advantage of that dependence to check all possible state transitions without checking any more than once. The resulting verification is simultaneously faster and more methodical, without the redundancy and lack of thoroughness that typifies simulation tools.

The amount of effort we've spent to get FormalCheck working on our largest designs is a testament to how valuable we expect the technology to become to our design flow. The work we are currently doing, however, doesn't get us closer to verifying our original problem: a large cache coherency protocol. To use formal analysis on a design of that complexity will take more work--and more time.

Critical challenges Any shift to a new methodology involves some degree of effort. Therefore the decision to switch always comes down to how badly the change is needed and how difficult it will be to make. For Cray, there is little question that the strains in our design flow have demanded a new system.

As for the difficulty required, it appears that there have been two major obstacles to adopting the technology and making it a seamless part of our design flow. Neither has been insurmountable, but both will take more work to overcome completely.

The first is the shift in perspective. As mentioned earlier, one of the problems with simulation is that it requires a great deal of time to develop ancillary items like test beds that support the actual simulation. Formal verification doesn't need that supporting environment, but it does require a deep understanding of the design to be checked. With that understanding, virtually any circuit can be verified; without it, what is otherwise a simple query-writing process can become very difficult.

The second obstacle is to learn where model checking should be used versus other design methodologies. The answer to that will become clearer the more we use the tool, and we've already made some distinctions. It's not difficult to see, for instance, that equivalence checking will be most effective for postsynthesis verification, whereas model checking will add the most value much earlier on.

What is likely to prove more puzzling is when to use simulation instead of formal verification, although we can make predictions to some degree, based on the current state of the tools. To be as systematic as possible, we'll likely perform model checking first on a subset of the design and then scale up to larger and larger portions until we are forced to move to a vector-based tool. For the rest, we'll most likely use event-driven simulation for circuits dominated by combinational logic and cycle-based simulation for very large circuits dominated by control logic.

The decision when to use each tool will, of course, change with new tool capabilities. BLDA has been working steadily on ways to increase the size of the largest circuit FormalCheck can handle. With such advances, coupled with increased computing power, it may not be long before very large system-level designs are within the technology's reach.

It should be noted that formal methods require a fairly significant shift in methodology and shouldn't yet be considered mainstream. At Cray, we're working on extremely sophisticated designs where simulation is simply no longer effective by itself. Today, at least, the effort necessary to change methodologies might not be justified for those working on non-leading-edge designs.

Nevertheless, it is Cray's belief that the market is moving very strongly toward formal verification, and that the average design two or three years from now will be complex enough to justify switching to formal methods. Furthermore, even though formal verification is not yet mainstream, commercial applications are clearly emerging. In fact, it is hard to imagine how a leading-edge design company could remain competitive today without adopting a formal verification strategy. It requires effort, but the alternative is to fall behind in an increasingly competitive high-technology marketplace. *

Scott Schroeder is the director of verification at Cray Research Inc. (Chippewa Falls, Wis.).

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

integrated system design  September 1997