Formal Verification Fulfilling Its Promise for IC Designers
Date: Wednesday , March 02, 2011
Formal verification for IC design has a long and interesting history spanning several decades. For many years it was seen more as a research project for academics than a real design and verification tool, but that began to change over the last decade as viable products began to appear on the market in the early to mid-2000s.
During this period there was initial reluctance to embrace formal technologies, often thought too challenging and complex for everyday use, but those notions are quickly changing with innovations to create a “user-friendly” formal tool. Once relegated to experts with very specialized knowledge, over time the complex aspects of formal technology have been pushed under the hood, opening it up to a broader audience. Over the past five years, formal verification was deployed first by experts in the verification team, then by the entire verification team, and lately it is being adopted by the designers themselves.
To put matters in context, semiconductor process technology is rapidly advancing as leading companies and foundries announce plans to move production to 20nm, opening vast new areas of silicon real estate that will populated with hundreds of millions of gates. As a result, the system-on-a-chip (SoC) will become mainstream, requiring IC designers to adapt from hand-crafting chips, to assembling them from individual blocks of intellectual property (IP). Formal verification is well-positioned in this changing environment to have an enormous impact on how SoC designs are created and verified.
Traditional verification methods, such as emulation which uses specialized and expensive hardware to mimic the behavior of a chip, or simulation to model behaviors, can be both time consuming and often unable to detect all errors, or “bugs,” in a chip. It is not at all uncommon for the verification of today’s large, complex ICs to consume weeks or even months of design time – estimated to be as much as 70 percent of the total – before they are ready to be manufactured.
Which brings us to formal verification. It is unique in its ability to fully prove that the design will perform as expected in a just fraction of the time required by other methods. Formal does this by ensuring the correctness of a design using advanced mathematical techniques, specifying design requirements that allow proving the correctness of the design with respect to the specification.
Formal verification provides 100 percent certainty that the design will work as expected by providing exhaustive coverage of the possible operating scenarios, something simulation alone is incapable of. To overcome the associated computational complexity, the latest formal tools can automatically model, at a higher level of abstraction, any design components which create complexity problems. This dramatically increases the performance and capacity for formal verification, while reducing the amount of memory needed to perform these tasks.
There are numerous instances of just how valuable formal can be in the SoC era. For example, IP that will be reused multiple times in many chips, needs to be certified for correctness using formal. If even one bug slips through, it could have a cascading effect on the entire system with disastrous consequences, and that nightmare scenario could play out on all the SoCs relying on that particular block.
At Jasper we have also applied formal techniques in new ways that allow designers to explore the functionality of a design and capture the design intent in a persistent and executable database with our ActiveDesign product. This database contains a variety of information, including configuration modes, transaction-annotated waveforms representing design functionalities, and more. The database, along with our formal analysis system, JasperGold, can then be used by the IP consumer to facilitate comprehension, modification, and re-verification.
These advances were validated at a recent meeting of Jasper users from around the globe, who are finding new and novel ways to apply formal to their biggest design challenges. Most notably, we learned that formal analysis is now routinely used during all phases of the design cycle, from specifying the architecture of the system, to finding bugs in test chips coming out of the fab.
As an early player in the development of these technologies, I am extremely gratified to see formal take its rightful place in the spotlight. It has moved well beyond the early adopter stage now, and will continue making inroads in every phase of IC design.
The author is the Chief Technology Officer, Jasper Design Automation.