Since the mid 1990s, Model-Driven Design (MDD) methodologies have aimed at raising the level of abstraction through an extensive use of generic models in all the phases of the development of embedded systems. MDD describes the system under development in terms of abstract characterization, attempting to be generic not only in the choice of implementation platforms, but even in the choice of execution and interaction semantics. Thus, MDD has emerged as the most suitable solution to develop complex systems and has been supported by academic and industrial tools. The gain offered by the adoption of an MDD approach is the capability of generating the source code implementing the target design in a systematic way, i.e., it avoids the need of manual writing. However, even if MDD simplifies the design implementation it does not prevent the designers from wrongly defining the design behavior. Therefore, MDD gives full benefits if it also integrates functional verification. In this context, Assertion Based Verification (ABV) has emerged as one of the most powerful solutions for capturing a designer’s intent and checking their compliance with the design implementation. In ABV, specifications are expressed by means of formal properties. These overcome the ambiguity of natural languages and are verified by means of either static (e.g., model checking) or, more frequently, dynamic (e.g., simulation) techniques. Therefore ABV provides a proof of correctness for the outcome of the MDD flow. Consequently, the MDD and ABV approaches have been combined to create efficient and effective design and verification frameworks that accompany designers and verification engineers throughout the system-level design flow of complex embedded systems, both for the Hardware (HW) and the Software (SW) parts. It is, indeed, worth noting that to achieve a high degree of confidence, such frameworks require to be supported by functional qualification methodologies, which evaluate the quality of both the properties and the testbenches which are adopted during the overall flow. In this context, the goal of the chapter consists of providing, first, a general introduction to MDD and ABV concepts and related formalisms, and then a more detailed view on the main challenges concerning the realization of an effective semiformal ABV environment through functional qualification.

Semiformal Assertion-Based Verification of Hardware/Software Systems in a Model-Driven Design Framework / Pravadelli, Graziano; Quaglia, Davide; Vinco, Sara; Fummi, Franco - In: Handbook of Hardware/Software Codesign / Soonhoi Ha, Jürgen Teich. - [s.l] : Springer Netherlands, 2017. - ISBN 978-94-017-7266-2. - pp. 683-720 [10.1007/978-94-017-7358-4_23-2]

Semiformal Assertion-Based Verification of Hardware/Software Systems in a Model-Driven Design Framework

QUAGLIA, Davide;VINCO, SARA;FUMMI, FRANCO
2017

Abstract

Since the mid 1990s, Model-Driven Design (MDD) methodologies have aimed at raising the level of abstraction through an extensive use of generic models in all the phases of the development of embedded systems. MDD describes the system under development in terms of abstract characterization, attempting to be generic not only in the choice of implementation platforms, but even in the choice of execution and interaction semantics. Thus, MDD has emerged as the most suitable solution to develop complex systems and has been supported by academic and industrial tools. The gain offered by the adoption of an MDD approach is the capability of generating the source code implementing the target design in a systematic way, i.e., it avoids the need of manual writing. However, even if MDD simplifies the design implementation it does not prevent the designers from wrongly defining the design behavior. Therefore, MDD gives full benefits if it also integrates functional verification. In this context, Assertion Based Verification (ABV) has emerged as one of the most powerful solutions for capturing a designer’s intent and checking their compliance with the design implementation. In ABV, specifications are expressed by means of formal properties. These overcome the ambiguity of natural languages and are verified by means of either static (e.g., model checking) or, more frequently, dynamic (e.g., simulation) techniques. Therefore ABV provides a proof of correctness for the outcome of the MDD flow. Consequently, the MDD and ABV approaches have been combined to create efficient and effective design and verification frameworks that accompany designers and verification engineers throughout the system-level design flow of complex embedded systems, both for the Hardware (HW) and the Software (SW) parts. It is, indeed, worth noting that to achieve a high degree of confidence, such frameworks require to be supported by functional qualification methodologies, which evaluate the quality of both the properties and the testbenches which are adopted during the overall flow. In this context, the goal of the chapter consists of providing, first, a general introduction to MDD and ABV concepts and related formalisms, and then a more detailed view on the main challenges concerning the realization of an effective semiformal ABV environment through functional qualification.
2017
978-94-017-7266-2
Handbook of Hardware/Software Codesign
File in questo prodotto:
Non ci sono file associati a questo prodotto.
Pubblicazioni consigliate

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/11583/2651305
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo