Verification of circuit description by means of model checking means to write propositions, expressed in some temporal logic, expected to be true on the implementation according to the specification content. Completeness of the set of written properties is still an open problem. We propose a practical approach to the property coverage metrics definition based on fault injection; a combination of model checking, fault simulation and emulation allows to reduce the coverage measure to an affordable task. The application of these three different technologies is illustrated on a real example, on which it leads to the discovery of a missing property in a property set formerly trusted to be complete.

A 1000X Speed Up for Properties Completeness Evaluation

FIN, Alessandro;FUMMI, Franco;PRAVADELLI, Graziano;
2002-01-01

Abstract

Verification of circuit description by means of model checking means to write propositions, expressed in some temporal logic, expected to be true on the implementation according to the specification content. Completeness of the set of written properties is still an open problem. We propose a practical approach to the property coverage metrics definition based on fault injection; a combination of model checking, fault simulation and emulation allows to reduce the coverage measure to an affordable task. The application of these three different technologies is illustrated on a real example, on which it leads to the discovery of a missing property in a property set formerly trusted to be complete.
2002
0780376552
Emulation; ATPG; Testing
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.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11562/16349
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 5
  • ???jsp.display-item.citation.isi??? 5
social impact