Room 206 (2nd floor, badged access)
13 November 2025 - 15h00
Towards scalable verification and efficient hardware generation using verified high-level synthesis tools
by Yann Herklotz from VCA lab at EPFL (CH)
invited by David MONNIAUX
13 November 2025 - 15h00
Towards scalable verification and efficient hardware generation using verified high-level synthesis tools
by Yann Herklotz from VCA lab at EPFL (CH)
invited by David MONNIAUX
Abstract: Hardware design companies spend more than 60% of their time just on verifying that the chip they are designing works as intended. As the need and complexity for custom hardware accelerators increases, hardware designers have been designing hardware at different levels of abstraction, however, verification itself is usually performed directly on the final hardware.
In an attempt to improve this situation, I propose two formally verified high-level synthesis (HLS) tools called Vericert and Graphiti to generate two different kinds of hardware designs from high-level specifications written in C. Vericert statically schedules instructions to find instruction-level parallelism over hyperblocks (a set of basic blocks without loops). Graphiti, on the other hand, generates circuits with latency-insensitive components which schedule themselves at runtime. This circuit correlates directly with the dataflow graph representation of the program, and optimisations are performed using graph rewrites on this dataflow graph.
I show that these two tools are comparable with existing unverified HLS tools, and explore how graph rewriting specifically can be useful to reason about hardware and could lead to a more scalable verification environment for hardware.
NB: potentiel candidat CR CNRS
