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


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"
}