DARTS.5.2.14.pdf
- Filesize: 404 kB
- 3 pages
Document
A Typing Discipline for Hardware Interfaces (Artifact)
Authors
Jan de Muijnck-Hughes 
,
Wim Vanderbauwhede
-
Part of:
Issue:
Special Issue of the 33rd European Conference on Object-Oriented Programming (ECOOP 2019)
Volume: DARTS, Volume 5 (ECOOP 2019)
Conference: European Conference on Object-Oriented Programming (ECOOP)
Journal: Dagstuhl Artifacts Series (DARTS) - License:
Creative Commons Attribution 3.0 Germany license
- Publication Date: 2019-07-12
Artifact Description
Document Identifiers
Author Details
Cite As Get BibTex
Jan de Muijnck-Hughes and Wim Vanderbauwhede. A Typing Discipline for Hardware Interfaces (Artifact). In Special Issue of the 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Dagstuhl Artifacts Series (DARTS), Volume 5, Issue 2, pp. 14:1-14:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/DARTS.5.2.14
Artifact
DARTS-5-2-14-artifact-0636fbdc64a9f3308c05e32b1a56eb2e.tar.gz
(Filesize: 1.31 GB)
MD5 Sum:
0636fbdc64a9f3308c05e32b1a56eb2e
(Get MD5 Sum)
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.
Subject Classification
ACM Subject Classification
- Theory of computation → Type theory
- Hardware → System on a chip
- Software and its engineering → System description languages
Keywords
- System-on-a-Chip
- AXI
- Dependent Types
- Substructural Typing
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
-
ARM Limited. AMBA APB Protocol, arm ihi 0024c edition, 2010.
-
ARM Limited. AXI and ACE Protocol Specification, arm ihi 0022f.b edition, 2017.
- Edwin Brady. Idris, a general-purpose dependently typed programming language: Design and implementation. J. Funct. Program., 23(5):552-593, 2013. URL: http://dx.doi.org/10.1017/S095679681300018X.
-
Xilinx. LocalLink Interface Specification, sp006 (v2.0) edition, 2005.