Internal Bus Bridge

Challenge

Hard-to-verify block with low controllability and observability

Solution

Replace simulation with formal

Success

  1. Dramatically reduced formal verification complexity
  2. Reduced overall verification schedule by 5x
  3. Eliminated bug escapes almost impossible to detect in a simulation-only environment

Design

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.

Proposal

  1. Replace block-level simulation with formal verification.
  2. Reduce the overall verification schedule.
  3. Achieve higher quantitative verification coverage.

Results

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.

DDR3 Memory Controller IP

Challenge

  1. Verify highly configurable designs
  2. Improve sanity testing across large configurable space
  3. Improve coverage

Solution

Complement simulation with a formal methodology to cover the configurable space

Success

  1. Decreased functional coverage holes by more than 20x
  2. Reduced verification code by 10x
  3. Delivered methodology for verifying configurable IPs

Design

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.

Proposal

  1. Complement simulation with a configurable formal verification implementation
  2. Define a coverage methodology to maximize simulation and formal coverage, verifying multiple configurations in the same run

Results

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.

A Case Study for the Completeness of End-to-End Formal

Challenge

    To demonstrate the completeness of our End-to-End formal testbench and the viability of using formal verification for sign-off.

  1. Deploy an End-to-End formal testbench for an 8×8 multicast crossbar design that can catch 100% of functional bugs.
  2. Demonstrate that that assertion-based verification cannot catch all design bugs

Solution

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.

Success

  1. Of the 73 functional bugs were inserted, 100% were caught
  2. This challenge established the viability of using End-to-End Formal for Sign-off

Design

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.

Proposal

  1. Use an End-to-End formal testbench to demonstrate the completeness of formal
  2. Create a challenge that allows users to review the design, insert functional bugs, then run the testbench to see the newly introduced bugs being caught in real time. 

Results

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.

Management
Career
Media
Contact