November 24, 2025 at 3:30 PM
Title : Towards scalable verification and efficient hardware generation using verified high-level synthesis tools
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.
More...Salle Turquoise, Bâtiment ESPRIT, CRIStAL
français
English