A typing discipline for hardware interfaces (Artifact)

Muijnck-Hughes, Jan de and Vanderbauwhede, Wim (2019) A typing discipline for hardware interfaces (Artifact). Dagstuhl Artifacts Ser., 5 (2). 14:1-14:3. (https://doi.org/10.4230/DARTS.5.2.14)

[thumbnail of Muijnck-Hughes-Vanderbauwhede-DAS2019-A-typing-discipline-hardware-interfaces-artifact]
Preview
 Text. Filename: Muijnck_Hughes_Vanderbauwhede_DAS2019_A_typing_discipline_hardware_interfaces_artifact.pdf
Final Published Version
License: Creative Commons Attribution 3.0 logo
Download (414kB)| Preview

Abstract

Modern Systems-on-a-Chip (SoC) are constructed by composition of IP (Intellectual Property) Cores with the communication between these IP Cores being governed by well described interaction protocols. However, there is a disconnect between the machine readable specification of these protocols and the verification of their implementation in known hardware description languages. Although tools can be written to address such a separation of concerns, such tooling is often hand written and used to check hardware designs a posteriori. We have developed a dependent type-system and proof-of-concept modelling language to reason about the physical structure of hardware interfaces respective to user provided descriptions. Our type-system provides correct-by-construction guarantees that the interfaces on an IP Core will be well-typed if they adhere to a specified standard.

CORE (COnnecting REpositories)