# Deductive Verification of Pipelined Machines Using First-order
Quantification

S. Ray and W. A. Hunt, Jr.

In R. Alur and D. A. Peled, editors,
Proceedings of the 16th
International Conference on Computer-aided Verification (CAV
2004), Boston, MA, July 2004, volume 3114 of LNCS, pages
31-43. Springer.

© Springer-Verlag
Berlin Heidelberg 2004.

## Abstract

We outline a theorem-proving approach to verify pipelined machines.
Pipelined machines are complicated to reason about since they involve
simultaneous overlapped execution of different instructions.
Nevertheless, we show that if the logic used is sufficiently
expressive, then it is possible to relate the executions of the
pipelined machine with the corresponding Instruction Set Architecture
using (stuttering) simulation correspondence. Our methodology uses
first-order quantification to define a predicate that relates pipeline
states with ISA states and uses its Skolem witness for correspondence proofs. Our
methodology can be used to reason about generic pipelines with interrupts, stalls, and
exceptions, and we demonstrate its use in verifying pipelines
mechanically in the ACL2 theorem prover.
## Relevant files

- Paper (ps, pdf)
- Slides for CAV 2004 (ps, pdf)
- Supporting ACL2 proof scripts (tar.gz)

## BibTex

@Inproceedings{ray-deductive,
author = "S. Ray and Hunt, Jr., W. A.",
title = "{Deductive Verification of Pipelined Machines Using First-Order Quantification}",
booktitle = "{Proceedings of the $16$th International Conference on Computer-Aided Verification (CAV 2004)}",
editor = "R. Alur and D. A. Peled",
address = "{Boston, MA}",
month = jul,
year = "2004",
series = "LNCS",
volume = "3114",
pages = "31-43",
publisher = "Springer"
}