The Project

Table of Contents

 

Abstract

Design and verification of modern embedded platforms are two highly related problems which are still mainly addressed by using unrelated methodologies. This effectively reduces development productivity and complicates achieving predictable system properties.
The COCONUT project thus focuses on the definition of a formal framework based on a tight integration of design and verification through all refinement steps of an embedded platform design flow, from specifications to logic synthesis and software compilation. In particular, it is intended to propose a modelling and verification flow to enhance and speed-up embedded platform design and configuration with particular regard to application fields related to mixed continuous/discrete models, like for example networked multimedia and sensor network managing.
In this context, the main activities of COCONUT will be related to the definition of innovative methodologies and tools to:

  • define and validate properties that represent the design specification;
  • automatically synthesize properties into code;
  • map models between hybrid and discrete domains;
  • provide correct-by-construction abstraction/refinement processes;
  • perform post-refinement verification.

Such activities will be implemented in a set of tools working on more that one abstraction level whose correctness will be formally proved. The reference platform to apply and validate the COCONUT flow will be FAUST with a couple of software defined radio applications.

Concept and project objectives

The COCONUT project is intended to propose a modelling and verification flow to enhance and speed-up embedded platform’s design and configuration with particular regard to application fields related to mixed continuous/discrete models, like for example networked multimedia and sensor network management.
The embedded platform market is converging on a limited but more powerful set of embedded platforms, mainly due to increasing design cost which requires higher production volume. Differentiation among effective platform configurations is thus a key advantage for a platform user to approach the market with innovative solutions.
The COCONUT flow will be at first specified and then verified by taking as reference the embedded platform showed in Figure 1.

 

Figure 1. The COCONUT reference embedded platform.

The main characteristics of this platform are:

  • multi–core architecture and highly SW programmable;
  • customizable HW to implement computationally intensive functions;
  • tight integration of HW and SW to differentiate families of applications starting from the same embedded platform;
  • communication ASICs specialized in the interaction with complex network protocols;
  • control ASICs for the acquisition of data from analogue sensors and the control of actuators.

The platform is thus well suited for heterogeneous application domains that require a high interaction between the digital domain and the network and continuous-time domains.

In this context, platform design and platform configuration consists of the following main activities.

  • Platform design:
    • identification of platform architecture, that is which components must be included in the platform (e.g., NoCs, ASICs, etc.) and how they are interconnected (e.g., buses, crossbar switches, etc.);
    • definition, design and verification of unprogrammable components (e.g., communication ASICs, control ASICs, etc.);
    • definition of general purpose software (e.g., basic RTOS, device driver of unprogrammable components, etc.);
    • design and verification of a reference application.
  • Platform configuration:
    • design of RTOS, middleware and SW application;
    • design and verification of customizable HW (e.g., configurable FPGAs);
    • application partitioning among available components through TLM refinement.

To better explain the concept of platform design and configuration, let us move from the reference embedded platform to the actual platform provided by CEA-LETI called FAUST. It stands for Flexible Architecture of Unified Systems for Telecom. It is an architectural concept initiated in 2003 for supporting multiple OFDM air interfaces in a single SoC. It was developed originally with IEEE 802.11a and 4MORE in mind, and it was naturally extended to the 3GPP/LTE mobile terminal baseband implementation.

The FAUST baseband architecture is organized around a homogeneous NoC (Network on Chip) based on a 2D meshed network. The different units are connected to the network, which is distributed over the whole system. The computing units communicate according to specific packet-switching techniques.

The FAUST functional units can either be implemented as hardware IP blocks or as software running on a specific processor resource available as computing unit. This offers several very interesting aspects, in terms of simplification of the control structure, of network bandwidth, and reconfigurability, thus emphasizing the role of embedded platform configuration activity.

Figure 2. The FAUST embedded platform.

The FAUST embedded platform is depicted in Figure 2. It includes 23 IP blocs connected to a 20 nodes network for a total complexity of 8 Mgates. Most of these IPs implement parametrizable data processing such as OFDM modulation or timing synchronization. Some of them are more reconfigurable, and include optimized data paths able to implement several algorithms such as channel estimation. Finally, the chip also implements “housekeeping” functions such as CPU (a ARM946 core), specialized DMA engines and Ethernet interface.

For this development a CMOS 0.13µ technology from STMicroelectronics has been used; chip area is 80mm2 and the selected package is a TBGA420. In FAUST chip, network routers are implemented using asynchronous logic, which allows defining a very smart GALS (Globally Asynchronous Locally Synchronous) architecture: each IP has its own clock and no global signal is distributed on the whole chip. Functionally, FAUST supports a class of baseband processing which complements the baseline OFDM scheme to support multiple space-time coding schemes, different channel coding, etc. Each specific protocol is mapped on the topological structure of the chip: the data routing between the functional units reflects the sequence of algorithms.

Design and verification of such a kind of embedded platforms are two highly related problems which are still mainly faced by using unrelated methodologies. The proposed project is thus focused on a tight integration of design and verification throughout all refinement steps of an embedded platform design, from specifications to logic synthesis and software compilation.

Figure 3. The key idea of the COCONUT workbench.

The complexity of both platform design and platform configuration requires an innovative design and verification flow able to effectively reduce the number of design errors and design recycles. This is a key factor for increasing system development productivity while achieving predictable system properties.

Moreover, an incremental and hierarchical verification strategy is fundamental to manage the huge complexity of this embedded platform that cannot be verified in the whole at a structural level such as the RTL.

Even at TLM the platform modelling would be difficult due to the presence of complex networks and continuous-time information. As a result, the addition of hybrid automata to SystemC TLM models will be proposed for tackling the modelling complexity.

In both platform design and platform configuration, this very abstracted platform description requires correct-by-construction refinements and/or automatic verification of manual refinements, to translate, without design errors, the abstract description into an actual application. This is the main objective of the COCONUT project.
In this context, the key idea of COCONUT is depicted in Figure 3. Platform design and platform configuration are considered as a continuous mix of the following processes:

  • definition and validation of properties that represent the specification;
  • automatic synthesis of properties into code;
  • mapping of models between hybrid and discrete domains;
  • correct-by-construction abstraction/refinement;
  • post-refinement verification with respect to the specification.

Such activities will be implemented in a set of tools working on more than one abstraction level whose correctness will be formally proved. Each model/property can be refined to a lower abstraction level or abstracted to a higher abstraction level, and verification should not be only a post-refinement step, but it should guide the design with a correct-by-construction methodology.