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.
Coverage of Formal Properties based on a High-Level Fault Model and Functional ATPG
FUMMI, Franco;PRAVADELLI, Graziano;
2005-01-01
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.
File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
