Formal verification of the UltraSPARC/sup (TM)/ family of techniques

Description

This item was taken from the IEEE Periodical ' Formal verification of the UltraSPARC/sup (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/sup (TM)/-I and UltraSPARC/sup (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.