Basu, P. ; Das, S. ; Dasgupta, P. ; Chakrabarti, P. P. ; Mohan, C. R. ; Fix, L. (2004) Formal verification coverage: are the RTL-properties covering the design's architectural intent? In: Design, Automation and Test in Europe Conference and Exhibition, 2004, 16-20 February 2004, Paris, France.
Full text not available from this repository.
Official URL: http://ieeexplore.ieee.org/document/1268922/
Related URL: http://dx.doi.org/10.1109/DATE.2004.1268922
Abstract
It is essential to formally ascertain whether the 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 limitation 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. In this paper we present: (1) a method for checking whether the RTL-properties are covering the architectural-properties, that is, whether verifying the RTL-properties guarantee the correctness of the design's architectural intent; and (2) a method to identify the coverage holes in terms of the architectural properties (or their sub-properties) that are not covered.
| Item Type: | Conference or Workshop Item (Paper) |
|---|---|
| Source: | Copyright of this article belongs to Institute of Electrical and Electronics Engineers. |
| Keywords: | Logic; Signal Design; Computer Science; Strategic Planning; Formal Verification; Design Automation; Automatic Testing; Europe |
| ID Code: | 101714 |
| Deposited On: | 19 Dec 2016 10:52 |
| Last Modified: | 19 Dec 2016 10:52 |
Repository Staff Only: item control page
