PolyMiR: Polynomial Formal Verification of the MicroRV32 Processor
Lennart Weingarten, Kamalika Datta, Rolf Drechsler · 2023
Formal verification techniques ensure completeness as opposed to simulation-based techniques. In general, the process of formal verification is computationally complex, and it is difficult to quantify the exact time and space complexities. Some of the recent works have shown that it is possible to achieve polynomial space and time complexities for verifying specific designs, like arithmetic circuits. However, this cannot be directly extended to complex circuits, like processors. A recent work has reported a formal verification method for the RISC-V processor with polynomial complexity, where only single-cycle instruction execution was considered and it was computation intensive. This method cannot be directly extended to multi-cycle operations, which are typical for most real processors. This paper introduces an improved data structure leading to Binary Decision Diagram (BDD) based Polynomial Formal Verification (PFV) with support for both single-cycle and multi-cycle operations. We use the MicroRV32 processor as a case study. Our method leads to significant improvement in runtime over the previous method. The entire process of verification can be carried out in polynomial space and time complexities for multi-cycle operations.