Upcoming Events

Abstract:

Verification and formal methods have long been embraced by hardware manufacturers. However, these are usually used late in the design process, at the Register Transfer Level.   On the other hand, verification in programming languages, while less widespread, has seen many promising advances. In this talk we will explore ongoing work to bring some of these advances to hardware design methods. By raising the level of abstraction, we can reason about designs at an earlier stage in the design process. We explore using the Lean  theorem prover to build domain-specific languages for pipeline design, as well as  verify properties about memory consistency models and the existence of side channels. We also discuss language methods, for streamlining this process and improving proof automation.