Coverage of Formal Properties Based on a High-Level Fault Model and Functional ATPG
- 7 June 2005
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- No. 15301877,p. 162-167
- https://doi.org/10.1109/ets.2005.12
Abstract
The use of model checking to validate descriptions of digital systems lacks a coverage metrics. If the set of formal properties defined to prove the correctness of the design is incomplete, the verification can lead to a false sense of security. This paper refines, extends, and compares with other symbolic approaches, a methodology to estimate the incompleteness of formal properties, which exploits a high-level fault model and functional ATPG.Keywords
This publication has 5 references indexed in Scilit:
- Coverage estimation for symbolic model checkingPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Coverage metrics for functional validation of hardware designsIEEE Design & Test of Computers, 2001
- ”Have I Written Enough Properties?” - A Method of Comparison Between Specification and ImplementationPublished by Springer Nature ,1999
- Efficient generation of counterexamples and witnesses in symbolic model checkingPublished by Association for Computing Machinery (ACM) ,1995
- Symbolic Model CheckingPublished by Springer Nature ,1993