Applied formal semantics in hardware compiler frameworks H/F (Mathématiques, information scientifique, logiciel)
Internship Palaiseau (Essonne)
Job description
Domaine : Mathématiques, information scientifique, logiciel
Contrat : Stage
Description du poste :
Internship context:
Chisel is a high-level Hardware Design Language (HDL) that facilitates automatic generation of synthesizable Verilog. Chisel HDL benefits from its integration over the Scala programming language, using powerful programming language features (e.g., strong type system, classes, pattern matching etc.) to advance the hardware circuit generation. Two popular processor designs written in Chisel are Rocket [1] (an in-order RISC-V core) and BOOM [2] (an out-of-order RISC-V core).
Purpose of this internship:
The internship topic is to study how to express safety and security properties in hardware designs done in Chisel HDL. The internship topic is to study how to express safety and security properties in hardware designs done in Chisel HDL.
The internship has two phases:
- a practical assessment of existing Chisel HDL
-based processor designs (like Rocket and BOOM) with respect to the language features that are used followed by
- the design (and if time allows, implementation) of an assertion language to express safety and security properties in Chisel HDL.
References:
[1] https://github.com/chipsalliance/rocket-chip
[2] https://github.com/riscv-boom/riscv-boom
Remark :
The internship will be co-advised by Mathieu Jan and Mihail Asavoae and it will take place in CEA LIST (at NanoInnov) in Palaiseau.
Requirements: interest in one of the following topics: hardware design, compilation, formal verification.
Ville : Palaiseau