Modeling and Verification of Out-of-Order Microprocessors in UCLID
- 5 November 2002
- book chapter
- Published by Springer Nature
- p. 142-159
- https://doi.org/10.1007/3-540-36126-x_9
Abstract
No abstract availableKeywords
This publication has 18 references indexed in Scilit:
- Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted FunctionsPublished by Springer Nature ,2002
- Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logicACM Transactions on Computational Logic, 2001
- A Comparison of Two Verification Methods for Speculative Instruction ExecutionPublished by Springer Nature ,2000
- Proof of Correctness of a Processor with Reorder Buffer Using the Completion Functions ApproachPublished by Springer Nature ,1999
- Exploiting Positive Equality in a Logic of Equality with Uninterpreted FunctionsPublished by Springer Nature ,1999
- Verifying Tomasulo's algorithm by refinementPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1999
- Combining Symbolic Model Checking with Uninterpreted Functions for Out-of-Order Processor VerificationPublished by Springer Nature ,1998
- Validity checking for combinations of theories with equalityPublished by Springer Nature ,1996
- Automatic verification of pipelined microprocessor controlPublished by Springer Nature ,1994
- The decision problem for standard classesThe Journal of Symbolic Logic, 1976