Loading...
Please wait, while we are loading the content...
Similar Documents
Efficient validity checking for processor verification (1995).
| Content Provider | CiteSeerX |
|---|---|
| Author | Jones, Robert Dill, David L. Burch, Jerry R. |
| Abstract | We describe an efficient validity checker for the quantifier-free logic of equality with uninterpreted functions. This logic is well suited for verifying microprocessorcontrol circuitry since it allows the abstraction of datapath values and operations. Our validity checker uses special data structures to speed up case splitting, and powerful heuristics to reduce the number of case splits needed. In addition, we present experimental results and show that this implementation has enabled the automatic verification of an actual high-level microprocessor description. 1 Introduction As microprocessor designs become more complex, the cost of validation becomes a larger fraction of the total design cost. Currently, validation consumes 25-30% of the design team and months of simulation time. Industry experts predict that there may soon be two or three validation engineers for every design engineer on major microprocessor design projects [Wil95]. Although today's theorem provers could be used,... |
| File Format | |
| Publisher Date | 1995-01-01 |
| Access Restriction | Open |
| Subject Keyword | Efficient Validity Checking Processor Verification Design Engineer Validity Checker Case Splitting Major Microprocessor Design Project Quantifier-free Logic Validation Consumes Uninterpreted Function Efficient Validity Checker Powerful Heuristic Design Team Simulation Time Validation Engineer Microprocessorcontrol Circuitry Special Data Structure Automatic Verification Actual High-level Microprocessor Description Datapath Value Case Split Theorem Provers Total Design Cost Experimental Result Industry Expert |
| Content Type | Text |
