International audience

In recent years, heterogeneous SoCs—comprised of multiple processor cores and programmable logic—have greatly progressed both complexity and performance. From a security point of view, this leads to an expansion of the attack surface exposed to adversaries. To address this issue, in this article, we propose a novel heterogeneous SoC architecture called RTrustSoC. Our proposal includes an innovative fully-reconfigurable post-deployment strategy for partitioning the SoC architecture into multiple exclusion levels—worlds—with customizable degrees of privilege. We aim to provide SoC designers with fine control over the security of the system by segregating trusted hardware components from third-party IPs with “on-demand” hardware isolation. Therefore, we expect that an RTrustSoC instance could evolve from a multi-world SoC to a fully trusted platform as IPs progressively develop. RTrustSoC also proposes a dynamic reconfigurable penalty system to monitor the third-party IPs and take measures in case of a detected abnormal behavior. Our experimental testing on an AMD-Xilinx Zynq-7000 SoC-FPGA showed the penalty of the proposed isolation strategy to be small, up to 1% in LUT and 0.7% Flip Flop utilization, thus enabling to an efficient security solution. RTrustSoC introduces a novel design paradigm, evolving from the binary notion of security—trusted vs untrusted—into a flexible set of worlds that can be adapted to any scenario. We demonstrate a real case scenario of RTrustSoC use on time-based cache memory attacks with implementation results.

Security by Design (SbD) has gained increasing interest over the past decade. While iterative processes and legacy preservation aim to reduce costs and mitigate risks through continuity, SbD encourages a break in the way we do things with a simple idea: dealing with new threats, leading to new risks, requires a complete rethink of our design processes.

Multiverse debugging extends classical and omniscient debugging to allow the exhaustive exploration of non-deterministic and concurrent systems during debug sessions. The introduction of user-defined reductions significantly improves the scalability of the approach. However, the literature fails to recognize the importance of using more expressive logics, besides local-state predicates, to express breakpoints. In this article, we address this problem by introducing temporal breakpoints for multiverse debugging. Temporal breakpoints greatly enhance the expressivity of conditional breakpoints, allowing users to reason about the past and future of computations in the multiverse. Moreover, we show that it is relatively straightforward to extend a language-agnostic multiverse debugger semantics with temporal breakpoints, while preserving its generality. To show the elegance and practicability of our approach, we have implemented a multiverse debugger for the AnimUML modeling environment that supports 3 different temporal breakpoint formalisms: regular-expressions, statecharts, and statechart-based Büchi automata.

To ensure correctness of critical systems, swarm verification produces proofs of failure on systems too large to be verified using model-checking. Recent research efforts exploit both intrinsic parallelism and low-latency on-chip memory offered by FPGAs to achieve 3 orders of magnitude speedups over software. However, these approaches are limited to safety verification that encodes only what the system should not do. Liveness properties express what the system should do, and are widely used in the verification of operating systems, distributed systems, and communication protocols. Both safety and liveness properties are of paramount importance to ensure systems correctness. This paper presents Dolmen, the first FPGA implementation of a swarm verification engine that supports both safety and liveness properties. Dolmen features a deeply pipelined verification core, along with a scalable architecture to allow high-frequency synthesis on large FPGAs. Our experimental results, on a Xilinx Virtex Ultrascale+ FPGA, show that the Dolmen architecture can achieve up to 4 orders of magnitude speedups compared to software model-checking.

Multiverse debugging is an extension of classical debugging methods, particularly adapted to non-deterministic systems. Recently, a language-independent formalization was proposed. Moreover, multiverse debugging is particularly beneficial for specification and design languages, such as UML. However, this method suffers from scalability issues during breakpoint lookup. This problem arises due to the exhaustive exploration performed on the potentially infinite state-space of the system.

The RISC-V Instruction Set Architecture (ISA) is an open-source, modular and extensible ISA. The ability to add new instructions into a dedicated core opens up perspectives to accelerate VM components or provide dedicated hardware IPs to applications running on top. However, the RISC-V ISA design is clashing on several aspects with other ISAs and therefore software historically built around them. Among them, the lack of condition codes and instruction expansion through simple instruction combination. In this paper we present the challenges of porting Cogit, the Pharo’s JIT compiler tightly linked to the x86 ISA, on RISC-V. We present concrete examples of them and the rationale behind their inclusion in the RISC-V ISA. We show how those mismatches are solved through design choices of the compilation process or through tools helping development: a VM simulation framework to keep the development in a high-level environment for the most part, an ISA-agnostic test harness covering main VM functionalities and a machine code debugger to explore and execute generated machine code. We also present a way to prototype custom instructions and execute them in the Pharo environment.

