Vertigo - Verification and Validation of Embedded System Design Workbench

The Project

Table of Contents

Embedded Systems are built on top of SW and HW capabilities. It is economically convenient to exploit common HW solutions among different applications, through the use of platform based design and architectures based on configurable logic HW.

A recurrent problem for the HW integrator is to validate a specific architecture without the knowledge of the final application(s). The development ofSW/HW co-simulation methods and related coverage metrics applied to this field are vital to achieve the verification of the embedded system platform.

The verification framework is often constituted by a mixof SW, TLM, RTL. In this context the main goal of the VERTIGO project is the development of a systematic methodology to combine a simulation-based approach (dynamic verification) together with formal methods (static verification) integrated into an IP-cores and platform based design flow, for the purpose of producing a SW kit applied to the platform validation.

Such system level based design verification flow must solve three main problems:

Verification of the correct interaction between all IP-cores and of the system in the networked environment, driven by coverage metrics
Production of a SW layer for the purpose of the embedded platform test
Verification of the correct modelling of system-level IP-cores and their correct mapping into RTL descriptions, driven by formal verification

The solution of these problems require to correctly integrate verification and design into a robust flow, to smoothly move from verification languages (e.g., SystemC, System Verilog) to RTL languages, to combine dynamic and static verification techniques, thus exploiting and composing a variety of verification engines (e.g., SAT, High-Level Decision Diagrams, Hierarchical Petri Nets, EFSMs, etc.).

VERTIGO addresses a new generation of technologies and tools for modelling and testing embedded platforms, that will be the foundation for a viable and cost-efficient mapping of HW/SW systems embedded in intelligent devices.

Rationale

The advent of IP-cores and platform based design paradigm has enabled the integration of ever more powerful Embedded Platforms, including a lot of options that enable the system to interact with the surrounding environment via networked connections. A large number of protocols have been developed for the purpose, e.g. PCI, Ethernet, USB, CAN, SPI, SMIA etc. Embedded Platforms take a great advantage from the increasing integration at disposal, making it possible to implement a full system in a single package.

As today’s design methodologies are moving to consider a Transactional Level Model (TLM) of the system as a starting point, the description of SW and HW components becomes very similar. A TL system model is a set ofIP-cores (IPs) described at the system level that execute, communicate and synchronize; at this stage it is very natural to interface TL HW blocks with SW modules, thanks also to the similarity of the respective languages like SystemC/C++, and to proceed by partitioning (SW/HW) and by refinement (behavioural synthesis) down to the familiar RTL.

However the high-level synthesis step is still immature for industrial use and in reality the Embedded Platform must be verified either by HW emulation/acceleration or by a composite environment of different modules in SW, TLM (to speed up the execution of certain tasks) and RTL.

It is estimated that 70% of the design cycle for systems is spent on verification. The verification of the architecture integration itself represents more than 50% of the verification effort, especially when SW/HW interaction is taken into account. Enhancing productivity and reliability of the system verification flow is thus a key competitive aspect, both in terms of time to market and end-product quality.

VERTIGO flow

The VERTIGO project is structured in five technical workpackages covering, respectively the definition of requirements (WP1), the extensions of verification and modelling technologies (WP2), the verification of IPs modelling and synthesis (WP3), the verification of IPs interaction (WP4) and the application and validation of the VERTIGO flow on the selected families of platforms (WP5).

Moreover, as needed for good project behaviour, two additional workpackages are added: WP6 concerns dissemination and exploitation while WP7 is for project management.

Let us now detail the technical workpackages by using the description of the VERTIGO verification flow depicted in Figure 1. Plain grey parts describe the starting point of the project, while yellow parts are the proposed extensions in the VERTIGO system verification flow.

Figure 1. VERTIGO system verification framework.

The VERTIGO verification flow spreads on three design levels: transaction level, system level and RTL.

At TL_layer-3, the design consists of an untimed SystemC description which focuses on the functionalities of the embedded system disregarding implementation details. Already existing lower-level modules can be abstracted to be integrated on in the TL_layer-3 description. A set of PSL assertions is also provided or abstracted from TL_layer-2/TL_layer-1 assertions to check TL_layer-3 functionalities. In fact, at this level, dynamic verification based on assertion checking represents a very effective approach for functional validation. Moreover, in this context, functional ATPG has a twofold role: to provide an high-quality test set for ABV, and to identify design errors early.

