Loading...
Please wait, while we are loading the content...
Similar Documents
EVC: A Validity Checker for the Logic of Equality with Uninterpreted Functions and Memories, Exploiting Positive Equality, and Conservative Transformations (2001)
| Content Provider | CiteSeerX |
|---|---|
| Author | Bryant, Randal E. Velev, Miroslav N. |
| Abstract | The property of Positive Equality [2] dramatically speeds up validity checking of formulas in the logic of Equality with Uninterpreted Functions and Memories (EUFM) [4]. The logic expresses correctness of high-level microproces-sors. We present EVC (Equality Validity Checker)—a tool that exploits Positive Equality and other optimizations when translating a formula in EUFM to a proposi-tional formula, which can then be evaluated by any Boolean satisfiability (SAT) procedure. EVC has been used for the automatic formal verification of pipelined, superscalar, and VLIW microprocessors. |
| File Format | |
| Publisher Date | 2001-01-01 |
| Access Restriction | Open |
| Subject Keyword | Present Evc High-level Microproces-sors Automatic Formal Verification Equality Validity Checker Uninterpreted Function Validity Checker Boolean Satisfiability Proposi-tional Formula Validity Checking Positive Equality Vliw Microprocessor |
| Content Type | Text |