Formalising the (Sub-)Structural Aspects of SystemVerilog

Today, I am very pleased to be traveling all the way to the Programming Languages and Systems Group at the University of Kent in Canterbury.

This is not the first time that I have given a talk at Kent. Years a go I spoke at a CryptoForma workshop hosted there. The topic was on linking dependent types, session types, and protocol implementation validation. A topic that I should revisit once my restraints are released, and I am unshackled!

Regardless, Canterbury is a nice little town from what I remember and over the years I have been fortunate to meet many of the PLAS members who have, so far, been very nice. Oh btw Kent Computing are hiring.

Anywhodate: 2021-03-08-PLAS.md —Today’s talk ¹ will be about my current work reasoning about physical hardware design as part of the Border Patrol Project, and tangentially the AppControl Project.

The abstract is:

Hardware design is becoming increasingly commoditised and it might bethe case that several components of your design are encrypted bitstreams bought from third-parties. Here we must have trust that the encrypted bitstreams do what they are supposed to. In the Border Patrol Project ² we are interested in being able to reason about the structure & behaviour of designs as a whole, regardless of if we can inspect each module down to the individual gates.

In this talk I will introduce System-V ³, a typed lambda calculus that can be used to capture physical hardware design. System-V is based upon the well-known hardware description and verification language SystemVerilog. I will show how a System-V design can model physicalhardware, and its type-system enforce correct-by-construction wiring. I will also show how System-V can enforce sub-structural properties overdata-types as defined in the SystemVerilog standard using techniques borrowed from maths-a-magical structured programming. With System-V we hope to establish a foundational formalism that we can later extend to reason about other interesting properties such as module interface design, quantitative wire usage, and behaviour.

Slides are not available. To see the slides ask me to give a talk!

This talk extends upon an SPLS talk I gave in October 2021.