Document Open Access Logo

A Typing Discipline for Hardware Interfaces (Artifact)

Authors Jan de Muijnck-Hughes , Wim Vanderbauwhede

PDF

Artifact Description

Thumbnail PDF
PDF
DARTS.5.2.14.pdf
  • Filesize: 404 kB
  • 3 pages

Document Identifiers

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)
    0
    PDF Downloads
    0
    Metadata Views

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.

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

Author Details

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

Funding

This work is part of Border Patrol: Improving Smart Device Security through Type-Aware Systems Design - EPSRC Project http://gow.epsrc.ac.uk/NGBOViewGrant.aspx?GrantRef=EP/N028201/1.

Artifact

  MD5 Sum: 0636fbdc64a9f3308c05e32b1a56eb2e (Get MD5 Sum)

Related Article

  • Jan de Muijnck-Hughes and Wim Vanderbauwhede, "A Typing Discipline for Hardware Interfaces", in 33rd European Conference on Object-Oriented Programming (ECOOP 2019), LIPIcs, Vol. 134, pp. 6:1 - 6:27, 2019. https://dx.doi.org/10.4230/LIPIcs.ECOOP.2019.6

References

  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
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact