Automatic generation of assertions for formal verification of PowerPC microprocessor arrays using symbolic trajectory evaluation
Li-C. Wang, Magdy S. Abadir, Nari Krishnamurthy · 1998
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 the 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.