NDLI: Formal Verification of Systems-on-Chip - Industrial Experiences and Scientific Perspectives

Content Provider	IEEE Xplore Digital Library
Author	Stoffel, D.
Copyright Year	2009
Abstract	Even after years of progress in the field of formal property checking many system designers in industry still consider simulation as their most powerful and versatile instrument when verifying complex systems-on-chip (SoCs). Often, formal techniques are only conceded a minor role. At best, they are viewed as nice-to-have and may be employed in addition to simulation, e.g. for "bug hunting'' in corner cases. Fortunately, in some parts of industry, a paradigm shift can be observed. Verification methodologies have emerged that involve property checking comprehensively, and in a systematic way. This has led to major innovations in industrial design flows. There are more and more applications where formal property checking does not only complement but replace simulation. In this talk, experiences from large-scale industrial projects are reported documenting this emancipation process of property checking. A systematic methodology is presented as it has established in some industries. Furthermore, there will be an attempt to identify the bottlenecks of today's technology and to outline specific scientific challenges. While formal property checking for individual SoC modules can be considered quite mature it is well-known that there are tremendous obstacles when moving from modules to the entire system. These problems do not only result from the sheer size of the system but also from the different nature of the verification problems. The presented analysis will also relate to well-known abstraction approaches and to techniques for state space approximation. More specifically, as a first step towards formal chip-level verification, the talk will discuss techniques for verifying communication structures (interfaces) between the individual SoC modules. New ideas will be outlined how certain abstraction techniques can be tailored towards a specific verification methodology such that correctness proofs become tractable even for complex SoC interfaces.
Starting Page	3
Ending Page	3
File Size	89697
Page Count	1
File Format	PDF
ISBN	9780769537634
ISSN	15294188
DOI	10.1109/DEXA.2009.83
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	2009-08-31
Publisher Place	Austria
Access Restriction	Subscribed
Rights Holder	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Subject Keyword	Formal verification Computer industry Databases Expert systems Application software Power engineering computing Data engineering Design engineering Power engineering and energy Computational modeling property checking system on chip 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

Simulation-guided property checking based on multi-valued AR-automata

The Application of Visualization in Scientific Computing Technology to Architectural Design

A formal verification methodology for checking data integrity

Embedding Formal Methods into Systems Engineering

Formal Verification of a Gravity-Induced Loss-of-Consciousness Monitoring System for Aircraft

The application of expert system on electrochemistry rectifying power supply CAD

Rapid prototyping of computer systems: experiences and lessons

A Verification Framework for FBD Based Software in Nuclear Power Plants

Decoupling synchronization from local control for efficient symbolic model checking of statecharts

Formal Verification of Systems-on-Chip - Industrial Experiences and Scientific Perspectives

Similar Documents

Simulation-guided property checking based on multi-valued AR-automata

The Application of Visualization in Scientific Computing Technology to Architectural Design

A formal verification methodology for checking data integrity

Embedding Formal Methods into Systems Engineering

Formal Verification of a Gravity-Induced Loss-of-Consciousness Monitoring System for Aircraft

The application of expert system on electrochemistry rectifying power supply CAD

Rapid prototyping of computer systems: experiences and lessons

A Verification Framework for FBD Based Software in Nuclear Power Plants

Decoupling synchronization from local control for efficient symbolic model checking of statecharts

Formal Verification of Systems-on-Chip - Industrial Experiences and Scientific Perspectives