BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:IC Colloquium: Hardware verification using high-level design langu
 ages
DTSTART:20220303T100000
DTEND:20220303T110000
DTSTAMP:20260407T020829Z
UID:a1d066cd722991ccb9f822416acd29983f453f908fe39cca22c5a9dc
CATEGORIES:Conferences - Seminars
DESCRIPTION:By: Thomas Bourgeat - MIT\nIC Faculty candidate\n\nAbstract\nV
 erification of hardware designs is a significant part of the hardware deve
 lopment cycle because post-silicon errors cause inordinate delays and expe
 nses.\n \nStandard hardware verification relies on heavy testing and boun
 ded model-checking. Both are expensive and often incomplete. Completeness 
 is achievable\, for example using interactive theorem provers\, but it typ
 ically requires hundred-lines-long invariants that architects find unintui
 tive.\n \nIn this talk\, I will present several aspects of a design and v
 erification methodology that I developed over the last few years. This met
 hodology enables architects to prove the correctness of designs such as a 
 pipelined processor quickly\, automatically\, and using only a few lines o
 f high-level invariants.\n \nTo illustrate this methodology\, I will star
 t by introducing a high-level hardware design language inspired by Bluespe
 c that lends itself to verification while retaining synthesizability to ci
 rcuits.  I will show how this language makes it possible to decouple proo
 fs of performance properties from proofs of functional correctness\, and h
 ow it reduces the semantics of a hardware module to the effect of individu
 al methods\, without worrying about concurrency.\nI will then illustrate t
 he kind of verifications projects that these developments enable: security
  proofs\, using performance models to capture a wide class of often-studie
 d security properties\; and lower-cost functional correctness proofs\, usi
 ng intuitive invariants that match the way architects reason about correct
 ness. \n\nBio\nThomas is a PhD candidate in CSAIL at MIT\, co-advised by 
 Arvind and Adam Chlipala. He works in computer architecture and programmin
 g languages\, leveraging high-level hardware programming languages to desi
 gn hardware that can be formally proven to verify its specification. Beyon
 d hardware design languages\, Thomas works on building processors and doma
 in-specific accelerators\, and has an interest for computer-architecture s
 ecurity.\n\nMore information 
LOCATION:BC 420 https://plan.epfl.ch/?room==BC%20420 https://epfl.zoom.us/
 j/61653753444?pwd=UURRS3BNYllpZFd1V0lDd0RZRTR6QT09
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR