Name
Title | ||
|---|---|---|
Microprocessor Verification Using Efficient Decision Procedures for a Logic of Equality with Uninterpreted Functions |
Abstract | ||
|---|---|---|
Modern processors have relatively simple specifications based on their instruction set architectures. Their implementations, however, are very complex, especially with the advent of performance-enhancing techniques such as pipelining, superscalar operation, and speculative execution. Formal techniques to verify that a processor implements its instruction set specification could yield more reliable results at a lower cost than the current simulation-based verification techniques used in industry. The logic of equality with uninterpreted functions (EUF) provides a means of abstracting the manipulation of data by a processor when verifying the correctness of its control logic. Using a method devised by Burch and Dill [BD94], the correctness of a processor can be inferred by deciding the validity of a formula in EUF describing the comparative effect of running one clock cycle of processor operation to that of executing a small number (based on the processor issue rate) of machine instructions. This paper describes recent advances in reducing formulas in EUF to propositional logic. We can then use either Binary Decision Diagrams (BDDs) or satisfiability procedures to determine whether this propositional formula is a tautology. We can exploit characteristics of the formulas generated when modeling processors to significantly reduce the number of propositional variables, and consequently the complexity, of the verification task. |
Year | DOI | Venue |
|---|---|---|
1999 | 10.1007/3-540-48754-9_1 | TABLEAUX |
Keywords | Field | DocType |
machine instruction,instruction set architecture,propositional variable,microprocessor verification,control logic,modern processor,efficient decision procedures,propositional formula,current simulation-based verification technique,uninterpreted functions,processor issue rate,instruction set specification,processor operation,speculative execution,binary decision diagram | Programming language,Computer science,Satisfiability,Correctness,Binary decision diagram,Algorithm,Propositional calculus,Cycles per instruction,Propositional formula,Propositional variable,Distributed computing,Formal verification | Conference |
ISBN | Citations | PageRank |
3-540-66086-0 | 1 | 0.39 |
References | Authors | |
12 | 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 |