NDLI: Formal verification of an ASIC ethernet switch block

Content Provider	IEEE Xplore Digital Library
Author	Krishna, B.A. Sullerey, A. Jain, A.
Copyright Year	2010
Description	Author affiliation: Cadence Design Systems, Inc (Jain, A.) \|\| Chelsio Communications Inc (Krishna, B.A.; Sullerey, A.)
Abstract	Traditionally, validation at the ASIC block level relies primarily upon simulation based verification. Specific components that are “hot spots” are then considered as candidates for Formal Verification. Under this usage model, the hurdles to Formal Verification are intractability and poor specifications. In this paper, we outline an alternate approach, where we used Formal Verification as the “first line of defense” in the course of validating a Packet Switch. This block had several components that were complex and hard to verify, including components that required liveness guarantees, where responses are event bound, and not cycle bound. To surmount typical hurdles, an early collaboration was formed between design and verification engineer, both to influence the design as well as to identify relevant manual abstraction techniques upfront. All significant components were formally verified at the module level. This approach was successful in identifying most bugs during the design phase itself and drastically minimized bugs during verification/emulation phases of the project. This paper illustrates the strengths of such an approach. It describes our overall methodology and the proof techniques utilized. The overall effort yielded a total of 55 bugs found (52 during the design phase and only 3 bugs during the verification phase). No bugs were found subsequently during emulation. As a result, this block was deemed “tape out ready” 2 months prior to other blocks of similar complexity.
Starting Page	13
Ending Page	20
File Size	330562
Page Count	8
File Format	PDF
ISBN	9781457707346
e-ISBN	9780983567806
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	2010-10-20
Publisher Place	Switzerland
Access Restriction	Subscribed
Rights Holder	FMCAD Inc
Subject Keyword	Computer bugs Switches Logic gates Complexity theory Synchronization Resource management Formal verification
Content Type	Text
Resource Type	Article

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Formal Verification of an ASIC Ethernet Switch Block

Clock gating assertion check: An approach towards achieving faster verification closure on clock gating functionality

Functional verification of logic modules for a Gigabit Ethernet switch

A semi-formal verification methodology

An Efficient Framework for Processor Verification

Automated methods for eliminating X bugs

Verifying a gigabit ethernet switch using SMV

Strategies for the interconnection of CAN buses through an Ethernet switch

A new generation of ISCAS benchmarks from formal verification of high-level microprocessors

Formal verification of an ASIC ethernet switch block

Similar Documents

Formal Verification of an ASIC Ethernet Switch Block

Clock gating assertion check: An approach towards achieving faster verification closure on clock gating functionality

Functional verification of logic modules for a Gigabit Ethernet switch

A semi-formal verification methodology

An Efficient Framework for Processor Verification

Automated methods for eliminating X bugs

Verifying a gigabit ethernet switch using SMV

Strategies for the interconnection of CAN buses through an Ethernet switch

A new generation of ISCAS benchmarks from formal verification of high-level microprocessors

Formal verification of an ASIC ethernet switch block