Moving from TL_layer-3 to TL_layer-2/TL_layer-1, both the design and the assertions are refined (and, eventually, RTL modules and properties are abstracted) to take care of IPs interaction issues and IPs implementation details. Dynamic verification is still adopted to check the correctness of IPs refined functionalities.
However, more rigorous verification approaches are needed to check the correctness of IPs interactions. Thus, static verification based on model checking and SAT-solving is introduced.
At this level, HW/SW partitioning is carried out too. At RTL, functionalities of HW modules are further refined by adding details related to the IPs communication protocols, and by optimizing the algorithms implemented within each module.
Transaction level and system level assertions can be reused by adopting the transaction-based verification. However, new temporal properties (in CTL or LTL) must be added to take care of communication protocols and timing synchronization between modules.
In particular, Petri Net-based model checking and SAT-based techniques will be exploited for RTL property verification. The transactor-based verification allows also the reuse of TL_layer-3 and TL_layer-2/TL_layer-1 test cases for dynamic verification. However, new ATPG strategies based on HLDD, which are particularly suited for modelling RTL descriptions, are introduced.

Finally, SW functionalities are validated by using both dynamic and static verification. SAT-solving and model checking are applied to verify the SW modules of the final application. Moreover, an accurate HW/SW co-simulation is introduced to (1) allow SW application and benchmark development before the final HW modules are available, (2) provide early performance evaluation.

The VERTIGO static and dynamic verification flow will include a complete integration of imPROVE-HDL, VN-Check and VN-Cover under a single GUI and coordinated in a clever way around RTL languages (System-Verilog and VHDL) and an ABV methodology.

Dedicated links and associated methodologies to other partners tools will also be provided, as reported in Figure 2. From a commercially standpoint, TL_layer-3 is often referred to as “System Level” whereas TL_layer-1 is often referred to as TLM - as it implies an HW architecture – being TL_layer-2 a sort of “grey” area between the two.

Figure 2. VERTIGO verification flow integration.

VERTIGO goal and objectives

In this context, the goal of the VERTIGO project is the development of a systematic methodology to enhance the modelling, integration and verification of architectures targeting embedded systems. To achieve this goal, VERTIGO will:

develop several formal techniques that can contribute to different stages of the design flow modelling and verification (SW,TLM level, RTL level, module level, system level) and integrate with the simulation-based approach (dynamic verification).

develop an Assertion Based Verification (ABV) method, that can be used both in static and dynamic verification with emphasis on TLM and the related metrics to measure their coverage.

prototype a SW/HW co-verification environment capable of driving the development of SW routines for the purpose of the embedded platform test.

The previous three points will allow for solving three main verification problems:

Verification of the correct interaction between all IP-cores and of the system in the networked environment.
Production of a SW layer for the purpose of the embedded platform test.
Verification of the correct modelling of system-level IP-cores and their correct mapping into RTL descriptions.

A specific case of interest holds in case of a platform conceived without knowing the final application that will be run by the customer; without application it is not possible to use HW emulation or prototyping to verify the system any more. What is asked, instead, is the verification of the platform architecture implementation itself in order to guarantee its function for a potentially very large number of variants, thus targeting a large number of possible embedded systems. Such a case is more and more popular due to (i) the tighter deadlines imposed by customers after product specification freeze and (ii) the need to reduce Non Recurrent Expenses (NRE) in design development and physical masks.

Operational goals and measurement of success

A detailed list of operational goals is reported in each Work package description – see section 7.6. A list of higher level requirements to be considered for the success of VERTIGO project is:

to provide a methodology to express useful properties at Transactional Level

measurement: at least two examples of methodology application to real STM designs will have to be put into existence as an effect of the collaboration with the project partners.
baseline: design platform requirements will be assessed in M1.1 and M1.2 . First application is at M5.1 .

to federate different techniques in the design of a novelstatic verification environment operating at RTL for IPs verification and IPs interaction

