On Wednesday 17 July, 2019 I will be at ECOOP 2019 presenting my work on constructing a type-system for hardware interfaces. This was joint work with Wim Vanderbauwhede as part of the Border Patrol project.
To promote good academic practise (and inspired my Matthew Green’s blogging), I will describe the work here. Think of this post, and my talk on Wednesday, as an extended abstract. If you are interested then you should read the paper, it has all the gory details.
Also, if you are at ECOOP please do say hello and ask me about my work.
Reasoning about Hardware Intefaces is Hard.
Modern Systems-on-a-Chip (SoC) are constructed by composition of IP (Intellectual Property) Cores with the communication between these IP Cores being governed by well described interaction protocols e.g. AXI, APB, and LocalLink. However, there is a disconnect between the machine readable specification of these protocols and the verification of their implementation in known Hardware Description Languages (HDLs). Although tools can be written to address such separation of concerns, the tooling is often hand written and used to check hardware designs a posteriori.
IP-XACT is not Exact.
These interaction protocols are presented as standards documents in PDF formats. We can encode the structure of these protocols using machine readable formats such as IP-XACT, and IDEs utilise these descriptions when facilitating IP Core construction and verification. IP-XACT encodes the structure of these protocols agnostic to the endpoint of the involved IP Cores. These descriptions represent the structure of the channel. IP-XACT is not exact and aspects of the natural language descriptions are not encodable with it’s XML goodness. For instance, IP-XACT cannot express inter-signal dependencies, parameterisation of specifications, and value-dependent signals.
HDLs need better Types.
At the HDL level, we see mixed support for linking IP Core interfaces and their specifications. SystemVerilog has this neat feature of allowing one to describe an endpoint agnostic interface and how the interface will look when used as an endpoint—modports. However, the language’s type-system doesn’t guarantee that the interface, and its endpoints, are structurally valid nor that they are compatible. Further, these interfaces do not allow one to ensure that an endpoint’s dangling port are ones that are allowed to be dangling. A dangling interface in which a ports on an interface is optional.
Type-Systems to the rescue.
The aim of our work is to improve the security and safety of SoC design by utilising state-of-the-art concepts from programming language theory to provide greater correct-by-constructionguarantees over the structural and behavioural aspects of SoC designs. My role on the Border Patrol project is to investigate how we can use more expressive type-systems to capture the physical structure of a SoC design. Our friends at the MRG at Imperial College London are looking at capturing the behavioural aspects.
In our ECOOP paper, we have developed a dependent type-system and proof-of-concept modelling language to reason about the physical structure of hardware interfaces using user provided descriptions. Dependent type-systems present a rich and expressive setting that allows for precise program properties to be stated and verified directly in the language’s type-system. Such type-systems also support modelling of resource usage in the style of sub-structural typing. By building upon existing work from hardware design we can use these concepts to construct a type-based formal description of abstract interfaces, and formally validate that concrete component interfaces adhere to these descriptions at design-time using type checking.
Modelling information is taken from the IP-XACT standard, and existing work, to construct a model (M_AID) to represent abstract interface descriptions.
Our model construction language (L_AID) is a simple extension to the Simply Typed Lambda Calculus (STLC) and models parameterised specifications as computable functions, and allows dependencies tobe made between signals.
The type-system of L_AID follows a substructural design allowing correctness guarantees towards labelling of signals to be lifted into the type-system.
Model construction is from compilation of L_AID to M_AID instances using continuation passing.
Concrete interfaces are modelled using M_COMP to present components in a SoC with multiple interfaces.
Inspired by notions of global and local types from Session Types abstract interface specifications are treated as a global description that is projected to a local description. By embedding the projected model into the type of the interface description the model’s type-system ensures that a local type is satisfied by its global type. Further, the concept of thinnings captures a specification’s optional ports, and allows optional ports to be knowingly skipped.
Application of our framework would see it embedded within existing SoC tooling and to enrich existing HDLs with static design-time mechanisms that would make mismatches between interface specification and implementation impossible and thus reduce errors, increase design productivity and enhance safety and security of the SoC designs.
Protocol designers would have a tool (based on L_AID) to design interface specifications.
During the SoC design phase SoC designers use these specifications to annotate their components and ensure their port selections are correct.
Playing with the Framework
We are fortunate to have had an artifact published that presents the framework as it stood on submission. You can find the code on GitHub:
https://github.com/border-patrol/cordial
What’s Next?
We are extending the framework to include an orchestration aspect that would support verification of complete SoC designs against an existing specification, and seeing how we could present our work as an extension to an existing IDE or to an existing HDL.