Making the investment in formal does not guarantee convergence. The value of Oski’s formal verification methodology is that it uses Abstraction Methods to transform the problem of state-space explosion, allowing formal tools to run thousands of times faster, resulting in convergence on end-to-end verification of designs as large as millions of state bits in the cone-of-influence of the verification problem. Oski’s formal verification methodology seamlessly integrates formal with traditional simulation-based and coverage-driven flows, starting with a comprehensive RTL verification plan.
Building a complete and effective RTL verification plan is based on a careful balance of two complementary verification techniques, as shown in the diagram below.
Formal verification methods include Sequential Equivalence Checking (SEC), and Model Checking (MC)
Simulation-based verification (both directed and constraint-based random) comes with the risk of missing difficult-to-detect corner-case bugs, and can take a long time in the schedule to achieve desirable verification convergence.
Formal verification proves that a design property holds for every point of the search space. Generally speaking, formal is driven in one of two ways. The first is by sequential equivalence checking (SEC), comparing an RTL to its C reference model, the second is by RTL formal property verification (model checking, or MC), proving properties against the RTL.
Sequential Equivalence Checking
Sequential Equivalence Checking (SEC) can be used to formally compare two models. One of these models could be the C reference model for the design, and the other, the RTL. Such a comparison can conclusively prove that the RTL complies with the C reference model, or find any mismatches between the two models. Again, a careful use of constraints and methodology is necessary to ensure that the problem complexity is manageable. The class of C constructs has to be chosen carefully, too. The set of designs where SEC is applicable is usually different from the ones where Formal Property Verification (or MC) is suitable.
RTL Formal Property Verification (Model Checking)
Formal verification tools can be used to verify the functionality of many control and datapath blocks, by proving the designs against a set of properties (or checkers). These tools, also known as model checkers, perform an exhaustive state-space search. They look for all possible corner cases that can show a violation of any of these checkers. The result of these tools, as shown in the diagram below, is one of three possibilities:
- proof that the properties are verified,
- counterexamples (or waveforms) that show problems in the RTL, or
- inconclusive results.
Complexity and the Risk of State-Space Explosion with Formal Tools
As we shift from simulation techniques to formal methods, verification methods become more powerful. But formal is not suitable for all designs, and making the investment in formal does not guarantee convergence, because of the problem of state-space explosion. The challenge for the formal tool, is complexity.
SEC and MC are complex techniques, and the straightforward use of these tools can result in state-space explosion, and protracted tool run times. For small or medium-size designs, the tool can run out of capacity, can take hours, or even weeks to run without producing interesting or conclusive results, and in most cases is not worth the return on effort. No formal tools on the market today completely solve the problem of state-space explosion.
Without Abstraction Models™, formal complexity can limit the applicability of formal tools
As shown in the diagram above, in order to get the maximum benefit from these formal methods and techniques, and improve convergence with formal, the use of Oski Abstraction Models is key.
How Do Abstraction Models Improve Convergence with Formal?
Abstraction Models are developed precisely to address the formal convergence problem of state-space explosion, by reducing complexity for the tool, even for large and/or complex designs. Abstraction Models are used to reduce the state-space of the design so that the formal verification tools can solve a computationally easier problem, allowing off-the-shelf EDA tools to scale for the verification of complex designs.
Oski Abstraction Models allow off-the-shelf EDA formal tools to scale for the verification of complex designs.
Oski Abstraction Models enable formal tools achieve unprecedented convergence by transforming the problem, allowing formal tools to analyze an alternate view of the design, and run thousands of times faster, resulting in convergence on end-to-end verification of designs as large as millions of state bits in the cone-of-influence of the verification problem.
Oski’s Plan-Verify-Measure Methodology Improves Return on Effort
Oski's Plan-Verify-Measure™ approach to End-to-End Formal™ verification
The key aspects of effective formal verification are structured verification planning, reusable verification IP, and good verification strategies. Because formal and simulation can be mutually reinforcing, and formal can complement simulation, or even replace it, formal can deliver better return on investment than simulation, provided that the correct methodology is applied. Creative verification strategies can mean better return on effort, and so the process of planning with formal becomes even more important.
Plan: Planning allows for a careful analysis of the design to determine which portions are suitable for formal vs simulation.
Verify: Abstraction Models are built to overcome the complexity problems while running formal verification.
Measure: After verification is complete, formal coverage measurement is used to quantify what was verified, and what was not.
The Value of Oski’s Methodology and Plan-Verify-Measure Approach
The value of Oski’s methodology and Plan-Verify-Measure approach is that it incorporates formal into the design flow. This means formal and simulation can achieve a measurable verification closure, before signoff. Formal can be integrated with traditional simulation-based and coverage-driven flows at each stage of the verification process, reducing schedule and increasing coverage for better overall return on effort and a measurable productivity advantage.