2026-07-22T22:31:27Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:10791 2024-03-06T11:05:07Z ddc:004 open_access

A Typing Discipline for Hardware Interfaces (Artifact) de Muijnck-Hughes, Jan Vanderbauwhede, Wim System-on-a-Chip AXI Dependent Types Substructural Typing 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Jan de Muijnck-Hughes and Wim Vanderbauwhede 2019 Is Part Of DARTS, Volume 5, Issue 2, Special Issue of the 33rd European Conference on Object-Oriented Programming (ECOOP 2019) Article Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/DARTS.5.2.14 urn:nbn:de:0030-drops-107919 https://drops.dagstuhl.de/entities/document/10.4230/DARTS.5.2.14 eng https://creativecommons.org/licenses/by/3.0/de/legalcode