Please login to view the entire Verification Horizons article.
Please register or login to view.
The verification of modern-day processors is a non-trivial exercise, and RISC-V® is no exception. In this article, we present a formal verification methodology for verifying a family of RISC-V® “low-power” processors. Our methodology is both new and unique in the way we address the challenges of verification going beyond just functional verification. We focus on architectural verification, lockstep verification (part of functional safety), X-issues due to low-power design, and security. Our approach finds bugs in previously verified and taped-out cores as well as establish bug absence through exhaustive proofs of correctness for end-to-end checks.
At Axiomise, we have designed a new RISC-V® ISA Formal Proof Kit® covering the RV32IC subset
...
