A European research project coordinated by the University of Verona, Italy, hopes to define a formal framework based on tight integration of design and verification through all the refinement steps of an embedded-platform design flow. The project, which spans specification through logic synthesis and software compilation, also aims to propose a modeling and verification flow that enhances and speeds up embedded platform design and configuration. That flow would also address mixed continuous/discrete models such as networked multimedia and sensor network management.
Since January the project has been known as Coconut (COrrect-by-CONstrUcT Workbench for Design and Verification of Embedded Systems). It has been evaluated as the best project proposal on embedded systems submitted to the European Union’s Seventh Framework Programme. As such, funding for the project is €3.2 million.
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.
The COCONUT project is scheduled to be completed in June 2010. The project will take the roadmaps of public consortia like Accellera as references for the development of verification standards and of OSCI for the standardization of transaction level models (TLMs).
Coconut
www.coconut-project.eu