A Mechanised, Bidirectional Type System for Bit-Width Determination in SystemVerilog

Abstract

Abstract SystemVerilog remains one of the most widely used languages for designing and verifying digital circuits. Despite its importance, the SystemVerilog standard suffers from ambiguities, which can lead to inconsistent implementations and portability challenges. Formal methods can provide precise semantics to address these issues. We focus on SystemVerilog’s mechanism for determining the bit-width of each expression that appears in a design. This is surprisingly subtle because an expression’s bit-width can depend on both its children and its parents. First, we develop a Rocq formalization of the existing IEEE standard for SystemVerilog. We then construct a bidirectional type system that captures the context-dependent nature of SystemVerilog expressions and prove it equivalent to our formalization of the standard using Rocq. We provide a reference implementation that determines bit-widths in linear time and prove its correspondence to our system, also in Rocq. Based on these results, we propose revisions to the text of the standard that reduce redundancy and improve precision.