[LOPSTR+PPDP'26] Certified hardware for regexp matching: A rocq library and its workflow

Certified hardware for regexp matching: A rocq library and its workflow (Video, LOPSTR+PPDP 2026) Julin Shaji, Piyush Kurur, and Sandeep Chandran (Indian Institute of Technology Palakkad; Indian Institute of Technology Palakkad; Indian Institute of Technology Palakkad) Abstract: We present a rocq library for designing \emph{certified hardware} for regular expression matching. The library provides a \emph{certified} synthesize function that takes as input a regular expression and outputs the corresponding matcher. A workflow similar to the case of certified software is then used to generate efficient hardware – use the extraction mechanism of rocq to generate the Haskell code of the matcher and then use the clash compiler to generate its corresponding VERILOG code. This VERILOG code is then synthesized and implemented on an FPGA using the Yosys toolchain. The finitary nature of hardware circuits means that clash only deals with a subset of Haskell. Therefore, we need to ensure that the extracted Haskell code falls into this subset, which is non-trivial once a certified hardware project goes beyond a certain level of sophistication. Our library takes a layered approach to address this issue of clash synthesizability. Beyond regular expression matching, this layered design can serve as a template for similar certified hardware projects. We demonstrate the feasibility of our approach by reporting the time taken to synthesize matchers corresponding to regular expressions with the highest number of atoms and the highest number of distinct atoms from the Brill suite. We note that the corresponding matchers occupy only a small number of cells (less than 200) on an FPGA while achieving a high (more than 358 MHz) operational frequency. Presentation at the LOPSTR+PPDP 2026 symposium, August 27-29, 2026, https://icfp26.sigplan.org/home/lopstr-ppdp-2026 Sponsored by ACM SIGPLAN.