Discover how semiconductor leaders leverage
Oski's expertise to reduce verification cost and
Hard-to-verify block with low controllability and observability
Replace simulation with formal
A bus bridge between ARM® AMBA® and AXI3® bus and an internal bus, including a DMA controller. The original plan was to build a block-level constraint-based coverage-driven environment to achieve verification coverage.
A formal verification environment was built to provide the highest possible coverage. Oski Abstraction Models were used to reduce the formal verification complexity by orders of magnitude. Line coverage and functional coverage was measured to quantify the effectiveness of the formal verification environment.
Low-probability corner-case bugs were found early in the formal verification flow. Overall verification schedule was reduced by about 5x. Bug escapes that were almost impossible to detect in a simulation-only environment, were eliminated.
Complement simulation with a formal methodology to cover the configurable space
A highly configurable DDR3 Memory Controller IP, which allowed different build configurations related to number of channels, data width, internal FIFO depths, scheduling algorithms. The existing simulation environment was a set of directed and random tests.
A formal verification methodology to verify the configurable IP was developed. The end-to-end checkers were partitioned into classes, and mapped into the configuration space. Multiple values of configuration registers were allowed in same formal verification runs, achieving more coverage in significantly less total time than simulation. The formal verification components were reusable to do assume-guarantee proofs on the neighboring blocks. Formal checkers and constraints were instantiated in simulation. Coverage results from formal and simulation were manually integrated.
Develop an End-to-End formal testbench for an 8×8 multicast crossbar design, and invite users to try to break it by inserting functional bugs.
The “Break the Testbench” Challenge used a 8×8 multicast crossbar design, with 8 clients and 8 targets, where each client can send a request and associated data to multiple targets. The formal tool used for the Challenge was VC Formal, by Synopsys.
100% of the functional bugs were caught by the End-to-End formal testbench. Only 22 of the 73 functional bugs were caught by internal assertions, suggesting that assertion-based verification cannot catch all design bugs, and should not be used for Sign-off.