IC Colloquium: Hardware verification using high-level design languages

Thumbnail

Event details

Date 03.03.2022
Hour 10:0011:00
Location Online
Category Conferences - Seminars
Event Language English
By: Thomas Bourgeat - MIT
IC Faculty candidate

Abstract
Verification of hardware designs is a significant part of the hardware development cycle because post-silicon errors cause inordinate delays and expenses.
 
Standard hardware verification relies on heavy testing and bounded model-checking. Both are expensive and often incomplete. Completeness is achievable, for example using interactive theorem provers, but it typically requires hundred-lines-long invariants that architects find unintuitive.
 
In this talk, I will present several aspects of a design and verification methodology that I developed over the last few years. This methodology enables architects to prove the correctness of designs such as a pipelined processor quickly, automatically, and using only a few lines of high-level invariants.
 
To illustrate this methodology, I will start by introducing a high-level hardware design language inspired by Bluespec that lends itself to verification while retaining synthesizability to circuits.  I will show how this language makes it possible to decouple proofs of performance properties from proofs of functional correctness, and how it reduces the semantics of a hardware module to the effect of individual methods, without worrying about concurrency.
I will then illustrate the kind of verifications projects that these developments enable: security proofs, using performance models to capture a wide class of often-studied security properties; and lower-cost functional correctness proofs, using intuitive invariants that match the way architects reason about correctness. 

Bio
Thomas is a PhD candidate in CSAIL at MIT, co-advised by Arvind and Adam Chlipala. He works in computer architecture and programming languages, leveraging high-level hardware programming languages to design hardware that can be formally proven to verify its specification. Beyond hardware design languages, Thomas works on building processors and domain-specific accelerators, and has an interest for computer-architecture security.

More information

Practical information

  • General public
  • Free

Contact

  • Host: Edouard Bugnion

Share