Formal methods for hardware design were commercialized more than 15 years ago, and there are now several established applications based on formal, mathematical analysis in the market. With years of practical experience and recent technical advances, the application of formal methods to system-on-chip (SoC) design and verification is expanding. More so, additional formal applications will be required as the electronics industry continues to try to address the challenges of increasing design complexity.
Traditionally, formal methods have found success verifying the output of design automation tools — that is, checking the results of synthesis. As an example, combinational equivalence checking is a fixture in all register-transfer-level (RTL) synthesis design flows.
Today, there are several new applications built upon formal methods. These include model checking, directed test-pattern generation, gate-level retiming, clock domain-crossing verification, sequential clock gating, and system-level-to-RTL equivalence checking. These new applications have been made possible by technology advances in formal analysis. Specifically, those advances include sequential analysis technology such as satisfiability (SAT) and symbolic model verification (SMV) engines. General-purpose formal analysis engines such as those developed in academia have been adopted and enhanced by companies to solve new classes of verification problems. For example, companies have applied sequential analysis technology to extend the use of formal methods from the traditional gate-level domain into RTL and the system level.
Whether verifying system-level models, retimed gates, or anything in between, formal methods have the advantage of comprehensively verifying code that is too complex or unfamiliar for a designer to confidently manage. In many cases simulation alone is not sufficient. Take power optimization as an example. A common technique for reducing power is RTL clock gating, a sequential design change that takes advantage of design "don't care" states to disable logic when the result is not used. To adequately verify RTL clock gating with simulation, testbenches must be modified to cover all combinations of inputs that create "don't care" scenarios. The number and temporal nature of these testbenches make verification difficult for designers to comprehend. Formal methods, on the other hand, exhaustively verify all combinations of inputs and transitions between active and "don't care" states automatically. This is one of the strengths of formal methods.
Formal methods have become a must-have tool for designers to manage verification complexity. However, they are not a substitute for an overall verification plan and simulation, since formal methods are based on fundamentally exponential algorithms. Successful formal applications use design knowledge, including intermediate points, design characteristics and constraints in order to deal with larger design capacity and to shorten runtimes. One trend is to integrate formal methods into an overall verification environment that leverages the strengths of multiple technologies. Such integrations break down the barriers of adoption and bring formal methods to the mainstream hardware designer.
As formal technologies advance, the applications they spawn are changing the way engineers design. Take, for instance, recent advances in sequential equivalence checking that allow designers to confidently make micro-architectural RTL optimizations, including retiming, pipelining, and clock gating. Previously, these power and performance optimizations were avoided — or performed only when necessary — because of the verification problems they create. Formal methods are also being applied to system-level design flows. With sequential equivalence checking, system-level hardware design becomes practical by verifying that RTL implementations match original system-level design or by providing a verifiable, high-level synthesis flow from system-level design.
Looking forward, design teams should expect to see new applications based on formal methods integrated into their overall verification environment. These applications will be required to manage design complexity. SoC designers, in turn, will adopt these solutions and push design complexity to yet another level. And the cycle of innovation, creativity and design complexity continues.