License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ECOOP.2023.8
URN: urn:nbn:de:0030-drops-182010
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/18201/
de Muijnck-Hughes, Jan ;
Vanderbauwhede, Wim
Wiring Circuits Is Easy as {0,1,ω}, or Is It...
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.
BibTeX - Entry
@InProceedings{demuijnckhughes_et_al:LIPIcs.ECOOP.2023.8,
author = {de Muijnck-Hughes, Jan and Vanderbauwhede, Wim},
title = {{Wiring Circuits Is Easy as \{0,1,\omega\}, or Is It...}},
booktitle = {37th European Conference on Object-Oriented Programming (ECOOP 2023)},
pages = {8:1--8:28},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-281-5},
ISSN = {1868-8969},
year = {2023},
volume = {263},
editor = {Ali, Karim and Salvaneschi, Guido},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2023/18201},
URN = {urn:nbn:de:0030-drops-182010},
doi = {10.4230/LIPIcs.ECOOP.2023.8},
annote = {Keywords: Hardware Design, Linear Types, Dependent Types, DSLs, Idris, SystemVerilog, Netlists}
}
