Muncake: Ein beweisgenerierender Übersetzer zur Überprüfung der Hardware-Bisimulation
Albert Rizaldi von PlanV stellt Muncake vor: einen beweisproduzierenden Übersetzer, der Hardware-Modelle, die in HOL4 geschrieben sind, in eine Reihe von Assertions in der Property Specification Language (PSLs) umwandelt, die mit dem kostenlosen und quelloffenen Modellprüfer Yosys überprüft werden können. Wenn diese Behauptungen den Yosys-Modellprüfer bestehen, ist mathematisch garantiert, dass sich das Modell in HOL4 und der RTL-Code gleich verhalten.
Die vollständige Aufzeichnung findet sich hier:
Unser Redner
Dr. Albert Rizaldi ist Formal Verification Engineer bei PlanV.