Content area
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...