The mapping of software verification algorithms on FPGA promise orders of magnitude faster verification. FP-GASwarm shows 900X speedup over software swarm verification. However, this approach misses important optimization opportunities and glosses over algorithmic design-space exploration.This paper introduces Carnac, a deeply pipelined swarm verification architecture, which by exposing the algorithmic variability points can realize multiple verification algorithms. Furthermore, we introduce the Mixed Young Random Frontier-Bounded (MYR_FB), a new swarm verification algorithm, found through an efficiency-based design-space exploration.Evaluated on the BEEM benchmark, the MYR_FB algorithm shows up to 144% efficiency gain over FPGASwarm on 72% of the models. The Carnac architecture runs at 400MHz on Xilinx Ultrascale+ FPGA, and can accommodate twice more verification cores than FPGASwarm. Overall the evaluation shows a 7.58X speedup over FPGASwarm, while enabling an unprecedented scalability on high-end FPGAs.

EFPGAs give designers the flexibility to make changes at any point in the chip’s life span, even in the customers’ systems. Though, eFPGA are not efficient from an integration perspective, making proper dimensionning and tailoring mandatory. Unfortunately, designing an eFPGA is a complex and error-prone task. Even though automatic generation from high level models can produce correct-by-construction layouts, integration remains complex due to process variation. A key point is then to reduce the technology dependency.This paper presents the ELNATH project in which three implementations of the same architecture have been addressed: overlay, eFPGA, and 55 nm FPGA thanks to an open-source integrated tool flow that supports defining, implementing and programming reconfigurable architectures.

Among formal methods, model-checking offers a high-level of automation and can lower the cost of the verification process. Two preliminary studies on FPGA model-checking show a high-performance increase, thanks to the massive parallelism and precise memory control opportunities. However, these approaches rely on HDL-based ad-hoc model encoding, and miss the importance of decoupling the modeling language from the verification core, which greatly limits their usability. In this paper we propose Menhir, a new highly modular hardware model-checker, inspired by the architecture of software verification frameworks. Menhir is based on a generic language-verification interface which isolates the modeling-language semantics from the verification core, allowing their independent evolution. Menhir opens the architecture to the whole spectrum of modeling languages. Moreover, it proposes a polymorphic verification core, which offers a continuum between partial and exhaustive verification, with promising performances.

In the new generation of networks, not only computers are connected but also objects like cars, streets, buildings, or just, everything. In general, these things communicate by means of internet using gateways. Simulating these systems can help to validate specific algorithms and concepts. However, it cannot give any accurate information about reality when some problems arise such as delays, disconbectivity, attacks, insecurity, and especially in the case of large networks. Also, the real implementation of such networks is very complex, time consuming and can be impossible when the nodes are situated in different cities or countries. In this demo we propose a new platform called CupCarbon-Lab based on the existing simulator CupCarbon, where the codes used in simulation can be directly injected in real connected embedded cards like Raspberry Pi cards. This platform can automatically generate from the software a real IoT network even it is already deployed, which can be reconfigured without the need to go through each node. It also helps to test the feasibility and the scalability of an algorithm in real conditions.

Security and safety are more and more important in embedded system design. A key issue, hence lies in the ability of systems to respond safely when errors occur at runtime, to prevent unacceptable behaviors that can lead to failures or sensitive data leakage. In this paper, we propose a design approach that automatically generates on-chip monitors (OCMs) during high-level synthesis (HLS) of hardware accelerators (HWaccs). OCM checks at runtime the input/output timing behavior, the control flow execution and algorithmic properties (via American National Standards Institute C assertions) of the monitored HWacc. OCM is implemented separately from the HWacc and an original technique is introduced for their synchronization. Two synthesis options are proposed to tradeoff between performance and area. Experiment results show that error detection on the control flow is 16× better compared to the existing approaches while the cost of assertions is reduced by 17.48% on average. The impact on execution time (i.e., latency of the HWacc) is decreased by 2.76× at no area penalty and up to 4.5× with less than 10% extra-area. The clock period overhead is at worst less than 5% and the overhead on the synthesis time of the HWacc to generate OCMs is 7.44% on average.

