Certified hardware for regexp matching: A rocq library and its workflow
summary
A rocq library implements a certified synthesize function that turns a regular expression DSL into a Haskell matcher, uses clash to generate VERILOG, and runs the resulting circuit on an FPGA via Yosys. The workflow enforces a three-layer design (abstract MathComp, concrete reifications, synthesis-friendly types) so extracted code stays clash-synthesizable. Benchmarks: extraction takes 5s and 25s for two Brill examples, clash VERILOG generation ~2.5 hours, resulting matchers use less than 200 cells and run above 358 MHz.
AI-written summary · about
chapters (12)
- 0:00Introduction
- 1:50Software to hardware with Clash
- 3:59Specifying regular expressions in Rocq
- 6:07Three-layer design
- 11:06Finite types and functions
- 13:20NFA in Rocq
- 17:42General regex proofs
- 18:23Experimental results
- 20:11End-to-end verification
- 21:16Q&A
- 24:29Q&A
- 26:16Q&A
related talks
29mVerified and Efficient Matching of Regular Expressions with Lookaround
51mSynthesis and Verification for All
23mTowards Verifiable System Code using a DSL Compiled to Efficient and Readable C Code
19mLoop Rerolling for Hardware Decompilation
27mClash: Haskell as an HDL
19mCertified Compilers à la Carte
09mBreaking the RISC-V Processor Customization Barrier with Formal Verification
56mProof Assistants At the Hardware-Software Interface