Achieve End-to-End FormalTM verification and
complete coverage with Oski Formal
Methodology and Abstraction ModelsTM!
Making the investment in formal does not guarantee convergence. The key is to use Oski Abstraction Models to incorporate formal into the design flow so that both formal and simulation can achieve a measurable verification closure, before sign-off. The result is reduced schedule, increased coverage, a measurable boost to productivity and better overall return on effort.
The value of Oski’s formal verification methodology is that it uses Abstraction Models 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, and is generally driven in one of two ways. The first is by sequential equivalence checking (SEC), comparing the RTL to its C reference model or a golden RTL. The second is by RTL formal property verification (model checking, or MC), proving properties against the RTL.
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.
Sequential Equivalence Checking (SEC) can also be used to formally compare two RTL models, one with modification that changes the sequential behavior of the design, such as inserting clock gating circuitry. Again for complex designs, careful use of constraints and methodology can help to ensure successful application of SEC to verify this class of problems.
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:
As we shift from simulation techniques to formal methods, verification methods become more powerful. The challenge for the formal tool is complexity.
SEC and MC are sophisticated techniques, and the straightforward use of these tools can result in state-space explosion, and protracted tool run times. There is no formal tool on the market today that completely solves the problem of state-space explosion. As shown in the diagram below, in order to get the maximum benefit from the formal methods and techniques, and improve convergence with formal, the use of Oski Abstraction Models is key.
Without Abstraction Models™, formal complexity can limit the applicability of formal tools
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 allow 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™ 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.
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.