International audience

With the increase in cybersecurity requirements and the growing connectivity of critical systems like vehicles and satellites, implementing both functional safety and hardware security is crucial. Although safety and security methods are well studied, combined analysis at the RTL or Netlist level remains under-explored. This paper provides an initial analysis of multiple AES designs—one unprotected, one with a safety-oriented countermeasure (Lockstep), and one with security-oriented countermeasures (Parity-Predictor)—using both simulation and formal methods. We identify the challenges and opportunities for enhancing combined safety and security assessments. Additionally, we evaluate the AES designs against ISO 26262 safety metrics and analyze their resilience to laser attacks, offering insight into their security robustness.

With the increasing availability of computational resources and the progress in research concerning automated formal methods, the characterization of safety features for hardware requires improved precision in functional vulnerability detection. In the context of formal fault injection, the model checking algorithm can be used to detect vulnerabilities in digital systems by violating the nominal temporal properties. We present a general methodology to reduce the state space that is computed and traversed during these fault campaigns. The chosen criteria preserves the nominal behavior and the failure modes, expressed by the fault-violated properties. This process is crucial to provide a manipulable object for subsequent Failure Mode and Effects Analysis. Finally, we propose an assumption-based guarantee technique to model how a fault may propagate through different hardware units, for a scalable methodology of formal fault injection and vulnerability detection in complex SoCs.

As digital systems are continuously becoming more complex, new methods are required to ensure their resilience. Research and industry are working together to develop automated formal methods, and, recently, great progress has been made to overcome this challenge. This work describes a general procedure to quantitatively determine, by Model Checking, the resilience level of a digital block whose flip-flops are perturbed by bit-flips. The flow relies on the formal proof, and provides a rich variety of results with much improved performance and accuracy (boost of ~ 300x and ~ 30x in the two test cases). The resilience metric is the number of distinct counterexamples provided by the formal engine, for each fault target. Failure traces are differentiated in two ways, showing on the test cases the great enhancement over simulation.

As digital systems keep miniaturizing and becoming more complex, new methods are required to ensure their fault tolerance. Research and industry are working together to automatize such task, and, recently, great progress has been made to overcome this challenge. Starting from an exhaustive reference simulation, we have a general procedure to determine, by Model Checking, the fault tolerance of flip-flops that are perturbed by bit-flip events. Assuming that the design is correctly implemented, the temporal properties are used as fault detectors, automatically generated through a re-adapted version of the open source software Goldmine. By this, we can also address circuits without explicit specification (blind blocks), using automatic assertions induced from the reference golden waveform. Properties are mainly mined inside the design, allowing to calculate by Model Checking the fault masking capacity of the addressed modules. We consider two medium sized blocks, showing results with much-improved performance and accuracy over classical simulated fault injection.

In the context of functional verification, the focus has always been on hardware and its ability to be both resilient to errors and to recover from them autonomously. In order to evaluate these characteristics, an extensive use of Fault Injection tools is made to achieve clear and granular results. These testing campaigns are carried out on the entire DUT and require a consistent amount of time and computational resources. The possibility of reducing these costs applying modern techniques as the study of the Dysfunctional State Machine or the proof of concept regarding the composability of single block fault injection campaigns to obtain a library of component of which the reliability metrics are well known, as already been extensively discussed and proven on hardware. In this work instead the application of this methodologies to software is presented for the first time. In order to do so, the software has been divided into basic block, atomic chunks of code having precise carachteristics that will ensure the possibility to study them singularly and then recompose them into a software product which reliability metrics are known, without the need for complete Fault injection campaign.

In the field of automatic quality or safety assurance level evaluation, this paper proposes the first approach towards the automation of the extraction processes of both the valid and faulty state machines within a System-on-a-Chip. The data automatically extracted by this method is a relevant input for behavioural modelization and FMEA analysis. The method is based on a semi-automated approach for the systematic extraction of failure modes of a digital design in the hypothesis of a single-event upset (SEU) or stuck-at in flip-flops. This procedure aims to enhance human driven failure analysis and provide inputs for RAMS frameworks in the process of quality assurance of complex devices. The main objective is to transport and apply RAMS methods and tools in the area of SoCs design. Experimental results have been conducted on an I2C - AHB system, laying the base for a complete and more complex analysis on an entire SoC.

We propose a novel approach relying on signal state conditional probabilities and circuit clustering to perform a probabilistic analytical estimation of the reliability of combinatorial logic circuits. This approach uses clustering and joint conditional probabilities to reduce the execution time and matrix size needed. Its effectiveness is demonstrated on a 8 bit Brent Kung adder.

This paper reviews recent experimental confirmations that the intrinsic radiation robustness of commercial CMOS technologies naturally improves with the down-scaling. When additionally using innovative design techniques, it becomes now possible to assure that performance and radiation-hardness are both met. An illustration is given with an original nano-power and radiation-hardened 8 Mb SRAM designed in 130 nm CMOS.

This paper describes the FlexCC2 register allocation framework. FlexCC2 is an optimizing retargetable C compiler for embedded processors, and in particular for DSP processors. Embedded processors often contain features such as irregular and constrained register sets that complicate register allocation, making traditional methods inefficient. In this paper, we present a register allocation framework specifically tailored for embedded processor specificities. This framework has been integrated in the FlexCC2 production compiler and is used by FlexCC2 customers.

This paper presents the underlying methodology of Cosmos, an interactive approach for hardware/software co-design capable of handling multiprocessor systems and distributed architectures. The approach covers the co-design process through a set of user guided transformations allowing semi-automatic partitioning. The transformations are based on a powerful set of primitives for functional partitioning, structural reorganization and communication transformation. It leads to a fast transformation of a system-level specification into an architecture with a short design time and fast exploration of design space. The application of this approach is illustrated using a design example starting from a system-level specification given in SDL to a distributed hardware/software architecture described in C/VHDL. We show that the use of transformational approach allows: 1) application of the expertise of the designer during partitioning; 2) the user to understand the results of the co-design process; 3) the process to take into account partial existing solutions; 4) large design space exploration; and 5) the designer to start from a very high-level specification language of the system to be designed.

The aim of this paper is to present a communication synthesis approach stated as an allocation problem. In the proposed approach, communication synthesis allows to transform a system composed of processes that communicate via high-level primitives through abstract channels into a set of processes executed by interconnected processors that communicate via signals and share communication control. The proposed communication synthesis approach deals with both protocol selection and interface generation and is based on binding/allocation of communication units. This approach allows a wide design space exploration through automatic selection of communication protocols. We present a new algorithm that performs binding/allocation of communication units. This algorithm makes use of a cost function to evaluate different allocation alternatives. We illustrate through an example the usefulness of the algorithm for allocating automatically different protocols within the same application system.