IC Colloquium: Hardware verification using high-level design languages
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
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