Sciweavers

Share
FMSD
2002

Verification of Out-Of-Order Processor Designs Using Model Checking and a Light-Weight Completion Function

10 years 4 months ago
Verification of Out-Of-Order Processor Designs Using Model Checking and a Light-Weight Completion Function
We present a new technique for verification of complex hardware devices that allows both generality andahighdegreeofautomation.Thetechniqueisbasedonournewwayofconstructinga"light-weight"completion function together with new encoding of uninterpreted functions called reference file representation. Our technique combines our completion function method and reference file representation with compositional model checking and theorem proving. This extends the state of the art in two directions. First, we obtain a more general verification methodology. Second, it is easier to use, since it has a higher degree of automation. As a benchmark, we take Tomasulo's algorithm for scheduling out-of-order instruction execution used in many modern superscalar processors like the Pentium-II and the PowerPC 604. The algorithm is parameterized by the processor configuration, and our approach allows us to prove its correctness in general, independent of any actual design.
Sergey Berezin, Edmund M. Clarke, Armin Biere, Yun
Added 19 Dec 2010
Updated 19 Dec 2010
Type Journal
Year 2002
Where FMSD
Authors Sergey Berezin, Edmund M. Clarke, Armin Biere, Yunshan Zhu
Comments (0)
books