MRPHS: Enabling Transaction-level Deductive Formal Verification Through PDVL
Tobias Strauch
https://fossi-foundation.org/latch-up...
Theorem-Proving is also called “Deductive Formal Verification, DFV”. In this presentation I will give an overview of open source DFV projects as well as introduce my own project. I developed the language PDVL to revolutionize design verification. One of the verification disciplines that PDVL will have a major impact on is DFV. In this presentation, I will show how the aspect-oriented and transaction-level based approach of the Programming Design and Verification Language (PDVL) provides important advantages for transforming your design and verification goals into Gallina code that can be used for assertions and theorem proving by "The Rocq Prover” (formerly known as the Coq Proof Assistant). A regular paper on this work was accepted at the DATE 2024 conference. The open-source files can be found here: PDVL specification: https://github.com/cloudxcc/PDVL PDVL examples: https://github.com/cloudxcc/PDVL_Exam... MRPHS compiler: https://github.com/cloudxcc/MRPHS.
The FOSSi Foundation is proud to announce Latch-Up, a conference dedicated to free and open source silicon.
Latch-Up: a weekend of presentations and networking for the open source silicon community, much like its European sister conference ORConf.
Produced by NDV: / @nextdayvideo
OpenHardware
Fri Apr 19 13:20:00 2024 at b45r230