# Verification of Executable Pipelined Machines with Bit-Level Interfaces

Panagiotis Manolios and Sudarshan K. Srinivasan.

*ICCAD 2005, International Conference on Computer Aided Design*. © IEEE

# Abstract

We show how to verify pipelined machine models with bit-level
interfaces by using a combination of deductive reasoning and
decision procedures. While decision procedures such as those
implemented in UCLID can be used to verify pipelined machines,
the models are at the *term level*: they abstract away the
datapath, require the use of numerous abstractions, implement a
small subset of the instruction set, and are far from
executable. In contrast, we focus on verifying executable
machines with bit-level interfaces. Such proofs have
previously required substantial expert guidance and the use of
deductive reasoning engines. 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. In this way, we exploit the strengths of ACL2 and UCLID
to prove theorems that are not possible to even state using
UCLID and that would require prohibitively more effort using
just ACL2.

PDF (131K) © IEEE