wky17/VerinferWidth: Artifact for Paper [A Formally Verified Procedure for Width Inference in FIRRTL]

This artifact contains the implementation and formalization accompanying the paper A Formally Verified Procedure for Width Inference in FIRRTL(ESOP2026). It includes: A Coq formalization of a width inference algorithm and its correctness proofs An OCaml implementation of a complete procedure for solving the width inference problem in FIRRTL Evaluation datasets and scripts to reproduce the experiments from the paper Abstract FIRRTL is an intermediate representation language for Register Transfer Level (RTL) hardware designs. In FIRRTL programs, the bit widths of some components may not be given explicitly, thus they must be inferred during compilation. In mainstream FIRRTL compilers such as firtool, the width inference is conducted by a compilation pass called InferWidths, which may fail even for simple FIRRTL programs. In this paper, we investigate the width inference problem for FIRRTL programs. We show that if the constraint obtained from a FIRRTL program is satisfiable, there must exist a unique least solution. Based on this result, we propose a complete procedure for solving the width inference problem, which can handle programs while firtool may fail. We implement the procedure in Rocq and prove its correctness. From the Rocq implementation, we extract an OCaml implementation, which is the first formally verified InferWidths pass. Extensive experiments demonstrate that it can solve more instances than the official InferWidths pass in firtool using less time.