Formal Verification Sign-Off Methodology
Growing Parallelism Mandates Formal Sign-Off
Applications such as high-performance computing (HPC), Big Data, and Machine Learning are driving ever-increasing requirements for networking and computing performance.
With transistors switching speed unable to keep up with performance demands, designers have been exploiting parallelism for well over a decade now. Their massively parallel computing architectures require complicated synchronization and resource sharing techniques that exponentially increase the:
- Number of possible states to be tested
- Coverage space
- Number of bugs to be found
Because there is so much parallelism, the gap between what simulation can achieve and 100% has grown. There are bugs that simulation cannot find.
Oski’s unique formal verification sign-off methodology shifts your bug discoveries weeks or months earlier by using abstraction models that allow existing formal tools to handle the complexity of formal sign-off.
Our methodology ensures that your configurable IPs are proven for all cases – even those that have not seen production silicon.
If you later modify your RTL, our follow-on proofs are also exhaustive.
Oski’s End-to-End Formal Verification Sign-Off Methodology
Oski’s end-to-end formal verification sign-off methodology ensures that no bugs are left behind in the design areas that we formally sign-off.
Our process has been successfully deployed on hundreds of tape-outs to find all bugs very efficiently – including superbugs that would have likely slipped through simulation, emulation, and traditional formal verification methods.
Our process can be broken down into the four “Cs” of formal sign-off.
The 4 C’s of formal sign-off
End-to-end checkers are 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.
End-to-end checkers are coded in a distinct way to makes them suitable for formal verification. For example, they are lightweight and don’t add significant complexity to the state space of the model, which is important to ensure formal proofs converge.
By default, formal will explore all possible input stimulus, so it’s important to filter out the illegal input space with constraints to avoid false failures of the checkers. Care must also be taken to verify there are no over-constraints, which could mask real failures 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.
Traditional formal verification tends to run into barriers for complex designs, especially when dealing with end-to-end checkers.
This brings the requirement for the next element of our formal sign-off methodology — the abstraction models. (more details below)
The abstraction models reduce the state space or latency of the design so that formal verification can explore beyond its default threshold.
Formal coverage is a key component of the sign-off methodology. As with simulation, formal coverage metrics help measure controllability – how much of the design states has been covered by the input stimulus that has been explored.
Formal methods have a unique ability to report observability coverage, i.e. how much of the design states are being checked by the end-to-end checkers. This makes formal coverage a strong metric for measuring progress and closing verification holes.
Oski Formal Abstraction Models™
Formal Tools, Complexity, & State-Space Explosion
There is no formal tool on the market today that completely solves the problem of state-space explosion. Formal complexity can limit the applicability of formal tools.
As shown in the diagram, Oski Abstraction Models are key to getting the maximum benefit from our formal verification sign-off methodology and improving convergence with formal.
Formal complexity can limit formal tool applicability without Abstraction Models™
Oski Abstraction Models enable off-the-shelf EDA formal tools to scale.
Oski Abstraction Models Improve Convergence with Formal
The Oski Abstraction Models 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.
The models enable formal tools to analyze an alternate view of the design, and run thousands of times faster.
The result is convergence on end-to-end verification of designs as large as millions of state bits in the cone-of-influence of the verification problem.
Oski Abstraction Models: Highest Coverage & Faster Time to Market
Making the investment in formal does not guarantee convergence. Oski addresses the convergence problem by using our Abstraction Models to incorporate formal sign-off into the design flow, which enables the complementary strengths of formal verification and simulation to greatly improve chip-level verification closure before sign-off.
Oski’s Abstraction Models resolve 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.
The result is reduced schedule, increased coverage, and a better overall return on effort.