NDLI: Model checking if your life depends on it: a view from Intel's trenches

Please wait, while we are loading the content...

From model checking to a temporal proof

Model checking if your life depends on it: a view from Intel's trenches

Model-checking infinite state-space systems with fine-grained abstractions using SPIN

Implementing LTL model checking with net unfoldings

Directed explicit model checking with HSF-SPIN

Addressing dynamic issues of program model checking

Automatically validating temporal safety properties of interfaces

Verification experiments on the MASCARA protocol

Using SPIN for feature interaction analysis—a case study

Behavioural analysis of the enterprise JavaBeans component architecture

p2b: a translation utility for linking promela and symbolic model checking (tool paper)

Transformations for model checking distributed Java programs

Distributed LTL model-checking in SPIN

Parallel state space construction for model-checking

Model checking systems of replicated processes with spin

A SPIN-based model checker for telecommunication protocols

Modeling and verifying a price model for congestion control in computer networks using promela/spin

A model checking project at Philips research

Applications of model checking at Honeywell Laboratories

Coarse-granular model checking in practice

Model checking if your life depends on it: a view from Intel's trenches

Content Provider	ACM Digital Library
Author	Gerth, Rob
Abstract	Hardware design is considered one of the traditional areas for formal (property) verification (FPV); in particular for symbolic model checking. Indeed, Intel, SUN, Motorola and IBM all develop and deploy model checking tools to ensure design correctness. On the other hand, hardware design is hostile territory because of the huge effort companies traditionally invest in classical testing and validation techniques which tend to be much more automated, require less sophistication from users and which will, in fact, discover many errors when deployed on such a scale. For these reasons FPV will never fully supplant traditional validation.The real challenge lies in convincing processor design teams that diverting some of their validation resources to FPV leads to provably higher design quality. Complicating factors include the relatively high quality of traditional validation at least within Intel which raises the bar for FPV; and the fact that in high-performance processors design large parts of the RTL tends to remain unstable enough throughout the design to make it very hard to verify suitable micro-architectural abstractions. For these reasons, FPV within Intel traditionally targets the same RTL from which the schematics is derived and on which all traditional validation is performed.Arguably the biggest (public) FPV success story within Intel is that of floating point hardware verification and it is illustrative to see how FPV is deployed in this area and how tool and methodology development is influenced.The major challenge that we are now facing is to move formal verification upstream in the design flow. Not only because ever increasing micro-architectural complexity creates a strong demand for early verification on an algorithmic level, but also because the ever shortening design cycle forces formal verification to start much earlier in the design. It is here that hardware FPV and software verification start to merge and there are lessons to be learned for either side.
File Format	PDF
ISBN	3540421246
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2001-05-02
Access Restriction	Subscribed
Content Type	Text
Resource Type	Article

Central Library (ISO-9001:2015 Certified)
Indian Institute of Technology Kharagpur
Kharagpur, West Bengal, India | PIN - 721302

See location in the Map
03222 282435
Mail: support@ndl.gov.in

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