I work on developing tools to formally verify hardware correct. In particular, I am interested in using interactive theorem provers to model hardware at various levels of abstraction. Interactive theorem provers make it possible to reason about parameterised hardware designs, but also makes it possible to express and verify security properties.
I have been developing Graphiti [1], which is a graph rewriting framework which can be used to represent and transform hardware. For example, we showed that we could represent and optimise dataflow circuits by representing them as graphs. We then also showed that we could represent loopy combinational circuits using this graph language [2], including modelling a register which cannot usually be represented in existing hardware semantics. The goal is to connect different representations of hardware to enable mixed-language hardware proofs where each component can be described at the right level of abstraction.
I have the following questions I would like to discuss:
- How can we best connect automated theorem provers like IC3 to Lean 4 for hardware verification?
- Can we translate assertions as well as code in between MLIR languages?
- What would a modular semantics for hw in CIRCT look like, where we can prove functional correctness theorems about modules in isolation?
- What are the advantages and disadvantages of term-based representations compared to graph-based representations for compiler transformations and hardware semantics?
Blog post with updates: https://yannherklotz.com/verify26-position-paper