Validation of PowerPCTM custom memories using symbolic simulation

This paper describes the use of Symbolic Trajectory Evaluation (STE), a modified form of symbolic simulation, to verify the equivalence between RTL and transistor-level representations of on-chip custom memories for the latest PowerPC microprocessor. The validation of embedded memories and their associated control logic poses a special problem for traditional formal equivalence checking tools due to the inherently sequential and self-timed nature of the internal control logic and the large number of state-holding elements. The use of the VERSYS STE engine to validate these custom memories is illustrated. We present our array verification methodology, discuss some of the results of our approach, and outline plans for future development