Automatic generation of assertions for formal verification of PowerPC™ microprocessor arrays using symbolic trajectory evaluation

For verifying complex sequential blocks such as microprocessor embedded arrays, the formal method of symbolic trajectory evaluation (STE) has achieved great success in the past [[3], [5], [6]]. Past STE methodology for arrays requires manual creation of "assertions" to which both RTL view and the actual design should be equivalent. In this paper, we describe a novel method to automate the assertion creation process which improves the efficiency and the quality of array verification. Encouraging results on recent PowerPC arrays will be presented.