Formal Bounded Proof , Does it make sense to DV engineer ?

In formal verification there are three type of proof

1. The property is passed it means that the property is unreachable
2. The properties failed, it means the design is not behaving correctly.
3. The properties unsolved, it will it ran for many hours, result is non conclusive.

When we talk about unsolved what does it mean, and how do we solve it.

There it comes bounded solution.

Lets run design for x cycle depth , x could be 20/../30 depends on the logic design and check the property, did design pass it , if yes great . Design is good to go for x cycle.

If it doesn’t pass for x+10 cycles , it means design is good till 20 (x is 20) cycles, between 20 to 30 , it doesn’t have guaranty

Once the user calculates the required proof depth, then all inconclusive results are separated into two groups. The first is checkers that reached the required proof depth. In this case, their status is as good as passing. The other is checkers that haven’t reached the required proof depth. For example, the required proof depth is 30, but the formal tool only reached 20 cycles in its analysis. At that point, the user looks at what techniques can be used to reach the required proof depth. Most often, there’s something he or she can do for that, such as using Abstraction Models.

Bounded results can be as good as unbounded results, if the checker reached the required proof depths. If the user doesn’t get unbounded proofs, it doesn’t mean the results aren’t meaningful.