Participants

I’m John Wickerson, and one thing I’d like to get out of this workshop is: I’m curious whether there are other properties of an HLS tool – besides correctness – that formal methods could help to guarantee.

Hi, I am Jianyi Cheng from Imperial College London. I have a talk today about optimizing HLS using Petri nets. People use formal methods to PROVE stuff, and I use formal methods to IMPROVE stuff. I am here to chat about anything!

Hi, I am Yann Herklotz from Imperial College. I am presenting today about implementing loop pipelining for verified high-level synthesis. I’m hoping to bring interactive theorem provers like Coq to HLS.

Hi, I’m Ben Reynwar from Information Sciences Institute, USC. I mostly do digital design and would love to be able to use human-assisted HLS to transform a high-level specification into a design and corresponding proof of equivalence. I’m also interested in any other methods that would make generating proofs less labor intensive.

Hello, I am Debjit Pal from Cornell University/University of Illinois at Chicago. I primarily work on the multiple facets of post-silicon and pre-silicon SoC verification using formal and simulation based techniques. Recently, I am exploring application of formal methods in verifying optimizations in domain-specific languages in the HLS context. Given HLS is also becoming commonplace in ASIC/SoC design, I am hoping to bring in developments from HLS community for agile SoC design.

Hi, I’m Joshua Einstein-Curtis from RadiaSoft, LLC. We consult on designs for large and small physics experiments, as well as associated electronics. Formal methods could be valuable at many levels in some of these designs.

Hi, I am Loïc Sylvestre from Sorbonne Université. I’m interested in design and FPGA-based implementation of programming languages with an emphasis on safety, correctness and expressiveness.

Hi, I’m Joe Warner from Chicago Trading Company. I work as a FPGA design engineer focused on ultra low latency designs. I’m hoping to learn more about where HLS is headed and how I can better leverage it in the future while being confident about its correctness.

Hi, I’m Rezgar Sadeghi from the University of Tehran, Iran. I’ve worked on High level synthesis tools for FPGA implementation.I’m interested in learning more and more about HLS for heterogeneous new architectures.

Hi everyone, I am Lana Josipovic from ETH Zurich. I work on different aspects of high-level synthesis, primarily on generating dynamically scheduled, dataflow circuits from high-level code. I am interested in exploiting formal methods to guarantee the correctness of such circuits and to improve them in various ways (e.g., area and performance optimization, introducing new circuit behaviors and properties).

Hi! I am Rubén Salvador, from CentraleSupélec in Rennes, France. I have a rather standard background in FPGA design using RTL, and I am mostly doing hardware security and architectural exploration (security for DNN accelerators, HW/SW co-design for space computers using COTS platforms). I have in fact little experience in HLS, and certainly none in formal methods. So, I basically registered to learn :-) and see how I can use this for future research.