In January 2008, work commenced on a European research project coordinated by the Electronic System Design Group of the Dipartimento di Informatica at the University of Verona, led by Prof. Franco Fummi. The project, COCONUT (www.coconut-project.eu) —A COrrect-by-CONstrUcTion Workbench for Design and Verification of Embedded Systems— has been evaluated as the best project proposal on embedded systems submitted to the European Union’s (EU's) Seventh Framework Programme. Project funding amounts to 3.2M €, encompassing a global effort of 360 person months over the course of 2.5 years.

The aim of the project is the definition of a formal framework based on 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 will propose a modeling and verification flow that enhances and speeds up embedded platform design and configuration and address mixed continuous/discrete models such as networked multimedia and sensor network management.

COCONUT brings together eight European partners: two EDA companies, Aerielogic (France) and Certess (France); two research centers, CEA-LETI (France) and Fondazione Bruno Kessler (Italy); and four Universities: Graz University of Technology (Austria), University of Southampton (UK), Universität Paderborn (Germany), and Università di Verona (Italy).

The competencies of these partners cover the wide spectrum of knowledge needed to ensure the successful completion of the project. CEA-LETI supplies its embedded system design expertise. Aerielogic and Certess provide design verification tools, focused, respectively, on static verification and dynamic verification. Fondazione Bruno Kessler, University of Southampton and Graz University of Technology are playing the role of design and verification technology providers by developing techniques for automatic static verification and automatic synthesis of systems from specifications. Universität Paderborn and Università di Verona are dealing with synthesis of embedded software, dynamic verification technologies, and analysis and synthesis in the hybrid and discrete domains.

Previous case studies taken from embedded systems developed by CEA-LETI will focus mainly on mixed-level/mixed-language flows, involving both TLM and RTL and targeting software-defined radio applications. 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; and
• perform post-refinement verification.

Such activities will be implemented in a set of tools working on more than one abstraction level with correctness formally proved.

COCONUT is scheduled to be completed in June 2010. The project will take the roadmaps of public consortia like Accelera as references for the development of verification standards and of OSCI for the standardization of transaction level models (TLMs).

About The Partners

University of Verona (http://www.univr.it) is one of the largest universities in the North-East of Italy. The research group on Electronic Systems Design (ESD, http://esd.sci.univr.it), that will be involved in COCONUT, belongs to the Department of Computer Science (http://www.di.univr.it) that has been ranked for several consecutive years the first Computer Science department of Italy by an official analysis of CENSIS (the national centre for statistical analysis of the society). Main research activities of the ESD group concern HDLs and EDA methodologies for modelling, synthesis, static and dynamic verification, testing, and optimization of hybrid and discrete HW/SW systems.

Aerielogic (http://www.aerielogic.com) is a French start-up based in Normandy (France) that was created in August 2005 around a team of experienced engineers/PhDs in Formal Verification and Assertion-based Verification. The company's goal is to enhance the SoC functional verification flow using an assertion-based methodology (ABV) and formal verification.

CEA-LETI (http://www-leti.cea.fr) is a laboratory belonging to the French Nuclear Energy Commission (CEA). The main activities of CEA-LETI are dealing with microelectronics, sensors, microsystems, instrumentation, optoelectronics, IC design and telecommunications.

Certess S.A. (http://www.certess.com) is the French subsidiary of Certess Inc., a US based EDA company. Certess developed the first commercial software product based on the theory of mutation analysis. By leveraging the first complete measure of functional verification quality, Certess' clients achieve more efficient functional verification.

The Fondazione Bruno Kessler (http://www.fbk.eu) is a private research foundation located in Trento -- Italy. Its mission is international competition, the exploitation of the results coming from the research and the innovation of industrial products. In the Labs located in Povo (Trento) more than 300 researchers work in two main research centers: Information Technology and Material and Microsystem Technology. The Information Technology centre (http://cit.fbk.eu) carries out research in key areas (e.g. Embedded Systems -- http://es.fbk.eu) with the aim to provide practical and experimental evidence of its added value for the market, cultural growth, and social welfare. The research of the Fondazione Bruno Kessler aims to push innovation through the construction of a networked system that involves companies, other research institutions, universities, public bodies, and end-users.

The University of Southampton (http://www.ecs.soton.ac.uk/) is ranked among the best research universities in the UK. The unit that will participate in the COCONUT consortium is the Declarative Systems and Software Engineering (DSSE) group. The DSSE group has a large number of scientific competencies, including formal methods (e.g. Model Checking) and algorithms for fundamental problems in Computer Science (e.g. Boolean Satisfiability and Optimization).

Graz University of Technology (http://www.tugraz.at/) is one of Austria’s leading polytechnical universities. Its faculty of computer science is well known for its activities in such areas as Knowledge Management, Computer Graphics, Security, and Design of Reliable Systems. Graz University of Technology will be represented by the Institut fur Angewandte Informations verarbeitung, whose foremost expertise lies in the formal analysis of digital systems.

Universität Paderborn (http://www.uni-paderborn.de/) is one of Germany’s leading universities in the IT area and well-known for its interdisciplinary work and close cooperation with industry. The main interests of Universität Paderborn in COCONUT are in the modelling, verification, and synthesis of RTOS-related system models and their properties.