| 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 given explicitly, which must be inferred during compilation. In mainstream FIRRTL compilers such as the official compiler firtool, the 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 constraint obtained from a FIRRTL program is satisfiable, there must exist a unique least solution. Based on this foundational result, we propose a complete procedure for solving the width inference problem, which can handle FIRRTL programs where firtool may fail. We implement the procedure 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 InferWidths pass. Extensive experiments demonstrate that it can solve more instances than the official InferWidths pass in firtool, normally with high efficiency. |
下载中心
会议室预定
电子邮箱