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 (jobs at fr.merce.mee.com)