- End-to-End Formal TM Verification
- Late-Stage ECOs and Post-Silicon Debug
- Trouble Shooting Formal Verification Challenges
- Pre- and Post- Clock-Gated Design Verification
- Formal & Simulation Coverage Closure
- Bypass Functionality for Operational Designs
Oski Formal Services include many components as shown in the picture below.
Many customers consult with Oski to implement Oski Formal Methodology as part of their verification sign-off flow. Oski gets involved from the beginning of the real project cycle to perform Formal Test-planning and stays involved all the way to the final Formal Training & Consulting stage. After the project, our customers are equipped with applying Oski Formal Methodology on their own in future projects. Customers enjoy both short-term benefits of formally verified design and long-term benefits of having a sound formal verification methodology in place to enable formal sign-off.
Other customers consult with Oski on certain activities, such as Formal Troubleshooting where Oski comes in and helps them understand the challenges in applying formal technology and crafts custom Abstraction Models to overcome the complexity barrier. Customers learn how to write the Abstraction Models and can leverage the newly developed expertise in future projects.
Whatever ways that works for you, Oski can help. See the types of projects we have done with our customers.
End-to-End FormalTM Verification
There are different levels of checkers one can write and deploy formal technology on, with different level of difficulties and benefits.
Local Assertions are internal RTL assertions (often embedded in RTL itself) that are easier to verify. Interface Assertions relate to inputs and outputs of the design, such as ACE, AXI4, OCP, DDR2 protocols. These are harder to verify compared to Local Assertions. End-to-End Checkers model End-to-End functionality, often requires Abstraction Models to manage complexity and therefore are hardest to verify. But to replace simulation completely for a block, End-to-End Checkers are needed. Though End-to-End Checkers require the most time and effort, the benefits of complete verification of End-to-End functionality of the block exhaustively that would otherwise be harder to achieve using simulation make it a worth well effort.
Often customers deploy formal technology only to verify Local and Interface Assertions. In order to make the best use of formal technology to replace simulation on suitable blocks, customers often consult Oski to perform End-to-End verification on certain blocks and learn from this experience. Success of End-to-End formal verification on certain blocks often lead to customers deploying formal more extensively by implementing Oski Formal Methodology as part of the whole verification strategy.
End-to-End formal verification conducted by Oski is a good starting point to see what Oski can do and the benefits of Oski Formal Methodology.
Late-Stage ECOs and Post-Silicon Debug
Often customers come to Oski because they have run into design bugs late stage in the project cycle or post silicon and wanted to know if formal could have caught such issues and to make sure this situation is avoided in future projects. Most of the times such design bugs could have been caught early with formal technology due to its exhaustive nature in catching corner-case bugs and hence late stage ECO can be avoided.
This often is a triggering event and acts as a changing agent in customers adopting formal technology more broadly in their verification flow. Oski has performed many projects starting from helping customers find the same bugs using formal technology and ending up implementing Oski Formal Methodology to enable Formal Sign-off.
Trouble Shooting Formal Verification Challenges
Formal verification offers many benefits, but it is also inherently complex due to the state space explosion problem – i.e. the search space increases exponentially:
- For a small design with 10 flops, the exhaustive search space is 1024,
- 20 flops, 1,048,756 (> 1 million)
- 30 flops, 1,073,741,824 (> 1 billion)
Today blocks often have hundreds and even hundreds of thousands flops. Applying formal technology in a brute force manner often leads to many time-outs and in-conclusive results.
Customers often come to Oski when they run into complexity barrier in applying formal technology. A key component in Oski Formal Methodology is the development of custom Abstraction Models to overcome the complexity barrier so formal technology can be applied to much larger and more complex blocks.
An Abstraction Model represents a superset of the design behavior and it effectively brings far away states closer to the reset states, so formal verification can converge. Writing abstraction models requires creativity. If an Abstraction Model is too coarse, then we run into false negatives. If it is too fine, then the verification proof may not converge. Hence it takes experience to quickly identify the complexity challenge and craft a solution to solve the challenge. But this is a learned skill and through our projects we teach our customers how to write Abstraction Models so they can apply this technique in future projects.
Pre- and Post- Clock-Gated Design Verification
Clock gating is a technique used to reduce power usage. The default verification strategy for a clock-gated design is to run the set of golden tests from the pre-clock-gated design on the post-clock-gated design, with the assumption that the golden test suite exercises all corner-cases when clocks become gated. However this is not always true, especially in less aggressive clock-gating schemes when clock-gating is enabled in rare corner-case situations, that makes it harder to cover with a given set of tests.
The best strategy is to use sequential equivalence checking tools for RTL vs. RTL comparison. This is a much harder computational problem than combinational equivalence checking and thus has capacity limitation. As a result, Oski is often consulted to simplify the verification problem to manageable scale, such as adding cut-points at architectural state points and registers, or modeling clock gating cell to make it friendly for formal tools. Oski has engaged in many projects to ensure successful verification of pre- and post- clock-gated designs.
Formal & Simulation Coverage Closure
Coverage data such as line or expression coverage is often used in simulation as a sign-off criterion for finishing functional verification. For formal verification to become a sign-off criterion in an advanced verification methodology, formal coverage (such as line coverage) is needed to ensure the set of constraints are appropriate and the proof depth is sufficient. Recently years coverage features have been added to advanced formal verification tools to make formal coverage data available as a measure for formal sign-off.
Oski has been involved in projects that help user perform formal coverage, interpret formal coverage results and incorporate such results with simulation coverage for formal and verification sign-off.
Bypass Functionality for Operational Designs
Deeply pipelined designs are susceptible to the problem of data hazards between multiple operations (or instructions). Such hazards arise when execution of one operation depends on the result of one or more previous operations, and the results of previous operations are not available directly from the pipeline registers. One easy solution is to stall the pipeline when such hazards are detected. This decreases the throughput of the system. An alternative is to build bypass logic (also called forwarding logic) so that results from later stages in the pipeline can be muxed into previous stages. Adding bypass logic comes with a significant increase in verification complexity; it is hard to cover all possible corner cases exercised by the bypass logic.
Oski has applied model checking to establish correctness of the bypass logic in many processor and networking designs and found corner case bugs that are almost impossible to find with simulation. Again End-to-End checks combined with custom abstraction models made it possible to formally verify the bypass functionality. This is also a case whereby both simulation and formal verification are needed to verify the same block, albeit different part of the functionalities.