Sciweavers

Share
AMAI
2004
Springer

Using Automatic Case Splits and Efficient CNF Translation to Guide a SAT-solver when Formally Verifying Out-Of-Order Processors

10 years 1 months ago
Using Automatic Case Splits and Efficient CNF Translation to Guide a SAT-solver when Formally Verifying Out-Of-Order Processors
The paper integrates automatically generated case-splitting expressions, and an efficient translation to CNF, in order to formally verify an out-of-order superscalar processor having register renaming, as well as Reorder Buffer and Reservation Stations that are completely implemented and instantiated. The processor was defined in the high-level Hardware Description Language AbsHDL, based on the logic of Equality with Uninterpreted Functions and Memories (EUFM), and was formally verified with an extended version of the decision procedure EVC, combined with a SAT-solver. The manual work was limited to definition of necessary invariant constraints. The formal verification was decomposed, based on automatically generated case-splitting expressions—matching Recorder Buffer entries with Reservation Stations to compute the results for those Reorder Buffer entries, and allowing for orders of magnitude speedup if many CPUs are available for parallel runs of EVC. Efficient translation from EUF...
Miroslav N. Velev
Added 30 Jun 2010
Updated 30 Jun 2010
Type Conference
Year 2004
Where AMAI
Authors Miroslav N. Velev
Comments (0)
books