Formal verification has threatened to become mainstream almost forever. However, could it be that "formal apps" are the disguised guest that finally see us realize the Kathryn Kranen prediction that "formal will dominate verification"?
Mythology tells us that the Greeks finally sacked Troy after a 10-year siege by being invited into the city hidden inside a now famous wooden “Trojan” horse. Similarly, formal verification (FV) has threatened to become mainstream for as long as I can remember. However, could it be that “formal apps” are the disguised guest that finally see us realize the Kathryn Kranen prediction that "formal will dominate verification"?
Formal apps are automated applications to achieve specific verification tasks such as verifying that signals correctly cross clock domain boundaries, that post-reset X’s do not cause functional issues, or that a SoC (system-on-chip) correctly implements signal connectivity as specified in a spreadsheet or an IP-XACT description. In this blog I investigate such apps and whether they are leading us to full formal adoption.
For example, Cadence has been offering a portfolio of such apps since 2011. One of the fastest growing apps is Automated Coverage Hole Analysis, also known as Unreachability (UNR). The app automatically creates assertions that check for the reachability of coverage holes, based on the coverage database merged from multiple simulation regression runs. No user-defined assertions are required by the app, yet it uses the power of formal to accelerate coverage closure.
Joerg Mueller, a formal verification expert at Cadence, explains, “While each app may only utilize a subset of the power of FV, they pave the path to adoption of, and trust in, FV at many of our customers... The share of FV is increasing dramatically in the functional verification mix.” Mueller believes the reason for this trend -- apart from performance and capacity enhancements -- is the dramatically increased applicability, enabled by automating the previously cumbersome process of creating assertions, targeted at solving well defined, commonly occurring, yet complex verification problems.
Pranav Ashar, CTO at Real Intent, sees several reasons FV is now mainstream: “The capacity of formal apps has improved dramatically. Secondly we know where to apply formal and to use it where it can make a real difference.”
Real Intent believes the best places are where the scope is narrow and there is a full understanding of the failure modes, especially in the places where simulation just can’t scale. Clock-domain crossing (CDC) is a great example of that. These kinds of failures are a mix of functionality and timing, and when these two things happen asynchronously, simulation falls apart. For example, Real Intent noted how a user at DVCon 2014 in Silicon Valley had finished simulation and then found another 20 bugs using a CDC tool. The more you understand a problem, and the design steps become more understood, there are more areas that are suitable to formal apps.
Real Intent is currently seeing a lot of interest in analysis of the propagation of Xs (unknowns) and reset optimization. Finally, Ashar added, “Because of the problem focus, debug information is easily provided that is relevant and actionable by design and verification engineers."
OneSpin Solutions includes a range of formal apps within its Design Verification 360 product line, including Connectivity, X-Propagation, Register Implementation, and other checks. The company has found that its DV 360 Verify Property Checker is now being adopted as a platform for domain experts to create their own highly specialized apps. It also provides a coverage solution as part of Verify to ensure verification closure that is focused on the formal process.
OneSpin's Quantify technology employs “Observation Coverage” to measure the effectiveness of verification checks in detecting design functionality changes as well as evaluating code reachability, leveraging formal engines to ensure a high degree of accuracy. The formal verification coverage data may be loaded into an Accellera Unified Coverage Interoperability Standard (UCIS) database from where it can be combined with simulation data using tools like asureSIGN™ from Test and Verification Solutions (TVS).
“Coverage is an essential mechanism to control complex verification processes,” notes Dave Kelf of OneSpin. “It is essential that coverage data is read from many different sources, and Accellera has provided the mechanism to do this.”
Mentor Graphics offers a full range of formal apps, many of which are of the Trojan horse variety. Some of the most widely used Questa Formal apps are fully automatic in nature, and they completely shield the user from the fact that the latest generation of formal engines are being used under the hood. These include CDC, RTL coding checks, X-checks, and property generation. In addition, the formal apps are fully integrated with simulation and emulation to create solutions that exploit multiple verification engines.
Mentor is seeing high growth in the adoption rate of Questa CoverCheck, its formal coverage closure solution. Roger Sabbagh, a 14-year veteran of Mentor’s formal team, explains how: “By seamlessly switching between formal, simulation, and emulation to target a common goal, the strengths of each technology can be brought to bear on challenging verification tasks, such as coverage closure.”
TVS has also seen strong demand for its Formal Verification Bootcamp, which helps delegates adopt both apps (from the client's chosen EDA vendor) and the more general-purpose formal verification flow through writing of design-specific SVA constraints and properties.
Mentor’s Sabbagh concludes, “According to EDA Consortium reports, the formal property checking market grew by over 40% last year and is expected to top the $100 million mark in 2014,” which is a significant milestone.
Is this evidence enough to say Formal will dominate?
— Dr. Mike Bartley, founder and CEO of TVS, has a PhD in mathematics from Bristol University, an MSc in software engineering and an MBA from the Open University, and over 20 years of experience in software testing and hardware verification. He has built and managed state-of-the-art test and verification teams in a number of companies (including STMicroelectronics, Infineon, and Elixent/Panasonic), which still use the methodologies he established. Since founding TVS he has consulted on multiple verification projects for respected organizations and has had more than 20 articles published on the subject of verification and outsourcing. Contact Dr. Bartley at firstname.lastname@example.org.