Formal verification of the UltraSPARC(TM) family of techniques

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 UltraSPARC^(TM)-I and UltraSPARC^(TM)-II microprocessors. The 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