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.
@Article{demuijnckhughes_et_al:DARTS.5.2.14, author = {de Muijnck-Hughes, Jan and Vanderbauwhede, Wim}, title = {{A Typing Discipline for Hardware Interfaces}}, pages = {14:1--14:3}, journal = {Dagstuhl Artifacts Series}, ISSN = {2509-8195}, year = {2019}, volume = {5}, number = {2}, editor = {de Muijnck-Hughes, Jan and Vanderbauwhede, Wim}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.5.2.14}, URN = {urn:nbn:de:0030-drops-107919}, doi = {10.4230/DARTS.5.2.14}, annote = {Keywords: System-on-a-Chip, AXI, Dependent Types, Substructural Typing} }
0636fbdc64a9f3308c05e32b1a56eb2e
(Get MD5 Sum)
Feedback for Dagstuhl Publishing