Well-typed models are correct models: applying state-of-the-art advances in programming language theory to systems-on-a-chip

Jan De Muijnck-Hughes, Wim Vanderbauwhede

Research output: Contribution to conferencePaperpeer-review

Abstract

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. However, there is a disconnect between the machine readable specification of these protocols and the verification of their implementation in known hardware description languages. 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. Further, it is important when connecting components together that only one signal can flow along a channel. Dependent type-systems present a rich and expressive setting that supports the precises specifi- cation of our programs properties to be stated and verified directly in the language?s type-system. Such type-systems also support reasoning about a programs substructural properties in the style of substructural typing. We can use these concepts to express model invarients directly within our model?s types and provide correctness-by-construction guarantees that our models adhere to external specifications, and are thus well-formed, at design-time using type checking. In this talk I will present my ongoing work as part of the Border Patrol project to construct a modelling languague for designing Systems-on-a-Chip. Our framework, Cordial, is designed to enrich existing Hardware Description Languages, and development environments, with static design-time mechanisms that reason about the (sub)structural properties of SoC Designs using Dependent, Session, and Quantitative Typing. Cordial?s type-system provides guarantees that the interfaces on an IP Core will be well-typed if they adhere to an external specification, and that we can guarantee that components are connected in a safe way by tracking the number of times a port is used within a design and comparing the interconnections ports. With Cordial mismatches between SoC specification and implementation become impossible thereby reducing errors, increasing designer productivity and enhancing safety and security of SoC designs.
Original languageEnglish
Publication statusPublished - 1 Sept 2019
EventScottish Seminar on Formal Modelling, Verification, and Synthesis - Glasgow, United Kingdom
Duration: 9 Sept 20199 Sept 2019

Workshop

WorkshopScottish Seminar on Formal Modelling, Verification, and Synthesis
Abbreviated titleSFMoVeS '19
Country/TerritoryUnited Kingdom
CityGlasgow
Period9/09/199/09/19

Keywords

  • systems on-a-chip
  • Intellectual Property Cores
  • programming language theory

Fingerprint

Dive into the research topics of 'Well-typed models are correct models: applying state-of-the-art advances in programming language theory to systems-on-a-chip'. Together they form a unique fingerprint.

Cite this