Oski has pioneered the methodology for end-to-end formal sign-off, which ensures that no bugs are left behind after the verification process – including simulation-resistant superbugs. This process can be broken down into the four “Cs” of formal sign-off (Fig. 1).
Figure 1: The 4 Cs of Oski Formal Sign-off
End-to-end checkers are quite different than typical assertion-based checks. They model the end to end behavior of the block under test and predict what the output should be based on the input, much like a scoreboard. However, they are coded in a distinct way that makes them suitable for formal verification. They are lightweight and don’t add too much complexity to the state space of the model which is important for formal.
By default, formal will explore all possible input stimulus, so it’s important to filter out the illegal input space with constraints so that we don’t see false failures of the checkers. However, care must be taken to verify that there are no over-constraints which could mask real failures and cause us to miss bugs in the design. Oski verifies the constraints through formal methods such as assume-guarantee and by running the constraints as assertions in the higher-level simulation environment.
Dealing with Complexity
Formal tends to run into complexity barriers for complex designs, especially when dealing with end to end checkers. This brings the requirement for the next piece of the methodology, which are the abstraction models. The abstraction models reduce the state space or latency of the design so that formal verification can explore beyond it’s default threshold.
Formal coverage is a key component of the sign-off methodology. Much like in simulation, formal coverage metrics help us to measure controllability – how much of the design states have been covered by the input stimulus that we’ve explored. But, they also have a unique ability to report observability coverage – that is how much of the design states are being checked by our end-to-end checkers. This makes formal coverage a very strong metric for measuring progress and closing verification holes.
This process has been successfully deployed on dozens of tape-outs and it has shown the ability to find all bugs in a design very efficiently, including superbugs that would have been likely to slip through the traditional verification process.