Assertion-based verification (ABV) affirmed as an effective methodology for functional verification, i.e., design specification conformance, of embedded systems. Academia and industry have thoroughly investigated formal ABV for high-budget or safety-critical hardware and software projects, while the scalability of dynamic ABV has led to the introduction of standard languages and commercial tools addressing hardware design verification, emulation, and silicon debug. However, up to now, there were only limited studies concerning the application of dynamic ABV to embedded-software design and verification flow. We propose an analysis aiming to bridge such a gap. In particular, we illustrate how dynamic ABV can integrate and improve the various stages of the embedded-software verification flow. The analysis leads us to develop a comprehensive ABV environment that integrates the still missing automatic synthesis of executable checkers for embedded software. Experiments show that the proposed environment reduces the verification-team efforts and makes dynamic ABV practical for embedded-software design.

On the use of assertions for embedded-software dynamic verification

DI GUGLIELMO, Giuseppe;DI GUGLIELMO, Luigi;PRAVADELLI, Graziano;FUMMI, Franco
2012

Abstract

Assertion-based verification (ABV) affirmed as an effective methodology for functional verification, i.e., design specification conformance, of embedded systems. Academia and industry have thoroughly investigated formal ABV for high-budget or safety-critical hardware and software projects, while the scalability of dynamic ABV has led to the introduction of standard languages and commercial tools addressing hardware design verification, emulation, and silicon debug. However, up to now, there were only limited studies concerning the application of dynamic ABV to embedded-software design and verification flow. We propose an analysis aiming to bridge such a gap. In particular, we illustrate how dynamic ABV can integrate and improve the various stages of the embedded-software verification flow. The analysis leads us to develop a comprehensive ABV environment that integrates the still missing automatic synthesis of executable checkers for embedded software. Experiments show that the proposed environment reduces the verification-team efforts and makes dynamic ABV practical for embedded-software design.
9781467311878
assertions; embedded software; dynamic verification
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: http://hdl.handle.net/11562/407337
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact