Design-intent coverage-a new paradigm for formal property verification

Basu, P. ; Das, S. ; Banerjee, A. ; Dasgupta, P. ; Chakrabarti, P. P. ; Mohan, C. R. ; Fix, L. ; Armoni, R. (2006) Design-intent coverage-a new paradigm for formal property verification IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 25 (10). pp. 1922-1934. ISSN 0278-0070

Full text not available from this repository.

Official URL: http://ieeexplore.ieee.org/document/1677681/

Related URL: http://dx.doi.org/10.1109/TCAD.2005.859490

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.

Item Type:Article
Source:Copyright of this article belongs to Institute of Electrical and Electronics Engineers.
Keywords:Chip Scale Packaging; Space Technology; Explosions; Formal Verification; Circuit Testing; State-space Methods; Government; Computer Science; Pipeline Processing; Design Optimization
ID Code:101440
Deposited On:12 Dec 2016 11:42
Last Modified:12 Dec 2016 11:42

Repository Staff Only: item control page