10.1184/R1/6622301.v1
Manish Pandey
Manish
Pandey
Richard Raimi
Richard
Raimi
Derek L. Beatty
Derek L.
Beatty
Randal Bryant
Randal
Bryant
Formal Verification of PowerPC(TM) Arrays using Symbolic Trajectory Evaluation
Carnegie Mellon University
1996
Software Research
1996-01-01 00:00:00
Journal contribution
https://kilthub.cmu.edu/articles/journal_contribution/Formal_Verification_of_PowerPC_TM_Arrays_using_Symbolic_Trajectory_Evaluation/6622301
<p>Verifying memory arrays such as on-chip caches and register
</p><p> files is a difficult part of designing a microprocessor. Current toolscannot 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 breakdowndue to the enormous number of state-holding elements in the arrays.
</p><p>
</p><p>
</p><p>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 logarithmicin the numberof memory locations. The circuit is modeled at the switch level, so the verification is done on the actual design.</p>
<p></p>
<p>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</p>
<p></p>
<p></p>
<p></p>
<p>
</p><p>which should greatly assist the widespread application of STE.</p>
<p></p>