Automatic Formal Verification of RISC-V Pipelined Microprocessors with Fault Tolerance by Spatial Redundancy at a High Level of Abstraction

Presented are abstraction techniques for efficient modeling of pipelined microprocessors of the RISC-V architecture, including designs with fault tolerance by spatial redundancy. This is done at a high-level of abstraction, allowing us to formally verify such processors extremely efficiently by using the property of Positive Equality. To the best of our knowledge, this is the first work on formal verification of RISC-V pipelined processors at a high level of abstraction, and the first work on formal verification of pipelined microprocessors with fault tolerance by spatial redundancy.