A Type-System for describing System-on-a-Chip Architectures – Jan De Muijnck-Hughes

Event details

  • When: 5th April 2018 12:00 - 13:00
  • Where: Cole 1.33a
  • Format: Talk


A Type-System for describing System-on-a-Chip Architectures



The protocols that describe the interactions between IP Cores on
System-on-a-Chip (SoC) 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 to capture and reason about hardware communication.

In this talk I will discuss my work in designing a dependent type-
system and corresponding language that captures and reasons about the
topological structure of a System-on-a-Chip. This language provides
correct-by-construction guarantees over:

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

We provide these guarantees through the (ab)use of dependent types as
presented in Idris; and abuse of indexed monads to reason about
resource usage.

Given time I will give an account of how this language enables
reasoning about SoC behaviour when considered in conjunction with
Session Types.