NDLI: Formal verification of digital systems by automatic reduction of data paths

Content Provider	IEEE Xplore Digital Library
Author	Macii, E. Plessier, B. Somenzi, F.
Copyright Year	1982
Abstract	Verification of properties (tasks) on a system P containing data paths may require too many resources (memory space and/or computation time) because such systems have very large and deep state spaces. As pointed out by Kurshan, what is needed is a reduced system P' which behaves exactly as P with respect to the properties that must be proved, but more compact than P, so that the verification can be easily performed. The process of finding P' from P is called reduction. P is specified by a network of interacting finite-state machines for data paths and controllers, and tasks are specified by finite-state automate. The verification of a task T on P is performed by the language containment check L(P)/spl sube/L(T), where L(P) is the language generated by P and L(T) is the language accepted by T. It has been shown that, under appropriate conditions, the system P can be reduced to P' and the task T to T' such that L(P')/spl sube/L(T')/spl hArr/L(P)/spl sube/L(T). The direct language containment check L(P)/spl sube/L(T) is no longer needed; it is replaced by L(P')/spl sube/L(T'), which is less expensive. More specifically, for the purpose of simplifying the verification of some properties, the system implementation is abstracted locally with respect to the behavior under observation (i.e., bottom-up reduction), in the context of an integrated top-down design/verification technique. The tasks that one may want to verify can express both safety and fairness constraints. In this paper, we prove that the reduction of some data paths to four-state, nondeterministic finite-state machines, and the redundancy removal performed on the controllers is a homomorphic transformation, so that the simplified language containment check can automatically be applied without testing the validity of the homomorphism. This homomorphism correctness verification, required when a formal proof is not available, can be executed using a tool like Cospan, but it may not be completed when the state space to be traversed is too large and deep. The redundancy removal performed on the controllers is important because it eliminates the spurious behaviors introduced in the system by the nondeterminism of the reduced data paths. Redundancy, in fact, may induce a failure in the verification of L(P')/spl sube/L(T'), while L(P)/spl sube/L(T) actually holds. In order to show the effectiveness of the proposed methodology, we verify properties on an extended version of the Mead-Conway Traffic Light Controller, on a modified IRQ communication protocol, and on a relatively prime integers checker and generator.
Sponsorship	IEEE Council on Electronic Design Automation IEEE Circuits and Systems Society
Starting Page	1136
Ending Page	1156
Page Count	21
File Size	818755
File Format	PDF
ISSN	02780070
Volume Number	16
Issue Number	10
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	1997-10-01
Publisher Place	U.S.A.
Access Restriction	One Nation One Subscription (ONOS)
Rights Holder	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Subject Keyword	Formal verification Digital systems State-space methods Automatic control Communication system traffic control Safety Performance evaluation Automatic testing Control systems Lighting control
Content Type	Text
Resource Type	Article
Subject	Computer Graphics and Computer-Aided Design Electrical and Electronic Engineering Software

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

Synthesis of Hardware for the Control of Digital Systems

A Survey of Automated Techniques for Formal Software Verification

Design-Intent Coverage—A New Paradigm for Formal Property Verification

Modular verification of timed circuits using automatic abstraction

A Compositional Method With Failure-Preserving Abstraction for Asynchronous Design Verification

Automated Synthesis of Data Paths in Digital Systems

Formal verification of sequential hardware: a tutorial

Compositional Reachability Analysis for Efficient Modular Verification of Asynchronous Designs

Formal Hardware/Software Co-Verification of Embedded Power Controllers

Formal verification of digital systems by automatic reduction of data paths

Similar Documents

Synthesis of Hardware for the Control of Digital Systems

A Survey of Automated Techniques for Formal Software Verification

Design-Intent Coverage&#8212;A New Paradigm for Formal Property Verification

Modular verification of timed circuits using automatic abstraction

A Compositional Method With Failure-Preserving Abstraction for Asynchronous Design Verification

Automated Synthesis of Data Paths in Digital Systems

Formal verification of sequential hardware: a tutorial

Compositional Reachability Analysis for Efficient Modular Verification of Asynchronous Designs

Formal Hardware/Software Co-Verification of Embedded Power Controllers

Formal verification of digital systems by automatic reduction of data paths

Design-Intent Coverage—A New Paradigm for Formal Property Verification