measurement: concerning specific techniques, e.g. SAT, performance evaluation is part of a continuous process to improve heuristics and engines. Concerning the collaboration of different techniques, e.g. SAT and Petri nets, there is no real reference to compare against. In the design domain it is expected to apply the developed techniques to the “top level” verification.
baseline: the deliverables D3.1b and D4.1b will provide the basic techniques to achieve the result, whereas D3.2 and D4.2 will provide the actual tools to be employed in the VERTIGO flow.

to measure property incompleteness on real sets of properties in which conscious damages (property removal and alterations) will be operated for metrics test. The tools/environment involved in this analysis constitute the “Property Coverage Checker” – PCC.

measurement: at least one example at TLM and one example at RTL. The reference to evaluate progress will be the PCC released by the SYMBAD IST-2001-34607 project; required enhancements are: 1) the degree of integration and automation between the different steps of the PCC process must be improved; 2) reduce to 1/10th the turnaround time of the PCC process (this will imply to re-design some very time-consuming steps, e.g. re-checking)
baseline: the deliverable D3.1b will provide the basic techniques to achieve the result, whereas D3.2 will provide the actual tools to be employed in the VERTIGO flow.

to provide an infrastructure telling if a property is movable from one abstraction level to another, how and where it would appear if moved, and what will be the case if preventing its moving

measurement will be made by trying to move different properties, some of which are expected to be movable and some others that arenot expected to be movable.
baseline: end of the project – D5.1.
possible extension: we expect to check that TLM and RTL descriptions of the same block satisfy a basic set of properties, thus employing a property restricted equivalence checking criterion. The infrastructure could be enhanced to show that the chosen set of properties is really significant, by checking that meaningfully mutated descriptions are reported to respond differently to the same set. The relevance of properties provided at this stage of the process must be checked also at the system/application level.

to integrate dynamic and static verification around a coherent assertion-based approach

measurement: availability ofthe ABV solution in the improve-HDL, VN-Cover and VN-Check toolset. Relevant criteria of evaluation are:

robustness, reliability and automation
consistency with System Verilog and VHDL flows
openness of VN-Cover and VN-Check to third party tools may be considered as well
more specific criteria will be provided as a result of task T1.4 .

baseline: first prototype at the beginning of task T5.2 . Stable platform at D4.2 .

WP1 will focus on selection of the embedded platform by ST-ITALY and the definition of requirements for VERTIGO verification flow. In task T1.4 metrics and benchmarking criteria will be produced by all partners, related to the different domains of application.

The evaluation of the progress beyond the state of the art will be performed in task T5.3, according to the criteria defined in T1.4 . At the very single technique level, evaluation and benchmarking constitute a continuous process, necessary to drive the developments. All partners will clearly report the achieved progress in their respective domains. In the system level domain a reference for the state of the art will be the outcome of the SYMBAD IST-2001-34607 project.

All of the produced tools will be tried in WP5 where the VERTIGO system level verification based flow will be evaluated on the embedded platform selected by STM in WP1.

VERTIGO innovations

A major innovation is to give access within a single project to a wide combination of state-of-the-art formal techniques and academic expertise for modelling and verification of hardware designs.

Main innovation areas of VERTIGO are:

Definition of an HW/SW co-simulation strategy which allows to check the correctness of the interaction between HW and SW through simulation and assertion checking.

A verification framework that combines simulation with model checking to reduce verification time and increase coverage.

Application of high-level ATPG as a well-established research field in hardware testing to dynamic verification by targeting new types of coverage metrics.

The development of techniques to separate the verification of IPs interaction from the verification of the IP-cores to facilitate efficient design-reuse.

Implementation of new coverage metrics, targeted towards assertions. The purpose is to address the assertions themselves (step coverage), their relation to the coverage of the design (variable coverage), and the density of assertions (fault coverage).

Integration of formal and dynamic techniques in a seamless manner and federated around an assertion-based methodology and new coverage metrics.

Integrating several state-of-the-art static verification techniques (SAT, High-Level Decision Diagrams, Hierarchical Petri Nets, EFSMs) to the same platform.

Bounded and unbounded model checking capability based on SAT, by selecting and extending the most promising existing solutions.

The utilization of hybrid solvers in RTL unbounded model checking, by extending previous work on SAT technology and on SAT extensions.

BUDGET

Total cost:	3,037,366€
Funding:	2,100,000 €