Loading...
Please wait, while we are loading the content...
Similar Documents
Modeling and Verification of Out-of-Order Microprocessors in UCLID (2002)
| Content Provider | CiteSeerX |
|---|---|
| Author | Lahiri, Shuvendu K. Seshia, Sanjit A. Bryant, Randal E. |
| Description | In this paper, we describe the modeling and verification of out-of-order microprocessors with unbounded resources using an expressive, yet efficiently decidable, quantifier-free fragment of first order logic. This logic includes uninterpreted functions, equality, ordering, constrained lambda expressions, and counter arithmetic. UCLID is a tool for specifying and verifying systems expressed in this logic. The paper makes two main contributions. First, we show that the logic is expressive enough to model components found in most modern microprocessors, independent of their actual sizes. Second, we demonstrate UCLID's verification capabilities, ranging from full automation for bounded property checking to a high degree of automation in proving restricted classes of invariants. These techniques, coupled with a counterexample generation facility, are useful in establishing correctness of processor designs. We demonstrate UCLID's methods using a case study of a synthetic model of an out-of-order processor where all the invariants were proved automatically. |
| File Format | |
| Language | English |
| Publisher | Springer-Verlag |
| Publisher Date | 2002-01-01 |
| Publisher Institution | FORMAL METHODS IN COMPUTER-AIDED DESIGN (FMCAD ’02), LNCS 2517 |
| Access Restriction | Open |
| Subject Keyword | Main Contribution Bounded Property Checking Out-of-order Processor Counterexample Generation Facility Actual Size Uninterpreted Function Out-of-order Microprocessor Full Automation Verification Capability High Degree Modern Microprocessor Quantifier-free Fragment Restricted Class First Order Logic Processor Design Synthetic Model Lambda Expression Unbounded Resource Case Study |
| Content Type | Text |
| Resource Type | Article |
