|
CMU-CS-98-124
Computer Science Department
School of Computer Science, Carnegie Mellon University
CMU-CS-98-124
Combining Symbolic Model Checking with
Uninterpreted Functions for Out-of-Order Processor Verification
Sergey Berezin, Armin Biere, Edmund Clarke, Yunshan Zhu
April 1998
[Submitted to FMCAD'98]
CMU-CS-98-124.ps
We present a new approach to the verification of hardware systems with
data dependencies using temporal logic symbolic model checking. As a
benchmark we take Tomasulo's algorithm for out-of-order instruction
scheduling. Our approach is similar to the idea of uninterpreted
function symbols. We use symbolic values and instructions instead of
concrete ones. This allows us to show the correctness of the machine
independently of the actual instruction set architecture and the
implementation of the functional units. Instead of using first order
terms, we represent symbolic values with a new compact encoding. In
addition, we apply some other reduction techniques to the model. This
significantly reduces the state space and allows the use of highly
efficient symbolic model checkers like SMV instead of special decision
procedures. The correctness of the method has been proven formally
with the PVS theorem prover.
Keywords: Out-of-order execution, automatic verification, temporal
logic, symbolic checking, theorem proving
22 pages
|