Formal verification of the UltraSPARC(TM) family of processors via ATPG methods

This paper describes a novel and important use of a commercial Automatic Test Pattern Generation (ATPG) tool to perform formal verification during the design of the UltraS-PARC(TM)-I UltraS-PARC(TM)-II microprocessors. The and verification problem addressed in this paper is that of required signal constraints amongst a group of signals to ensure correct multiplexor operation. We do not address the equivalence between two representations of a design which is the more common problem in literature. The technique developed was a significant contributor to the overall success of the project. The problem addressed, solution formulation, software developed, and results are presented.