This article describes TBES, a software end-to-end environment for synthesizing multitask applications on FPGAs. The implementation follows a template-based approach for creating heterogeneous multiprocessor architectures. Heterogeneity stems from the use of general-purpose processors along with custom accelerators. Experimental results demonstrate substantial speedup for several classes of applications. Furthermore, this work allows for reducing development costs and saving development time for the software architect, the domain expert, and the optimization expert. This work provides a framework to bring together various existing tools and optimisation algorithms. The advantages are manifold: modularity and flexibility, easy customization for best-fit algorithm selection, durability and evolution over time, and legacy preservation including domain experts' know-how. In addition to the use of architecture templates for the overall system, a second contribution lies in using high-level synthesis for promoting exploration of hardware IPs. The domain expert, who best knows which tasks are good candidates for hardware implementation, selects parts of the initial application to be potentially synthesized as dedicated accelerators. As a consequence, the HLS general problem turns into a constrained and more tractable issue, and automation capabilities eliminate the need for tedious and error-prone manual processes during domain space exploration. The automation only takes place once the application has been broken down into concurrent tasks by the designer, who can then drive the synthesis process with a set of parameters provided by TBES to balance tradeoffs between optimization efforts and quality of results. The approach is demonstrated step by step up to FPGA implementations and executions with an MJPEG benchmark and a complex Viola-Jones face detection application. We show that TBES allows one to achieve results with up to 10 times speedup to reduce development times and to widen design space exploration.

The concept of System of Systems (SoS) has become a key to handle the complexity of large scale systems designed in domains such as aerospace or defense. Virtual prototyping, by providing modelling and execution, increases the success of the SoS. Large scale systems involve heterogeneous modelling and execution formalism. Typical approaches based on types fail in offering the needed dynamicity to answer the virtual prototyping requirements. In order to bridge the existing gap between system models and execution tools, we suggest an approach based on roles and parser combinatory. Roles provide a dynamic coupling between modelling and execution allowing independent evolution of modelling and execution. Parser combinatory ease the integration of new modelling formalisms. This approach has been validated on a seafloor observatory project and lead to the implementation of a framework in Smalltalk.

Embedded systems often implement safety critical applications making security a more and more important aspect in their design. Control-Flow Integrity (CFI) attacks are used to modify program behavior and can lead to learn valuable information directly or indirectly by perturbing a system and creating failures. Although CFI attacks are well-known in computer systems, they have been recently shown to be practical and feasible on embedded systems as well. In this context, CFI checks are mainly used to detect unintended software behaviors while very few works address non programmable hardware component monitoring. In this paper, we present a hardware-assisted paradigm to enhance embedded system security by detecting and preventing unintended hardware behavior. We propose a design approach that designs on-chip monitors (OCM) during High-Level Synthesis (HLS) of hardware accelerators (HWacc). Synthesis of OCM is introduced as a set of steps realized concurrently to the HLS flow of HWacc. Automatically generated OCM checks at runtime both the input/output timing behavior and the control flow of the monitored HWacc. Experimental results show the interest of the proposed approach: the error coverage on the control flow ranges from 99.75% to 100% while in average the OCM area overhead is less than 10%, the clock period overhead is at worst less than 5% and impact on the synthesis time is negligible.

Evolution of Systems-On-Chip (SoC) increases the challenge of verification and post-silicon debug. Nowadays, Assertion Based Verification (ABV) is a widely used methodology. Languages like PSL (Property Specification Language) or SVA (System Verilog Assertions) allows engineers to define properties at Register Transfer Level (RTL). Properties can then be used to generate simulation/hardware assertion checkers for dynamic verification. In this paper, we propose to consider ANSI-C assertions during High-Level Synthesis (HLS) of hardware accelerators (HWacc) to automatically generate on-chip monitors (OCM). The proposed method is portable to any HLS tool and supports both static and dynamic application behaviors. OCM is implemented separately from the HWacc and an original technique is introduced for their synchronization. Two synthesis options are proposed for the OCM design i.e. speed and area. Experimental results show the interest of the proposed approach: while the cost of the OCMs mainly depends on the complexity of input assertions, setting synthesis option is area allows reducing the complexity of the OCM by 2.37x on average compared to the option for speed optimization.

