Trustworthy Tuesday #9 - Let them eat (mun)cake!

Description

This month, Trustworthy Tuesday is all about cakes.

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.

Verifying hardware design against a golden model is easier and more intuitive than compliance checking against a set of correctness properties. This model-based flow also fits nicely into common engineering practices where a design is first described in a higher level of abstraction before being refined to an implementation.