Content area
Today, commercial formal-verification tools are allowing CPU designers to overcome functional verification hurdles caused by the skyrocketing size and complexity of deep-submicron silicon. One recent adopter of formal verification is Rise Technology, a Silicon Valley startup designing a multimillion-transistor microprocessor system. Without formal verification, CPUs would be prohibitively costly to develop, especially for startup companies. Rise Technology has pioneered a CPU design methodology that combines formal verification with emulation to validate the register-transfer-level model of a new design. Diagnostics, operating systems and applications run on the target system with the new CPU in the emulator, and formal verification ensures that the emulated gates are functionally identical to the RTL. The Chrysalis Design Verifyer formal-equivalence-checking software ensures that the emulated design has exactly the same logic as the RTL.
Full text
CPU designers are the first to feel the pain when established design methods no longer work, and the first to adopt new design tools and techniques. One such technique is formal verification, which has been used for several years by large CPU design houses such as IBM and Intel. Now, commercial formal-verification tools are allowing other CPU designers to overcome functional verification hurdles caused by the skyrocketing size and complexity of deep-submicron silicon.
One recent adopter of formal verification is Rise Technology, a Silicon Valley startup designing a multimillion-transistor microprocessor system. As a small company, Rise must use its limited resources as efficiently as possible. Since exhaustive simulation would be prohibitive both in terms of schedule and compute resources, Rise planned its validation methodology around formal verification and emulation.
Unlike many ASIC designers, engineers designing CPUs cannot use logic synthesis for all portions of their designs. Instead, they must rely on skilled circuit designers to craft performance-critical blocks from register-transfer-level (RTL) specifications. While this design style maximizes CPU performance, it also requires extensive verification of detailed circuit models.
It is this aspect of CPU design that has made formal verification a staple of the process. Formal verification is helping CPU designers overcome the exponential growth in effort required to design a new processor. Without it, CPUs would be prohibitively costly to develop, especially for startup companies.
All the nuances
In a typical CPU design project, system architects write RTL models that capture the intended processor microarchitecture. These models describe all the nuances of a machine's logic functions and serve as a detailed specification. Hierarchy is used in the RTL to partition the design into manageable blocks.
Verification engineers simulate the RTL model of an emerging CPU to ensure that it is functionally correct before detailed implementation begins. As much simulation as possible is run, and most CPU verification teams run at least part of a real operating system. So many vectors are required to do this that there is no way to repeat the simulation at lower levels of abstraction.
Circuit designers create a gate or transistor-level implementation for blocks that require custom design. This type of implementation is necessary to maximize performance of the finished product.
Unfortunately, the cell models used by synthesis tools to map a design to a silicon technology are not the most efficient way to allocate silicon or optimize for performance. Circuit designers can take advantage of their experience and certain tricks of the trade to eke out a block-level design that is typically faster and smaller than if the block were synthesized in a standard-cell technology.
Formal verification is an essential part of the CPU design methodology because the full suite of functional verification tests simulated at the RTL cannot possibly be run at the gate or switch level. If only a subset of the tests were simulated-a common way to stay on schedule before the emergence of formal verification-then the designers would be left with lingering doubt about the accuracy of their implementation.
When they use simulation to check an implementation, designers must assume that because the tests they tried did not reveal any errors, the design will operate correctly under all conditions-even those not simulated. This verification approach is inconclusive.
In contrast, formal verification is conclusive. All formal techniques use deductive mathematical proofs to check whether a design matches its specification. In the case of formal equivalence checking, the RTL model serves as the specification. Logic implemented by a switch-level netlist is compared with the logic encoded in an RTL model completely.
Because the comparison provided by formal verification is complete, designers are assured of detailed implementations that fully match the corresponding RTL specification. Moreover, formal equivalence-checking tools finish the comparison in a fraction of the time required to simulate a meaningful set of tests. CPU designers rely on formal verification because it helps them get higher-quality products to market faster.
A modern CPU design flow employs simulation, synthesis, manual design, formal verification and emulation. Simulation validates the RTL model prior to implementation. While some CPU designers handcraft every block, others synthesize as much as they can and handcraft only what they must.
Synthesis can often create most of the control logic, but circuit designers handcraft the parts of the design that must be fastest. Usually, this means manually designing the majority of the data path. In either case, formal equivalence checking proves whether the implementation matches the RTL specification.
Emulation is used to test the design in the target system, to begin software development early and to run long tests that cannot run on an RTL simulator due to time constraints. Since formal verification guarantees that the emulated net-list is functionally equivalent to the RTL, any errors found during emulation must be corrected in the RTL model.
When physical design proceeds in parallel with RTL functional validation, formal verification continually establishes the functional equivalence of the physical design with the RTL specification. This ensures that functional problems found and corrected late in the RTL validation are accurately reflected in the actual physical design.
Design validation
Rise Technology has pioneered a CPU design methodology that combines formal verification with emulation to validate the RTL model of a new design. Diagnostics, operating systems and applications run on the target system with the new CPU in the emulator, and formal verification ensures that the emulated gates are functionally identical to the RTL.
Although pioneered by CPU designers, this design flow has much in common with the practices of engineers who use gate-array and standard-cell technology. Although designers of ASICs for systems such as workstations and telecom equipment may not work at the switch level, they often handcraft gate-level net-lists, particularly for standard-cell data paths. Like CPU designers, they also rely on formal verification to confirm that they have implemented the intended logic functions.
Formal verification is not limited to checking the handcrafted portions of a design. As designers gain experience with the methodology, they typically replace regression simulation of synthesized gatelevel net-lists with formal equivalence checking. This saves time and makes designers confident of releasing functionally correct net-lists to physical design.
In the Rise methodology, simulation is concentrated at the RTL, which serves as the executable specification for the design. The gate-level implementation is emulated to run a comprehensive set of diagnostics, operating systems and applications. The Chrysalis Design Verifyer formal-equivalence-checking software ensures that the emulated design has exactly the same logic as the RTL
To implement the design, some blocks are synthesized and others are manually crafted by Rise circuit designers. Either way, the gate-level implementation is not archived in the design database until it receives a "certificate of equivalence" from the formal-verification tool. This certificate indicates that the implementation is equivalent to its RTL counterpart. Only when every block has a certificate can the design proceed to emulation.
Formal equivalence checking is an automated part of the check-in process at Rise. After a designer checks out a block and modifies it, the formal-verification tool runs as part of the check-in script. This "continuous verification" process gives the design team confidence that the implementation remains true to the RTL specification as the design progresses. No matter whether the change is a functional one that also affects the RTL or a net-list change such as a timing adjustment, formal verification makes sure the logic isn't inadvertently altered.
Formal verification also helps Rise engineers when they modify already verified RTL. For example, they often try to improve synthesis results while preserving the behavior of the logic. Using the capability of Design Verifyer to compare one RTL module with another, the engineers can confirm that the manual modifications did not alter any of the original functionality. This comparison works best for relatively minor changes confined to a single block.
Recursive excision
Rise optimized its design process to ease validation throughout the project. Module boundaries were clearly defined and strictly organized up front, and the hierarchy was kept consistent between RTL and gate-level representations. The boundaries were chosen both to partition the design logically and to correspond with levels at which the engineers thought they would want formal checks of equivalence.
Consistent, well-defined boundaries allow Rise to perform hierarchical formal verification by a process called recursive excision. In this process, lower-level blocks are verified first, and the higher levels in the design are checked by removing (excising) blocks that have already been verified.
When a block is excised, the signals it drives are treated as primary inputs and the signals that drive it as primary outputs of the design. This avoids having to reverify every lower-level block, and shortens formal-verification run-times.
Careful design of signal- and module-naming conventions helped Rise create scripts that automate many steps of the design process. These scripts generate certificates of equivalence for models at various levels by running formal-verification tools and recording the results of the comparisons. This automation helps ensure that the design is not corrupted as various team members work on the blocks, and helps engineers stay focused on design tasks rather than tool details.
Designing for verification helps Rise maintain concurrent development streams. It is not uncommon for several RTL, gate and physical design steps to proceed in parallel. The strategy allows work to progress on one portion of the design while another is in a state of flux. Formal verification ensures that parts don't get out of sync. Because of the well-thought-out hierarchy and naming conventions, functional equivalency is correlated among the models of the various design streams.
Transistor logic simulates very slowly. Circuit simulators are extremely accurate, but speed is not their goal. Eventdriven simulators are swamped by the number of primitives and nets in these detailed models. Most compiled-code and cyclebased simulators cannot even compile switch-level primitives.
Formal methods verify transistor logic quickly and completely. Logic functions implemented by switch-level net-lists are compiled into the same mathematical representation as the logic in RTL models or gate-level net-lists. That allows the comparison algorithms to check whether the logic created by circuit designers is equivalent to that specified by the architects at the RTL.
Rise uses a two-step, cellbased approach to verify the libraries it uses for its net-lists. A gate-level cell library contains both standard and custom cells, which are used when synthesizing or manually creating blocks of the design. Engineers add cells as necessary.
To verify the libraries, a Verilog switch-level model for each cell is extracted from the actual cell layout. Formal verification compares the switch-level model with the gate-level model for each cell, and the gate-level model with the RTL for the entire design. That ensures that the logic is correct and consistent across all levels of abstraction.
In addition to the static transistor logic that Rise extracts to verify its libraries, the Chrysalis symbolic-logic technology also handles dynamic transistor logic. Other users have developed additional techniques for identifying precharge and evaluate portions of the logic so that the compiler can infer correct operation.
Enhancements needed
Formal verification is already very effective, but like any new technology it can be improved. In particular, debugging tools and signal-name creation offer opportunities for enhancement.
Design Verifyer helps engineers examine the logic-driving signals to find out why they were not proven equivalent The idea is to directly explore the symbolic representation of the design's equations, but because the current tool is too awkward to use, Rise mostly relies on traditional methods instead. A new tool from Chrysalis, called Design Explore, will let engineers take better advantage of this technique.
When formal-verification software compiles an RTL module, it infers logic structures in much the same way synthesis does. In the process, the tool creates signal names that are not explicitly declared in the high-level model. Those names are not meaningful. A better naming algorithm would ease debug differences.
In spite of its limitations, formal verification's ability to locate mismatches between two blocks of logic makes it easier to find signal-mislabeling and connectivity problems. By reporting on the exact node of the mismatch, debugging a mismatched block is simplified to picking a particular node and tracing the logic that drives it. A formal-verification report with no mismatches, treated as a certification of equivalence by Rise, gives assurance that the implementation and executable specification are truly equivalent under all conditions.
Copyright CMP Publications, Inc. Nov 11, 1996