PhD student (Teaching assistant, European Commission)
Team : APR
Arrival date : 10/01/2021
    Sorbonne Université - LIP6
    Boîte courrier 169
    Couloir 25-26, Étage 3, Bureau 331
    4 place Jussieu
    75252 PARIS CEDEX 05

Tel: +33 1 44 27 88 04, Loic.Sylvestre (at)

Supervision : Emmanuel CHAILLOUX

Co-supervision : SEROT Jocelyn (CNRS/UCA/SIGMA)

Safe, expressive and efficient programming of FPGA-based reprogrammable circuits

Widely used for the past twenty years by the digital circuit design community, FPGA-based reconfigurable circuits (Field Programmable Gate Array) are the subject of growing interest from programmers in the broadest sense, particularly for embedded applications with critical performance or safety. By allowing the hardware to be "tailored" to the needs of the software, this type of circuit offers a novel way of bypassing the limitations of conventional processors. In the state of the art, the efficient programming of this type of circuit requires the use of languages dedicated to hardware description (Hardware Description Languages) such as VHDL or Verilog. While these language allow a fine control and an optimal exploitation of the available hardware resources, they are nevertheless characterized by a low level of abstraction, which makes their use delicate by a public not familiar with hardware design. To address these difficulties, a hybrid approach is proposed. The idea is to have the main program, written in a high level host language (functional, imperative, ...), executed by a virtual machine implemented on a "softcore" processor - which gives access to all the expressive power of the host language - and to carry out the translation at the RT (Register Transfer) level - a translation that we will call here hardware "inlining" - only for a certain number of specific functions, duly identified. The identification of these functions, in this context, is the responsibility of the programmer, taking into account his field of application and the objectives pursued. The programmer may thus choose to "inline" certain functions because their execution via the virtual machine on the "softcore" processor is too slow - which corresponds to using the surrounding hardware as a dynamically configurable hardware accelerator - or because, in a critical embedded context for example, he wants to guarantee certain properties linked to the execution of these functions (safety, liveliness, limited execution time, etc.). The formulation of the functions to be "inlined" will not be done directly in the host language but via a dedicated language (DSL, Domain Specific Language). This DSL will, by construction, be susceptible of an efficient and certifiable translation into a description at RT level (we mean that we can prove that the said description produces a circuit whose behavior is identical to that deduced from the formal semantics of the DSL). It must also be directly executable by the host language (either by interpretation or by direct translation into this language). Finally, it must allow the expression of the properties that one wishes to associate to the defined functions. The definition, and the implementation, of this DSL is a key point since it conditions the feasibility of the RTL translation and the efficiency of the code produced, on the one hand, and the nature of the verifiable properties associated with the functions thus described, on the other

2020 Publications