Carnegie Mellon University
Browse

Formal Verification of PowerPC(TM) Arrays using Symbolic Trajectory Evaluation

journal contribution
posted on 1996-01-01, 00:00 authored by Manish Pandey, Richard Raimi, Derek L. Beatty, Randal BryantRandal Bryant

Verifying memory arrays such as on-chip caches and register

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.

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.

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.

History

Publisher Statement

All Rights Reserved

Date

1996-01-01

Usage metrics

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC