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

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.