Dr. Andres Goens , The University of Edinburgh, School of Informatics
Towards compilers for correct-by-construction hardware design
, 16:00 - 17:30
Barkhausen-Bau, Room BAR E85 // Online Access below , Dresden
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.
Meeting ID: 663 7595 3176