Type-Driven Development of SoC Architectures.

Jan gave a talk about his work at SPLS Oct ’18 at the University of Strathclyde. This event is being hosted by the MSP Group of the School of Computer and Information Sciences.

This talk extends upon early talks given to the MSP, FP-StAnd, and PL Interest groups, with an even more complete picture of the language and how it is used. Sadly, this talk won’t be Chalk&Talk, and a more conventional slidedeck will be used.

The protocols that describe the interactions between IP Cores on System-on-a-Chip (SoC) architectures are well-documented, describing not only the structural properties of the physical interfaces but also the behaviour of the emanating signals. However, there is a disconnect between the design of SoC architectures, their formal description, and the verification of their implementation in known hardware description languages.

Within the Border Patrol project we are investigating how to model the structural and behavioural properties of SoC architectures using state-of-the-art advances in programming language research. Namely, we are investigating how dependent types and session types can be leveraged to model hardware communication at design and runtime.

In this talk I will discuss my work in designing a modelling language with a substructural type-system that reasons about the structure of SoC Architectures. This language provide correct-by-construction guarantees over:

• the physical structure of an interaction protocol;
• the adherence of a component’s interface to a given protocol; and
• the validity of the connections made between components.

We provide these guarantees by: (ab)using dependent types as presented within Idris; using novel ideas from programming language design such as Session Types and Thinnings; and incorporating novel ideas to reason about effectful programs, namely Hoare Monads and Resource-Dependent Algebraic Effects.

Slides are not available.