posted on 1996-01-01, 00:00authored byRandal E. Bryant, Shuvendru K Lahiri, Sanjit A Seshia
In this paper, we present the logic of Counter Arithmetic
with Lambda Expressions and Uninterpreted Functions (CLU). CLU
generalizes the logic of equality with uninterpreted functions (EUF) with
constrained lambda expressions, ordering, and successor and predecessor
functions. In addition to modeling pipelined processors that EUF has
proved useful for, CLU can be used to model many infinite-state systems
including those with infinite memories, finite and infinite queues
including lossy channels, and networks of identical processes. Even with
this richer expressive power, the validity of a CLU formula can be efficiently
decided by translating it to a propositional formula, and then
using Boolean methods to check validity. We give theoretical and empirical
evidence for the efficiency of our decision procedure. We also describe
verification techniques that we have used on a variety of systems, including
an out-of-order execution unit and the load-store unit of an industrial
microprocessor.