Report On Chelsio’s DAC Case Study In Formal Verification

23 Aug 2010 • 2 minute read

As the leader of the Formal Verification R&D team, I'm always fascinated by the many ways our customers apply the tools we build. This year's Design Automatic Conference (DAC 2010) in Anaheim, CA, provided a wealth of examples thanks to a whole user track dedicated to "Case Studies in Formal Verification". The first paper in this series was titled "Leveraging Formal Techniques for Packed Based Designs," presented by B.A. Krishna from Chelsio Communications. You can obtain both the video and presentation for the entire user track from the DAC website (details listed below). Here are my impressions of their cutting edge work.

This is an interesting case study where the designer (Anamaya Sullerey) and the verification engineer (B.A. Krishna) collaborated to do end-to-end formal verification on a Ethernet Packet Switch block. This is a fairly complex, high-density block (around 650K gates) with 18 internal modules. Krishna and Anamaya collaborated to perform formal verification on 14 of the most complex modules in this block. The collaboration started pretty early in the design process, where Anamaya designed this block with formal verification techniques in mind. As an example, he made the modules highly parameterizable, and had clear, crisp interfaces with rigorous specifications.

The paper then zooms in on one of the modules inside the block, the "Page Manager" module. This was a particularly critical module since bugs in this circuit could result in hangs or data corruption. Krishna wrote various end-to-end properties on this module including liveness properties like "All page allocation requests should be eventually satisfied." Krishna also used several techniques to handle the complexity of this block. Specifically, he used Wolper's data independence theorem and symmetry reductions to prove data integrity for the FIFOs in the module. He also used manual abstractions to abstract the Free List Manager into a single "Magic Page" that tracked the entire life cycle of a page during normal operation.

Krishna and Anamaya used the Incisive Formal Verifier (IFV) tool from Cadence to perform verification on the 14 modules in Ethernet Packet Switch block. Over the course of the 6 month project, they found 55 bugs using IFV, out of which 52 were deemed to be critical. After IFV based formal verification, testbench based simulation found only 3 additional bugs. These 3 bugs slipped past formal verification due to missing properties and incorrect assumptions. There were no bugs found in this block later during emulation and bring up. Even better: of the 14 modules that were formally verified, all were deemed tapeout ready more than 2 months before the other blocks.

This is a very useful case study that shows that formal verification can be used early in the design process and can find critical bugs in complex modules. I would encourage you view the video and presentation of this paper at the links mentioned below:

Video link for the DAC user track - http://www2.dac.com/videos+from+dac+user+track+videos.aspx

Presentation link for the DAC user track - http://www2.dac.com/user+track+poster+slides.aspx

Alok Jain
Distinguished Engineer
Cadence R&D
(and Team Verify member!)