SUMMARY Smalltalk is an exciting object‐oriented language in which even primitive values are uniformly handled as normal objects described by classes that one can browse and extend. Smalltalk was born during the seventies, but the ideas behind currently available implementations are still modern and innovative. Smalltalk benefits from being a highly expressive language in which complex and powerful systems can emerge from the composition of simple building blocks. Thanks to its dynamic nature, fast prototyping and agile software development are made possible. Smalltalk also benefits from having powerful meta‐programming facilities. A program is able to query and to change its own structure and behavior. Smalltalk is not only a language but also an interactive system that is implemented in Smalltalk and that can be customized according to users needs. This special issue presents four extended versions of research papers from the third International Workshop on Smalltalk Technologies (IWST) that was organized at Edinburgh on September 2011. Johan Fabry et al. presented Phantom, an aspect language that includes recent research results in aspect interactions and reentrancy control. Phantom is designed to be optimized and compiled where possible. Increasing use of reflection and meta‐programming techniques in real world applications underlines the need for more dynamic approaches. New approaches have shifted to object‐specific reuse. Jorge Ressia et al. proposed a new abstraction called a talent, which models features that are shared between objects of different class hierarchies. Martin Dias et al. presented Fuel, a general‐purpose object serializer that focuses on speed, through a compact binary format and an efficient pickling algorithm. Fuel serializes any object, thus having a full‐featured language‐specific format. Redesign of nontrivial software is often a challenge. Ciprian Teodorov et al. addressed physical‐design automation and presented a methodological approach relying on model‐driven engineering. Also, they summarized some lessons learned from the incremental redesign of Madeo, a toolkit that targets field‐programmable gate array design automation. The goal of the IWST workshop series is to create and foster a forum around advances or experiences in Smalltalk. Each IWST workshop is organized as a collocated event of the European Smalltalk User Group annual conference. Copyright © 2012 John Wiley & Sons, Ltd.

SUMMARY The current integrated circuit technologies are approaching their physical limits in terms of scaling and power consumption, in this context, the electronic design automation (EDA) industry is pushed towards solving ever more challenging problems in terms of performance, scalability and adaptability. Meeting these constraints needs innovation at both the algorithmic and the methodological level. Amongst academic EDA tools, Madeo toolkit has been targeting field‐programmable gate array (FPGA) design‐automation at the logic and the physical level since the late 1990s. As many other long‐living software, despite embedding valuable legacy, Madeo exhibits unwanted characteristics that penalize evolution and render the automation problems even more difficult. This study presents a methodological approach to physical‐design automation relying on model‐driven engineering, which is illustrated through the incremental redesign of the Madeo framework. A benefit of this approach is the emergence of a common vocabulary to describe the EDA domain in an FPGA scope. A second advantage is the isolation of the optimization algorithms from the structural domain models. However, the main asset is the possibility to re‐inject into the newly designed toolkit most of the legacy code. The redesigned framework is compared with and scored against initial code‐base, and demonstrates a regression‐free remodeling of the environment with net improvements in terms of size and complexity metrics. As a consequence, the evolution capability is back on stage, and the domain‐space exploration widens to the algorithmic axis. Copyright © 2013 John Wiley & Sons, Ltd.

In this paper we propose an ESL synthesis framework which, from the C code of an application and a description of a generic architecture, automatically explores and generates a complete synthesizable version of a H-MPSoC architecture along with the adapted code application. We developed a Design Space Exploration (DSE) algorithm that merges hardware specialization, data-parallelism exploration, processor instantiation and task mapping according to user performance and cost constraints. We also inserted HLS in the DSE loop and get fast exploration of hardware acceleration. A new ESL framework is presented, it combines our contributions with some legacy tools issued from our and another team. We validated our framework with a case study of an MJPEG decoder.

This paper presents a new debugging methodology for applications targeting reconfigurable platforms. The key issue behind is that bringing software engineering techniques advantages to hardware design would reduce design cycles hence time-to-market. Our high-level synthesis framework supports probes insertion both in the behavioural description of the application and in its hierarchical netlist. Probe status can control the execution, and traced signals can be read back from software. Probes' conditions can be reassigned at runtime tackling the main disadvantage of modifications through re-synthesis and favours short debugging cycles similarly to software development.