License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ECOOP.2019.6
URN: urn:nbn:de:0030-drops-107983
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2019/10798/
Go to the corresponding LIPIcs Volume Portal

de Muijnck-Hughes, Jan ; Vanderbauwhede, Wim

A Typing Discipline for Hardware Interfaces

pdf-format:
LIPIcs-ECOOP-2019-6.pdf (0.6 MB)

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 separation of concerns, the 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 using 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.

BibTeX - Entry

@InProceedings{demuijnckhughes_et_al:LIPIcs:2019:10798,
  author =	{Jan de Muijnck-Hughes and Wim Vanderbauwhede},
  title =	{{A Typing Discipline for Hardware Interfaces}},
  booktitle =	{33rd European Conference on Object-Oriented Programming (ECOOP 2019)},
  pages =	{6:1--6:27},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-111-5},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{134},
  editor =	{Alastair F. Donaldson},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2019/10798},
  URN =		{urn:nbn:de:0030-drops-107983},
  doi =		{10.4230/LIPIcs.ECOOP.2019.6},
  annote =	{Keywords: System-on-a-Chip, AXI, Dependent Types, Substructural Typing}
}

Keywords: System-on-a-Chip, AXI, Dependent Types, Substructural Typing
Collection: 33rd European Conference on Object-Oriented Programming (ECOOP 2019)
Issue Date: 2019
Date of publication: 10.07.2019
Supplementary Material: ECOOP 2019 Artifact Evaluation approved artifact available at https://dx.doi.org/10.4230/DARTS.5.2.14

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI