Abstract
This paper proposes a methodology based on formal correspondence checking to automatically debug and also optimize pipelined microprocessors including reconfigurable processors with timing error recovery techniques. Since formal verification analyzes the design exhaustively, it may give good insights into not only debugging but also optimization of hardware designs with complicated control structures. The paper gives two main contributions, 1) modeling and formal verification of pipelined microprocessors including reconfigurable processors with timing error recovery techniques and 2) an approach to debug and optimize the implementation using the UCLID system as a correspondence checker. Using our method, the debug time can be reduced significantly. In addition, the implementation can be optimized by removing unnecessary signals and components while the correctness of the design is guaranteed.
