Modern Systems-on-a-Chip (SoC) are constructed by composition of IP (Intellectual Property) cores. There are well described interaction protocols for communication between IP Cores. 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.
Wed 17 JulDisplayed time zone: Belfast change
13:30 - 15:10 | |||
13:30 20mResearch paper | Transient Typechecks are (Almost) Free Research Papers Richard Roberts Victoria University of Wellington, Stefan Marr University of Kent, Michael Homer Victoria University of Wellington, James Noble Victoria University of Wellington DOI Media Attached | ||
13:50 20mResearch paper | A Typing Discipline for Hardware Interfaces Research Papers DOI Media Attached | ||
14:10 20mResearch paper | Minimal Session Types Research Papers Alen Arslanagić University of Groningen, Jorge A. Pérez University of Groningen, The Netherlands, Erik Voogd University of Oslo DOI Media Attached | ||
14:30 20mResearch paper | Julia's Efficient Algorithm for Subtyping Unions and Covariant Tuples Research Papers Benjamin Chung Northeastern University, Francesco Zappa Nardelli Inria, Jan Vitek Northeastern University DOI Media Attached | ||
14:50 20mResearch paper | On Satisfiability of Nominal Subtyping with Variance Research Papers Aleksandr Misonizhnik Saint-Petersburg State University, Dmitry Mordvinov Saint-Petersburg State University, JetBrains Research DOI Media Attached |