TY - GEN
T1 - A typing discipline for hardware interfaces
AU - de Muijnck-Hughes, Jan
AU - Vanderbauwhede, Wim
N1 - Funding Information: Funding This work is part of Border Patrol: Improving Smart Device Security through Type-Aware Systems Design (EP/N028201/1) and has been sponsored by an EPSRC funding call on Trust, Identity, Privacy and Security in the Digital Economy.
Funding Information: This work is part of Border Patrol: Improving Smart Device Security through Type-Aware Systems Design (EP/N028201/1) and has been sponsored by an EPSRC funding call on Trust, Identity, Privacy and Security in the Digital Economy. The authors would like to thank the anonymous reviewers for commenting on the paper, and also various members of Scottish Programming Language Community (SPLS) for their helpful comments on early versions of the work.
Publisher Copyright: © Jan de Muijnck-Hughes and Wim Vanderbauwhede.
PY - 2019/7/19
Y1 - 2019/7/19
N2 - 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.
AB - 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.
KW - AXI
KW - dependent types
KW - substructural typing
KW - system-on-a-chip
KW - theory of computation
KW - intellectual property
KW - computer hardware description languages
KW - intellectual property core
KW - modeling languages
KW - programmable logic controllers
KW - correct-by-construction
UR - http://www.scopus.com/inward/record.url?scp=85069511106&partnerID=8YFLogxK
U2 - 10.4230/LIPIcs.ECOOP.2019.6
DO - 10.4230/LIPIcs.ECOOP.2019.6
M3 - Conference contribution book
AN - SCOPUS:85069511106
T3 - Leibniz International Proceedings in Informatics, LIPIcs
BT - 33rd European Conference on Object-Oriented Programming, ECOOP 2019
A2 - Donaldson, Alastair F.
T2 - 33rd European Conference on Object-Oriented Programming, ECOOP 2019
Y2 - 15 July 2019 through 19 July 2019
ER -