In recent years, formal verification has become the verification methodology of choice for many designers and verification engineers. It's now in the mainstream marketplace, as it's easy to use, integrates easily into the design flow, and finds bugs that simulation-based methods often miss.
With verification continuing to be the biggest bottleneck in the semiconductor design flow, demand for next-generation formal verification methodologies won't decrease in the short term, or even in the long term. Instead, formal verification will be used in an ever increasing variety of interesting ways.
For example, many assumptions made during the design and verification process aren't verified by equivalence checking, necessitating further use of gate-level simulation. Advances in formal-based methodologies will enable some designers to almost entirely eliminate lengthy gate-level simulations.
As outlandish as this may sound, certain classes of bugs don't manifest themselves until the gate level. These bugs include differences in handling of don't-cares or un-knowns between register-transfer-level (RTL) and gate-level designs, as well as functional changes made at the gate level, like test logic and clock trees.
Synthesis tools sometimes make some assumptions about the designer's intent when implementing RTL designs into gates. Equivalence checkers have traditionally not checked these assumptions. They may flag RTL don't-cares or unknowns with warnings, but when there are too many warnings, designers often ignore them.
Many times, test logic isn't added to the design until the gate level, and it may not have a functional counterpart in the RTL design. To equivalence-check the gate-level design against the RTL, test logic is disabled and not verified. Users of equivalence checking must either assume that the test logic is correct, or verify it using gate-level simulation.
Formal flows that provide both equivalence checking and supplemental types of formal techniques, such as formal analysis and assertion checking, can verify assumptions made during the design process, bridging this verification gap. This reduces or even eliminates the need for gate-level simulation to check these assumptions.
Many bugs found today with formal verification software are problems that caused designers to refabricate or respin their designs in the past. Before formal verification, these bugs went undetected because there just wasn't enough time to simulate everything.
Formal methods can automate and speed up the process of thoroughly checking things that a designer might not otherwise remember to check. For example, they can automatically find every multidriven signal in a design and check that there are no bus-contention or floating-bus problems.
Formal methods also can verify designer-specified characteristics faster and far more thoroughly than simulation. For instance, checking that a 64-bit comparator operates correctly would take more than 500,000 years to exhaustively verify via a simulator that runs at 1 million vectors per second. But using an assertion checker to make the same check might take about 1 minute for the designer to write and merely seconds for it to be exhaustively verified.
Market acceptance of this type of formal verification will accelerate. This is due to progress in easy-to-use assertion languages and open-source assertion library standardization efforts, like the Open Verification Library (OVL) donated to Accellera.
Formal methods and solutions are being extended well beyond the gate level to the physical. In the not-too-distant past, altering netlists after logic synthesis was a design taboo. Newer physical-design closure flows often perform aggressive logic optimization right until the final Spice netlist is generated. Closely associated with this trend is the increasing use of customer-owned tooling flows, many of which also terminate at the Spice level.
For designers to gain more confidence that physical-design closure flows are producing correct results, they will increasingly depend on RTL-to-transistor-level equivalence checking. Spice-level simulation just takes too much time and can't be thorough enough for confidence.
In addition, formal methods are expanding into the area of field-programmable gate-array (FPGA) design verification. Formal verification has become an important piece of an FPGA design environment as design density increases because simulation is no longer adequate for verifying complex designs. Applying formal verification techniques can reduce design cycle times to meet demanding time-to-market challenges.
All in all, the future for formal verification is bright. Designers are finding more applications for the technology from initial RTL to final physical netlist. The more entrepreneurial electronic design automation companies will listen carefully and respond to the challenges presented by their users.
Reprints
