Formal verification of PowerPC arrays using symbolic trajectory evaluation

Verifying memory arrays such as on-chip caches and register files is a difficult part of designing a microprocessor. Current tools cannot verify the equivalence of the arrays to their behavioral or RTL models, nor their correct functioning at the transistor level. It is infeasible to run the number of simulation cycles required, and most formal verification tools break down due to the enormous number of state-holding elements in the arrays. The formal method of symbolic trajectory evaluation (STE) appears to offer a solution, however. STE verifies that a circuit satisfies a formula in a carefully restricted temporal logic. For arrays, it requires only a number of variables approximately logarithmic in the number of memory locations. The circuit is modeled at the switch level, so the verification is done on the actual design. We have used STE to verify two arrays from PowerPC microprocessors: a register file, and a data cache tag unit. The tag unit contains over 12,000 latches. We believe it is the largest circuit to have been formally verified, without abstracting away significant detail, in the industry. We also describe an automated technique for identifying state-holding elements in the arrays, a technique which should greatly assist the widespread application of STE