# A Framework for Verifying Bit-Level Pipelined Machines Based on Automated Deduction and Decision Procedures

Panagiotis Manolios and Sudarshan K. Srinivasan.

*Journal of Automated Reasoning*, to appear. © Springer Verlag

# Abstract

We describe an approach to verifying bit-level pipelined machine
models using a combination of deductive reasoning and decision
procedures. While theorem proving systems such as ACL2 have been
used to verify bit-level designs, they typically require
extensive expert user support. Decision procedures such as those
implemented in UCLID can be used to automatically and efficiently
verify term-level pipelined machine models, but these models use
numerous abstractions, implement a subset of the instruction set,
and are far from executable. We show that by integrating UCLID
with the ACL2 theorem proving system, we can use ACL2 to reduce
the proof that an executable, bit-level machine refines its
instruction set architecture to a proof that a term-level
abstraction of the bit-level machine refines the instruction set
architecture, which is then handled automatically by UCLID. We
demonstrate the efficiency of our approach by applying it to
verify a complex seven stage bit-level interface pipelined
machine model that implements 593 instructions and has features
such as branch prediction, exceptions, and predicated instruction
execution. Such a proof is not possible using UCLID and would
require prohibitively more effort using just ACL2.

PDF (170K) © Springer Verlag