An initiative undertaken by Oski Technology to create an interactive dialogue with the formal verification community and answer your questions regarding formal verification. The idea is simple: take the questions from the community and post the answers here periodically. You have a question? — #AskOski

Submitting a question to Oski is easy. Just type it in the form below, or post it on social media platforms like LinkedIn with hashtag #AskOski.

Submit your #AskOski question

Recently answered questions…

What is an Abstraction Model? How to ensure its correctness?

An Abstraction Model can be a savior when checkers are inconclusive and stuck at insufficient proof depths. Abstraction Models combat proof complexity. They aid formal tools to reach deeper corners of a design in many fewer steps of formal search. They help to achieve sufficient proof depths for checkers and provide confidence that the last design bug has been found. Correctness of an Abstraction Model can be ensured by proving it against the un-abstracted design, making it a foolproof solution to formal complexity.
Read the detailed answer here.

What is a vacuous proof? How dangerous are they?

A vacuous proof is a dangerous thing in formal verification and needs immediate attention. It is an extreme case of a false positive where your checker says that everything is working fine while often checking nothing meaningful. The most common reason to arrive at a vacuous proof is the presence of conflicting constraints in the formal verification environment. So, meticulous management of constraints goes a long way in helping to avoid them. However, there are other reasons as well.

Read the detailed answer here.

Does formal verification support code coverage?

Yes, formal verification supports as much code coverage as simulation does – and more! However, the way we use code coverage in formal verification is very different from the way we use it in simulation.

Read the detailed answer here.

None of my assertions are passing. They're all inconclusive. What should I do?

First of all, please don’t throw them away. Trust me, they are useful. It’s painful to see engineers throwing away their hard work just because the formal tools are conservative about how they report results and tag bounded proofs as inconclusive. We just need to go one step further and analyse these results to find the good news in them. Hint: every inconclusive result usually comes with a number attached to it.

Read the detailed answer here.