Combining Stream-based and State-based Verification Techniques for Microarchitectures

Nancy A. Day, Mark D. Aagaard, and Byron Cook

In Formal Methods in Computer-Aided Design, 2000.

Abstract
Paper (gzipped postscript)
Bibtex entry


Abstract

Algebraic verification techniques manipulate the structure of a circuit while preserving its behavior. Algorithmic verification techniques verify properties about the behavior of a circuit. These two techniques have complementary strengths: algebraic techniques are largely independent of the size of the state space, and algorithmic techniques are highly automated. It is desirable to exploit both in the same verification. However, algebraic techniques often use stream-based models of circuits, while algorithmic techniques use state-based models. We prove the consistency of stream- and state-based interpretations of circuit models, and show how stream-based verification results can be used hand-in-hand with state-based verification results. Our approach allows us to combine stream-based algebraic rewriting and state-based reasoning, using SMV and SVC, to verify a pipelined microarchitecture with speculative execution.

Bibtex Entry

@INPROCEEDINGS{DaAoCo00,
  title={Combining Stream-based and State-based Verification Techniques for Microarchitectures},
  author ={Nancy A. Day and Mark D. Aagaard and Byron Cook},
  booktitle={Formal Methods in Computer-Aided Design},
  series={Lecture Notes in Computer Science},
  volume=1954,
  publisher={Springer}
  editors ={Warren A. Hunt, Jr. and Steven D. Johnson},
  month={November},
  year = 2000,
  pages ={126-142}
}                                                        

Send questions or comments to Mark Aagaard < markaa@swen.uwaterloo.ca >