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.

Oski Abstraction Models Offer Highest Coverage and Faster Time to Market

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.

Formal Tools, Complexity and the Risk of State-Space Explosion

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.

Oski Methodology

Without Abstraction Models™, formal complexity can limit the applicability of formal tools

How Abstraction Models Improve Convergence with Formal

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.

Abstractions Diagram

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.