A Typing Discipline for Hardware Interfaces (Artifact)

Authors Jan de Muijnck-Hughes , Wim Vanderbauwhede

Thumbnail PDF

Artifact Description

  • Filesize: 404 kB
  • 3 pages

Document Identifiers

Author Details

Jan de Muijnck-Hughes
  • University of Glasgow, UK
Wim Vanderbauwhede
  • University of Glasgow, UK

Cite AsGet 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)



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
  • System-on-a-Chip
  • AXI
  • Dependent Types
  • Substructural Typing


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. ARM Limited. AMBA APB Protocol, arm ihi 0024c edition, 2010. Google Scholar
  2. ARM Limited. AXI and ACE Protocol Specification, arm ihi 0022f.b edition, 2017. Google Scholar
  3. 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.
  4. Xilinx. LocalLink Interface Specification, sp006 (v2.0) edition, 2005. Google Scholar
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail