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

Jan de Muijnck-Hughes*, Wim Vanderbauwhede*

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

32 Downloads (Pure)

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.

Original languageEnglish
Title of host publication37th European Conference on Object-Oriented Programming, ECOOP 2023
EditorsKarim Ali, Guido Salvaneschi
Place of PublicationWadern, Germany
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Number of pages28
ISBN (Electronic)9783959772815
DOIs
Publication statusPublished - 8 Jul 2023
Event37th European Conference on Object-Oriented Programming, ECOOP 2023 - Seattle, United States
Duration: 17 Jul 202321 Jul 2023

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
Volume263
ISSN (Print)1868-8969

Conference

Conference37th European Conference on Object-Oriented Programming, ECOOP 2023
Country/TerritoryUnited States
CitySeattle
Period17/07/2321/07/23

Keywords

  • dependent types
  • DSLs
  • hardware design
  • Idris
  • linear types
  • netlists
  • SystemVerilog

Fingerprint

Dive into the research topics of 'Wiring circuits is easy as {0,1,w}, or is it...'. Together they form a unique fingerprint.

Cite this