|
Published Articles >> Table of Contents >> Abstract
Design, Automation and Test in Europe Conference and Exhibition Volume I (DATE'04)
p. 10168
Automatic Verification of Safety and Liveness for XScale-Like Processor Models Using WEB Refinements
Panagiotis Manolios, Georgia Institute of Technology
Sudarshan K. Srinivasan, Georgia Institute of Technology
Full Article Text:
  
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/DATE.2004.1268844
Send link to a friend
| Abstract |
|
We show how to automatically verify that complex XScale-like pipelined machine models satisfy the same safety and liveness properties as their corresponding instruction set architecture models, by using the notion of Well-founded Equivalence Bisimulation (WEB) refinement. Automation is achieved by reducing the WEB-refinement proof obligation to a formula in the logic of Counter arithmetic with Lambda expressions and Uninterpreted functions (CLU). We use the tool UCLID to transform the resulting CLU formula into a Boolean formula, which is then checked with a SAT solver. The models we verify include features such as out of order completion, precise exceptions, branch prediction, and interrupts. We use two types of refinement maps. In one, flushing is used to map pipelined machine states to instruction set architecture states; in the other, we use the commitment approach, which is the dual of flushing, since partially completed instructions are invalidated. We present experimental results for all the machines modeled, including verification times. For our application, we found that the time spent proving liveness accounts for about 5% of the overall veri.cation time.
|
 Additional Information
|
Citation:
Panagiotis Manolios, Sudarshan K. Srinivasan,
"Automatic Verification of Safety and Liveness for XScale-Like Processor Models Using WEB Refinements,"
date,
p. 10168,
Design, Automation and Test in Europe Conference and Exhibition Volume I (DATE'04),
2004
|
|
