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

Content Provider	IEEE Xplore Digital Library
Author	Basu, P. Das, S. Banerjee, A. Dasgupta, P. Chakrabarti, P.P. Mohan, C.R. Fix, L. Armoni, R.
Copyright Year	1982
Abstract	It is essential to formally ascertain whether the register-transfer level (RTL) validation effort effectively guarantees the correctness with respect to the design's architectural intent. The design's architectural intent can be expressed in formal properties. However, due to the capacity limitations of formal verification, these architectural properties cannot be directly verified on the RTL. As a result, a set of lower level RTL properties are developed and verified against the RTL modules. In a top-down design approach, the architect would ideally like to formally guarantee the coverage of the architectural intent at the time of creating the specifications for the component RTL modules (that is, before they are passed to the designers for implementation). In this paper, the authors present: 1) a method for checking whether the RTL properties are covering the architectural properties, that is, whether verifying the RTL properties guarantees the correctness of the design's architectural intent; 2) a method to identify which architectural properties are still uncovered, that is, not guaranteed by the RTL properties; and 3) a methodology for representing the gap between the specifications in a legible form
Sponsorship	IEEE Council on Electronic Design Automation IEEE Circuits and Systems Society
Starting Page	1922
Ending Page	1934
Page Count	13
File Size	268176
File Format	PDF
ISSN	02780070
Volume Number	25
Issue Number	10
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	2006-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	Chip scale packaging Space technology Explosions Formal verification Circuit testing State-space methods Government Computer science Pipeline processing Design optimization functional coverage
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

POWER-TRUCTOR: An Integrated Tool Flow for Formal Verification and Coverage of Architectural Power Intent

Automated Interface Refinement for Compositional Verification

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

Using Transfer-Resource Graph for Software-Based Verification of System-on-Chip

Compositional Reachability Analysis for Efficient Modular Verification of Asynchronous Designs

Statistical Static Timing Analysis Considering Process Variation Model Uncertainty

Analyzing Functional Coverage in Bounded Model Checking

Fine-grained transaction-level verification: using a variable transactor for improved coverage at the signal level

Optimizing interacting finite state machines using sequential don't cares

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

Similar Documents

POWER-TRUCTOR: An Integrated Tool Flow for Formal Verification and Coverage of Architectural Power Intent

Automated Interface Refinement for Compositional Verification

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

Using Transfer-Resource Graph for Software-Based Verification of System-on-Chip

Compositional Reachability Analysis for Efficient Modular Verification of Asynchronous Designs

Statistical Static Timing Analysis Considering Process Variation Model Uncertainty

Analyzing Functional Coverage in Bounded Model Checking

Fine-grained transaction-level verification: using a variable transactor for improved coverage at the signal level

Optimizing interacting finite state machines using sequential don't cares

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

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