NDLI: Tutorial T4A: Formal Verification Techniques and Tools for Complex Designs

Content Provider	IEEE Xplore Digital Library
Author	Abraham, J.A. Saab, D.G.
Copyright Year	2007
Description	Author affiliation: Texas Univ., Austin, TX (Abraham, J.A.; Saab, D.G.)
Abstract	Integrated circuit technology has evolved from micro-controllers and discrete components to fully integrating a large system on a single chip (SoC). Today, verification is the most expensive component in the design cycle in term of cost and time. This cost is estimated to consume about 70% to 80% of the total design effort. The verification cost is expected to increase for SoC designs. This is mainly due to the increase in complexity and to the shrinking of the product design cycle. For example, the color TV took over 10 years to sell 1 million units, while the DVD player took just over a year. This shrinking of the design cycle is going to put more pressure on increasing designer productivity which is affected directly by the cost of verification. For these reasons, verification of complex designs is becoming a bottleneck in the process of producing integrated SoC systems. This tutorial provides an overview of emerging directions in formal verification and a discussion of new tools being developed in industry and research directions to enable automated verification of next generation systems on a chip. The tutorial will begin with a comprehensive overview of techniques for formally verifying complex designs. It will include the fundamental theory, applicability to different types of VLSI designs, as well as the performance and limitations of various approaches. The focus will be on Formal methods and will include both equivalence checking and property checking. Formal equivalence checking methods (between RTL and gate levels) incorporated into industry tools will be described, as well as new techniques for checking the equivalence between electronic system languages (such as SystemC) and RTL. The basics of property checking techniques in existing tools will be described, including the basics of model checking, and search algorithms that automatically show the correctness/violation of a property. Limitation and benefits of both SATisfiability and automatic test pattern generation (ATPG) based bounded model property checking (BMC) will be described. In order to deal with complexity, powerful model abstractions which can be automatically generated from static analysis of the RTL descriptions will be introduced. These include functional partitioning, static slicing and antecedent conditional slicing. These techniques can be used with existing tools to reduce their CPU and memory requirements while producing exactly the same results. This would be of particular interest to verification engineers and designers
Sponsorship	VLSI Soc. of India IEEE CAS Soc. IEEE ED Soc. ACM IEEE SSC Soc
Starting Page	6
Ending Page	6
File Size	168434
Page Count	1
File Format	PDF
ISBN	0769527620
ISSN	10639667
DOI	10.1109/VLSID.2007.168
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	2007-01-06
Publisher Place	India
Access Restriction	Subscribed
Rights Holder	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Content Type	Text
Resource Type	Article
Subject	Electrical and Electronic Engineering Hardware and Architecture

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