Muncake: a proof-producing translator for checking hardware bisimulation
Albert Rizaldi from PlanV presents Muncake: a proof-producing translator from hardware models written in HOL4 to a set of assertions in Property Specification Language (PSLs) that can be checked with free and open-sourced model checker Yosys. When this set of assertions passes Yosys model checker, it is mathematically guaranteed that the model in HOL4 and the RTL code behave equivalently.
The full recording can be found here:
Our Speaker
Dr. Albert Rizaldi works as a Formal Verification Engineer at PlanV.