In February, I gave a talk about my work on the Border Patrol at the University of Strathclyde’s, School of Computing and Information Sciences MSP 101.
This was a fun talk to prepare and deliver as the MSP101 talks are traditionally Chalk&Talk. Hopefully, I was able to convince the group that I was working on something interesting.
The protocols that describe the interactions between IP Cores on System-on-a-Chip architectures are well-documented. These protocols described 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 capture and reason about the structural and behavioural properties of SoC architectures using state-of-the-art advances in programming language research. Namely, we are investigating using dependent types and session types for the description of hardware communication.
In this talk I will discuss my work in designing a linked family of languages that captures and reasons about the topological structure of a System-on-a-Chip. These languages provide correct-by-construction guarantees over the interaction protocols themselves; the adherence of a component that connects using said protocols; and the validity of the specified connections. These guarantees are provided through abuse of indexed monads to reason about resource usage; and general (ab)use of dependent types as presented in Idris.
I will not cover all aspects of the languages but will concentrate my talk detailing the underlying theories that facilitate the correct-by-construction guarantees.
Slides are not available.