Name
Abstract | ||
|---|---|---|
In using the logic of equality with unininterpreted functions to verify hardware systems, specific characteristics of the formula describing the correctness condition can be exploited when deciding its validity.We distinguish a class of terms we call "p-terms" for which equality comparisons can appear only in monotonically positive formulas. By applying suitable abstractions to the hardware model, we can express the functionality of data values and instruction addresses flowing through an instruction pipeline with p-terms. Adecision procedure can exploit the restricted uses of p-terms by considering only "maximally diverse" interpretations of the associated function symbols, where every function application yields a different value except when constrained by functional consistency.We present a procedure that translates the original formula into one in propositional logic by interpreting the formula over a domain of fixedlength bit vectors and using vectors of propositional variables to encode domain variables. By exploiting maximal diversity, this procedure can greatly reduce the number of propositional variables that must be introduced. We present experimental results demonstrating the efficiency of this approach when verifying pipelined processors using the method proposed by Burch and Dill. Exploiting positive equality allows us to overcome the exponential blowup experienced previously [VB98] when verifying microprocessors with load, store, and branch instructions. |
Year | DOI | Venue |
|---|---|---|
1999 | 10.1007/3-540-48683-6_40 | ACM Transactions on Computational Logic |
Keywords | Field | DocType |
positive equality,original formula,monotonically positive formula,propositional variable,branch instruction,associated function symbol,adecision procedure,propositional logic,domain variable,uninterpreted functions,equality comparison,exploiting positive equality | Computer science,Correctness,Theoretical computer science,Distributed computing,Discrete mathematics,Uclid,Monotonic function,Algorithm,Propositional calculus,Formal specification,Function application,Propositional variable,Formal verification | Conference |
ISBN | Citations | PageRank |
3-540-66202-2 | 56 | 5.12 |
References | Authors | |
9 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Randal E. Bryant | 1 | 9204 | 1194.64 |
| Steven M. German | 2 | 596 | 106.83 |
| Miroslav N. Velev | 3 | 953 | 60.17 |