skip to contentW3CSVG

Home

FLASHLIGHT is the first workshop on Formal Methods in High-Level Synthesis. It will be held as part of the 30th IEEE International Symposium on Field-Programmable Custom Computing Machines (FCCM ‘22).

Why?

With FPGAs now widespread, there is huge demand for tools that make them easier to program. High-level synthesis (HLS) is a particularly compelling solution, as it promises to make the computational power and energy efficiency of FPGAs available to software engineers who may not have a background in hardware design. There has, accordingly, been a huge amount of HLS research in recent years, much of which has been presented at FCCM and its sister conferences.

We believe that there is a considerable opportunity to improve the reliability of HLS tools, as well as the quality of the hardware designs they produce, through the application of formal methods. Formal methods include tools such as proof assistants, static analysers, and automatic verifiers, and also techniques such as formal semantics for specifying the source/target languages.

Work presented at FCCM in recent years indicates a substantial number of researchers in the community with interests at the intersection of HLS and formal methods. For instance, static analysis has been applied to hardware circuits formalised as Petri nets in order to determine initiation intervals for pipelines; fuzzing methods have been used to test HLS tools, motivating the need to formally verify the HLS process; and the Coq proof assistant has been employed to verify that HLS optimisations respect dependencies in the source code. More generally, “translation validation” and “formal verification” have long been popular topics in FCCM papers.

What?

We intend this workshop to provide a forum to bring these people together to share ideas. We hope that it will be valuable both to HLS experts who are interested in how formal methods could improve the correctness and efficiency of HLS tools, and to formal methods experts who would like to learn about HLS as an interesting and worthwhile application domain for their techniques.

When?

Wednesday 18th May 2022, 09:00 - 12:00 (New York time, EST)

Where?

Verizon Executive Center, Cornell Tech, 2 West Loop Road, Roosevelt Island, New York City, NY 10044

Who?

FLASHLIGHT was brought to you by:

  • Jianyi Cheng, Imperial College London, UK, who talked about “Optimizing HLS using Petri Nets”
  • Yann Herklotz, Imperial College London, UK, who talked about “Towards Loop Pipelining for a Verified High-Level Synthesis Tool” [slides]
  • Lana Josipović, ETH Zürich, Switzerland (co-chair)
  • John Wickerson, Imperial College London, UK (co-chair)

With contributions from:

  • Ecenur Üstün, Cornell University, who talked about “Optimizing Large Integer Multiplication in HLS using Equality Saturation”
  • Debjit Pal, Cornell University
  • Rajit Manohar, Yale University
  • Rachit Nigam, Cornell University, who talked about “Time-Sensitive Interfaces for Hardware Modules”
  • Christian Pilato, Politecnico di Milano, who talked about “Designing memory architectures with high-level synthesis: What could possibly go wrong?”
  • Michael Adler, Intel