Wiring circuits is easy as {0,1,w}, or is it...

de Muijnck-Hughes, Jan and Vanderbauwhede, Wim; Ali, Karim and Salvaneschi, Guido, eds. (2023) Wiring circuits is easy as {0,1,w}, or is it... In: 37th European Conference on Object-Oriented Programming, ECOOP 2023. Leibniz International Proceedings in Informatics, LIPIcs . Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, USA. ISBN 9783959772815 (https://doi.org/10.4230/LIPIcs.ECOOP.2023.8)

[thumbnail of Muijnck-Hughes-Vanderbauwhede-ECOOP-2023-Wiring-circuits-is-easy-as]
Preview
 Text. Filename: Muijnck_Hughes_Vanderbauwhede_ECOOP_2023_Wiring_circuits_is_easy_as.pdf
Final Published Version
License: Creative Commons Attribution 4.0 logo
Download (1MB)| Preview

Abstract

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 usage 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, and the impact that such a quantitative type-system has when creating designs. Netlists are gate-level descriptions of hardware that are produced as the result of synthesis, and it is from these netlists that hardware is generated (fabless or fabbed). First, we present a simple structural type-system for a featherweight version of 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 language with quantitative types, 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.

ORCID iDs

de Muijnck-Hughes, Jan ORCID logoORCID: https://orcid.org/0000-0003-2185-8543 and Vanderbauwhede, Wim; Ali, Karim and Salvaneschi, Guido
CORE (COnnecting REpositories)