A Formally Verified Procedure for Width Inference in FIRRTL
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866917209747488768 |
|---|---|
| author | Wang, Keyin Shi, Xiaomu Liu, Jiaxiang Wu, Zhilin Chen, Taolve Song, Fu Jansen, David N. |
| author_facet | Wang, Keyin Shi, Xiaomu Liu, Jiaxiang Wu, Zhilin Chen, Taolve Song, Fu Jansen, David N. |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2601_12813 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | A Formally Verified Procedure for Width Inference in FIRRTL Wang, Keyin Shi, Xiaomu Liu, Jiaxiang Wu, Zhilin Chen, Taolve Song, Fu Jansen, David N. Programming Languages Logic in Computer Science 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. |
| title | A Formally Verified Procedure for Width Inference in FIRRTL |
| topic | Programming Languages Logic in Computer Science |
| url | https://arxiv.org/abs/2601.12813 |