Formal verification of pipelined microprocessors with delayed branches

Presented is an approach for formal verification of pipelined microprocessors with delayed branches, i.e., branch instructions whose immediately following instruction is always executed regardless of whether the branch is taken. Delayed branches are used in the instruction sets of the MIPS, SPARC, and PA-RISC architectures. Because of their sequential semantics that spans several consecutive instruction slots, delayed branches complicate the checking of safety and liveness for pipelined designs. The presented approach is highly automatic compared to previous methods for formal verification of pipelined processors with delayed branches