First Steps in Verified Placement, Routing and Timing
Magnus O. Myreen · 2023
Doing any formal reasoning below the boolean abstraction of hardware gates is very unusual, mostly because the models of hardware below this abstraction layer are, at least to me, vague and/or complicated. In this talk, I will present a not-so-serious work-in-progress project on formal reasoning below the level of the boolean abstraction of hardware gates. More precisely, I will explain how hardware gates realised in Conway's Game of Life can be verified and how verified circuits consisting of such gates can be developed. This project touches on verification of placement, routing and timing, which are topics I suspect formal verification in interactive theorem provers have not explored before.