Home > Community > Blogs > Functional Verification > report on chelsio s dac user track case studies in formal verification paper
 
Login with a Cadence account.
Not a member yet?
Create a permanent login account to make interactions with Cadence more conveniennt.

Register | Membership benefits
Get email delivery of the Functional Verification blog (individual posts).
 

Email

* Required Fields

Recipients email * (separate multiple addresses with commas)

Your name *

Your email *

Message *

Contact Us

* Required Fields
First Name *

Last Name *

Email *

Company / Institution *

Comments: *

Report On Chelsio’s DAC Case Study In Formal Verification

Comments(0)Filed under: Functional Verification, Formal Analysis, DAC, verification strategy, Incisive, ABV, formal, IFV

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!)

Follow us on Twitter: http://twitter.com/teamverify, @teamverify

 

Comments(0)

Leave a Comment


Name
E-mail (will not be published)
Comment
 I have read and agree to the Terms of use and Community Guidelines.
Community Guidelines
The Cadence Design Communities support Cadence users and technologists interacting to exchange ideas, news, technical information, and best practices to solve problems and get the most from Cadence technology. The community is open to everyone, and to provide the most value, we require participants to follow our Community Guidelines that facilitate a quality exchange of ideas and information. By accessing, contributing, using or downloading any materials from the site, you agree to be bound by the full Community Guidelines.