From: Florian Faissole <F.Faissole@fr.merce.mee.com>
Mitsubishi Electric R&D Centre Europe (MERCE) is opening one fixed-term/post-doctoral research position (12 months) in the city of Rennes (France).
The research position focuses on the formal verification of domain-specific floating-point units and the formalization of hardware description languages (VHDL...) using proof assistants.
Recent compilers and architectures generally declare themselves compatible with the IEEE-754 standard. Nonetheless, it has been noticed that some of them may lead to different results for identical floating-point computations. Formal development efforts have been made to increase confidence in floating-point computations. As an example, the Flocq library for the Coq proof assistant provides a formalization of generic floating-point formats.
Our goal is to initiate the Coq development of a whole correct-by-construction domain-specific Floating-Point Unit (FPU). This includes the design of the hardware instructions set, its formal implementation and the verification of its compliance with IEEE-754 high-level properties as formalized in the Flocq library. In order to complete the formalization effort, it would be interesting to investigate the interaction of these hardware instructions with formally-verified compilers. The project scope also includes the verification of lower-level properties of the floating-point-units, e.g. the compliance of the circuits with the floating-point instructions they are intended to execute, taking the inherent parallelism of hardware into account. An approach would be to compare the formalized instructions with RTL/Netlist implementations. Finally, we envision the formal integration of the FPU into a global processor and its verification.
The detailed position and contact information are provided at the following address:
If you are interested or would like to have additional information, do not hesitate to contact us.
Contact for application: Magali BRANCHEREAU (email@example.com<mailto:firstname.lastname@example.org>)
Contact for further technical enquiry: Florian FAISSOLE (email@example.com<mailto:firstname.lastname@example.org>) ; Benoît BOYER (email@example.com<mailto:firstname.lastname@example.org>).
Last updated: Sep 28 2021 at 20:18 UTC