# Automatic Verification of Safety and Liveness for XScale-Like Processor Models Using WEB-Refinements

Panagiotis Manolios and Sudarshan K. Srinivasan.

*CERCS TR# GIT-CERCS-03-17*.

# Abstract

We show how to automatically verify that a complex XScale-like
pipelined machine model is a WEB-refinement of an instruction set
architecture model, which implies that the machines satisfy the
same safety and liveness properties. 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 UCLID to transform the
resulting CLU formula into a CNF formula, which is then checked
with a SAT solver. We define several XScale-like models with out
of order completion, including models with 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 SAT
solver Siege
provides superior performance over Chaff and that
the amount of time spent proving liveness when using the
commitment approach is less than 1% of the overall verification
time, whereas when flushing is employed, the liveness proof
accounts for about 10% of the verification time.

Gzipped Postscript (56K)

PDF (57K)

Postscript (185K)