Quantitative Type-Systems support fine-grained reasoning about term usage in our programming languages. Hardware Design Languages are another style of language in which quantitative typing would be beneficial. When wiring components together we must ensure that there are no unused ports, dangling wires, or accidental fan-ins and fan-outs. Although many wire usages checks are detectable using static analysis tools, such as Verilator, quantitative typing supports making these extrinsic checks an intrinsic aspect of the type-system. With quantitative typing of bound terms, we can provide design-time checks that all wires and ports have been used, and ensure that all wiring decisions are explicitly made, and are neither implicit nor accidental.

We showcase the use of quantitative types in hardware design languages by detailing how we can retrofit quantitative types onto SystemVerilog netlists. Netlists are gate-level descriptions of hardware the are produced as the result of synthesis, it is from these netlists that hardware is generated (fabless or fabbed). First, we present a simple structural type-system for SystemVerilog netlists that demonstrates how we can type netlists using standard structural techniques and what it means for netlists to be type-safe but still lead to ill-wired designs. We then detail how to retrofit the type-system with quantitative types and make the type-system sub-structural and detail how our new type-safety result ensures that wires and ports are used once.

Our ideas have been proven both practically and formally by realising our work in Idris2, through which we can construct a verified language implementation that can type-check existing designs. From this work we can look to promote quantitative typing back up the synthesis chain to a more comprehensive hardware description language; and to help develop new and better hardware description languages with quantitative typing.