Leveraging your Investment in Formal with Abstraction Models

Formal tools and technology have made significant advances in recent years. Formal tools allow designers to more easily use formal, even when formal was not part of the initial verification strategy. This is especially valuable for very large designs, which is why an increasing number of very visible IC companies are adopting formal as part of verification sign-off.

But while formal is being more widely adopted, no formal tools on the market today completely solve the problem of state-space explosion. Even the best high-performance formal tools very rapidly run into complexity and state space explosion and inevitably fail to converge, having a significant and detrimental impact on schedule. For small and medium-sized designs, they may never finish the job because the tools are looking at a very large state space of the design.

Formal complexity graph

Oski Abstraction Models Improve Runtimes, Reduce Schedule

Oski’s Abstraction Models benefit design and verification engineers by reducing the effort for formal tools, compressing the state space, very often improving the runtimes by x1000. Abstraction Models are critical for the application of advanced verification, in that they apply formal modeling methods to transform the state space of the design, reducing verification complexity with better coverage.

Because formal verification can be used to find, fix and verify bugs at any stage of the SOC cycle, including post-silicon bugs, leveraging Abstraction Models can have a significant overall impact on ROI.