Title :
Do´s and don´ts of CTL state coverage estimation
Author :
Jayakumar, Nikhil ; Purandare, Mitra ; Somenzi, Fabio
Author_Institution :
Univ. of Colorado, Boulder, CO, USA
Abstract :
Coverage estimation for model checking quantifies the completeness of a set of properties. We present an improved version of the algorithm of Hoskote et al. (1999) that applies to a larger subset of CTL; we prove properties of the algorithm and apply it to three case studies. From these case studies we derive recommendations for an effective use of coverage estimation.
Keywords :
formal verification; integrated circuit modelling; logic CAD; state estimation; CTL estimation; CTL larger subset; algorithm properties; coverage estimation; model checking; state coverage; vacuity detection; Algorithm design and analysis; Contracts; Labeling; Logic design; Permission; State estimation;
Conference_Titel :
Design Automation Conference, 2003. Proceedings
Print_ISBN :
1-58113-688-9
DOI :
10.1109/DAC.2003.1219011
