When formal verification was introduced a few decades ago, the perception was that a Ph.D. in the subject was needed to use the methodology. SystemVerilog, the hardware description and verification language used in modeling, designing, simulating, testing, and implementing electronic systems, was not commonly known at the time. In the early 2000s, many formal startups had their own property languages and there was little compatibility between tools. Over the years, consolidation took hold, and more engineers began writing SystemVerilog assertions. Today, the SystemVerilog language is an industry standard, well-known by chip verification engineers now accustomed to writing assertions and developing formal testbenches. Without formal verification, it would be nearly impossible to find all corner-case bugs. The human brain is simply not wired to come up with the seemingly endless input combinations to exhaustively verify each block of each design.
Formal verification can exhaustively verify a block using mathematical proof without the need of enumerating all input combinations. However, it does take effort to write assertions that can be verified with FPV to provide conclusive results on whether the assertions pass or fail the design, and when some of the assertions fail to debug the assertion failure. Another possible outcome of FPV is inconclusive results where FPV tools are not able to conclusively prove or falsify the assertions under the time and resource constraints. Often techniques such as writing abstraction models are needed to reach convergence. Even though designers have deep knowledge of the blocks and designs they’re verifying, for many, writing abstraction models to address inconclusive findings is not easy.
Synopsys VC Formal™ next-generation formal verification solution provides the capacity, speed, and flexibility to verify complex SoCs. Machine learning techniques have been used in the VC Formal solution to improve performance and reduce the user debugging effort. For example, Smart Strategy Selection enables smart engine orchestration by learning, during the run, to assign the best engine to the assertions to be verified, leveraging the right resources. Regression Mode Accelerator (RMA) allows learning to continue in subsequent regression runs to optimize performance and improve convergence. Machine learning is also used in debugging. When there are many violations, some are bound to be caused by the same issues. VC Formal technology clusters violations based on root-cause analysis so that when one is fixed, the others are also fixed, reducing user debugging effort.