Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Formally Verified Procedure for Width Inference in FIRRTL

Keyin Wang, Xiaomu Shi, Jiaxiang Liu, Zhilin Wu, Taolve Chen, Fu Song, David N. Jansen

TL;DR

This work addresses the challenge of inferring unspecified bit-widths in FIRRTL by formalizing the problem as FIRWINE constraints and proving that satisfiable instances have a unique least solution. It presents a complete width-inference procedure that reduces inequalities to $\Phi_W$-constraints, analyzes dependency graphs with SCCs, and distinguishes expansive versus nonexpansive components to guide solving. The procedure is implemented and formally verified in Rocq, with an OCaml extraction that yields the first formally verified InferWidths pass; extensive experiments show the approach solves more instances and often outperforms the official firtool and competes with industrial ILP solvers. Together, these results mark a significant step toward a formally verified FIRRTL compiler and demonstrate a scalable, verifiable solver for a practical hardware-width inference problem.

Abstract

FIRRTL is an intermediate representation language for Register Transfer Level (RTL) hardware designs. In FIRRTL programs, the bit widths of many components are not specified explicitly and must be inferred during compilation. In mainstream FIRRTL compilers, such as the official compiler firtool, width inference is conducted by a compilation pass referred to as InferWidths, which may fail even for simple FIRRTL programs. In this paper, we thoroughly investigate the width inference problem for FIRRTL programs. We show that, if the constraints obtained from a FIRRTL program are satisfiable, there exists a unique least solution. Based on this result, we propose a complete procedure for solving the width inference problem. We implement it in the interactive theorem prover Rocq and prove its functional correctness. From the Rocq implementation, we extract an OCaml implementation, which is the first formally verified implementation of the InferWidths pass. Extensive experiments demonstrate that our approach can solve more instances than the official InferWidths pass in firtool, normally with high efficiency.

A Formally Verified Procedure for Width Inference in FIRRTL

TL;DR

This work addresses the challenge of inferring unspecified bit-widths in FIRRTL by formalizing the problem as FIRWINE constraints and proving that satisfiable instances have a unique least solution. It presents a complete width-inference procedure that reduces inequalities to -constraints, analyzes dependency graphs with SCCs, and distinguishes expansive versus nonexpansive components to guide solving. The procedure is implemented and formally verified in Rocq, with an OCaml extraction that yields the first formally verified InferWidths pass; extensive experiments show the approach solves more instances and often outperforms the official firtool and competes with industrial ILP solvers. Together, these results mark a significant step toward a formally verified FIRRTL compiler and demonstrate a scalable, verifiable solver for a practical hardware-width inference problem.

Abstract

FIRRTL is an intermediate representation language for Register Transfer Level (RTL) hardware designs. In FIRRTL programs, the bit widths of many components are not specified explicitly and must be inferred during compilation. In mainstream FIRRTL compilers, such as the official compiler firtool, width inference is conducted by a compilation pass referred to as InferWidths, which may fail even for simple FIRRTL programs. In this paper, we thoroughly investigate the width inference problem for FIRRTL programs. We show that, if the constraints obtained from a FIRRTL program are satisfiable, there exists a unique least solution. Based on this result, we propose a complete procedure for solving the width inference problem. We implement it in the interactive theorem prover Rocq and prove its functional correctness. From the Rocq implementation, we extract an OCaml implementation, which is the first formally verified implementation of the InferWidths pass. Extensive experiments demonstrate that our approach can solve more instances than the official InferWidths pass in firtool, normally with high efficiency.
Paper Structure (4 sections, 1 theorem, 2 figures)

This paper contains 4 sections, 1 theorem, 2 figures.

Table of Contents

  1. Introduction
  2. FIRRTL and the width inference problem
  3. The width inference problem in FIRRTL
  4. Existence of a unique least solution

Key Result

proposition thmcounterproposition

Each inequality $w_{{\tt x}} \ge w_{\tt e}$ formulated in a width inference problem can be transformed into an equivalent $\Phi_{W}$-constraint.

Figures (2)

  • Figure 1: A FIRRTL program with unspecified widths
  • Figure 2: A FIRRTL program with unspecified widths and circular dependencies

Theorems & Definitions (2)

  • definition thmcounterdefinition: $\Phi_{W}$-constraints
  • proposition thmcounterproposition