Email Gateway (Jul 03 2021 at 09:26): Email Gateway (Jul 03 2021 at 09:26):From: Florian Faissole <F.Faissole@fr.merce.mee.com>
Dear all,
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:
https://www.mitsubishielectric-rce.eu/job/machine-checked-verification-of-domain-specific/
If you are interested or would like to have additional information, do not hesitate to contact us.
Contact for application: Magali BRANCHEREAU (jobs@fr.merce.mee.com<mailto:jobs@fr.merce.mee.com>)
Contact for further technical enquiry: Florian FAISSOLE (f.faissole@fr.merce.mee.com<mailto:f.faissole@fr.merce.mee.com>) ; Benoît BOYER (b.boyer@fr.merce.mee.com<mailto:b.boyer@fr.merce.mee.com>).
Best regards,
Florian Faissole.
Last updated: Jan 04 2025 at 20:18 UTC