CEA-List is developing a suite of tools to support design (prototyping, design space exploration, analysis, model generation) and validation (simulation, code analysis, performance analysis, etc.), which facilitates the implementation and optimisation of new architectures. These tools enable virtual proofs of concept to be carried out for software and hardware computing architectures based on existing and/or future technologies, and allow the models to be utilised effectively.
It is possible to model software environment constraints in order to optimise execution tools (compilers, runtimes, libraries).
The CEA-List has developed expertise in formal methods for modelling and verifying code, at both the software and hardware levels.
On the software side, the two flagship formal verification tools are Frama-C, for analysing C code, and BINSEC, for analysing binary executable code. The link to the hardware-specific features of architectures (instruction sets, dedicated operators) is provided by decoders derived from the UniSIM-VP dynamic binary code analysis tool.
The LEAF framework, meanwhile, enables the formal verification of temporal and security properties of the combined software and hardware of an embedded system.
This expertise is utilised by the programme, in particular to validate functional and non-functional properties with the aim of adapting the software to the hardware environment, in accordance with system-level specifications.
As the design of digital computing architectures becomes increasingly complex, the number of parameters to be taken into account is growing, and it is necessary to rapidly explore the design space to find the best configuration. The teams develop and use the VPSim (virtual prototyping and simulation) and A-DECA (automatic design space exploration) tools to support the design of digital architectures arising from research work. VPSim thus enables the rapid simulation and validation of complex systems, striking the best balance between simulation runtime and the accuracy of the evaluated parameters. It therefore provides an accurate assessment of the system’s various performance characteristics.
A-DECA (Automated Design Space Exploration for Computing Architectures) is a modular decision-support tool that interfaces with simulators (in particular VPSim) and combines the results with analytical formulations to provide a relevant evaluation of architectures. It enables the automatic and efficient exploration of the design space by integrating various traditional design constraints and objectives (performance, power consumption, area) as well as innovative criteria such as security and environmental footprint. Its aim is to propose relevant configurations that meet multi-objective optimisation criteria.
Accurately simulating extra-functional properties such as performance or power consumption is a key challenge in the simulation and exploration of digital architectures. CEA List is developing kMLeon, a tool that uses machine learning to automatically generate models that represent these properties; when combined with functional models, these make the simulation of digital architectures more accurate. CEA List is thus seeking to make the best possible use of artificial intelligence technologies in the design of computing architectures.
CEA-List uses a wide range of technologies:
With the ever-increasing demand for numerical computation – driven in particular by the rise of applications utilising artificial intelligence – we need to rethink development processes and offer innovative methodologies and high-performance tools to simplify the design of new architectures.”