Are you an EPFL student looking for a semester project?
Work with us on data science and visualisation projects, and deploy your project as an app on top of GraphSearch.
This lecture covers the concept of formally verifying Chisel designs using SMT solvers. It explains Chisel as a hardware construction language in Scala, the use of SMT solvers to prove hardware design properties, and examples like delayed assertions and proofs by induction on state. It also delves into formal verification of communication protocols like AXI4, emphasizing the importance of loop invariants, preconditions, and postconditions in digital circuit design.