Formal Verification’s Continental Divide

Formal verification is picking up steam with engineering groups worldwide doing complex functional verification for bug-free and reliable digital chips. In fact, many difficult verification challenges are solved with formal verification, given its flexibility in targeting a broad range of verification challenges. Recent advances in formal verification’s ease of use and capacity has made it an all-the-more indispensable tool.

Oddly enough, the way formal verification is deployed appears to be different continent by continent. Global trends and use models for formal verification could almost be considered a continental divide. In an interesting dichotomy, formal might also reduce the effect of this divide.

Just consider the use of SystemC, popular with large semiconductor and electronic systems companies in Asia and only now catching on in the engineering community elsewhere. High Level Synthesis transforms algorithmic and potentially untimed design models often written in SystemC and C++ to fully timed RTL design blocks. This mechanism has been used in Japan as a method to generate design components with varying microarchitectures, while optimizing algorithm processing datapaths rapidly and effectively, providing flexibility and faster time to market. The SystemC language is based on C++, which was not designed for hardware description and, as such, could create issues for engineers more familiar with HDLs. Japanese engineering groups now use SystemC-based formal verification to detect and eliminate these language issues (e.g. X-state problems and race conditions) in their SystemC code prior to high level synthesis. This use of formal verification is spreading to other companies worldwide, easing their issues with SystemC.

A few continents away, safety critical design is important in Europe because of the large automotive industry there. It’s starting to become important in the U.S., but the momentum’s not quite there yet. Formal verification has multiple applications for both systematic and random fault verification to meet the requirements of the ISO 26262 standard. It addresses specific challenges in the efficient development of safety-critical hardware, significantly transforming both the quality and efficiency of the verification process, and streamlining the activities required to satisfy the ISO 26262 standard. Engineering groups in Europe designing for safety critical applications view it as a powerful technique to uncover hardware design bugs that might otherwise escape simulation-based verification and lead to systematic failures. Formal verification also improved the engineering team’s ability to calculate diagnostic fault coverage, and this again has improved the flow and made it easier to apply universally.

U.S.-based engineering groups have slightly different concerns than their fellow engineers in other continents and are often challenged with more immediate project issues that need quick solutions. Formal verification has proven invaluable in solving specific and difficult verification issues hard to handle using other methods. Be it automated apps or assertion-based verification, formal can provide a layer of functionality over simulation that cuts verification schedules. Formal verification has been used for a few years in the bug-hunting cycle toward the end of the verification process, and its application is moving up front at the beginning of the cycle, where it replaces simulation for some tougher blocks. Combining coverage metrics and integrating formal into the verification planning process has led to even greater efficiency.

Formal verification’s ability to provide solutions for all of these applications demonstrates how the technology can be used in disparate environments. Moving forward, the semiconductor industry is left to ponder whether this divergence by continent is the wave of the future or a convergence of applications.  Or whether formal can be the tool that unifies these varied methodologies and allows all engineering teams to benefit from each other’s experience.