Loading...
Please wait, while we are loading the content...
Similar Documents
Proving the Correctness of a Complete Microprocessor (2000)
| Content Provider | CiteSeerX |
|---|---|
| Author | Jacobi, Christian Kroening, Daniel |
| Description | . This paper presents status results of a microprocessor verification project. The authors verify a complete 32-bit RISC microprocessor including the floating point unit and the control logic of the pipeline. The paper describes a formal definition of a "correct" microprocessor. This correctness criterion is proven for an implementation using formal methods. All proofs are verified mechanically by means of the theorem proving system PVS. 1 Introduction Microprocessor design is an error-prone process. With increasing complexity of current microprocessor designs, formal verification has become crucial. In order to achieve completely verified designs, adjusting the design process itself plays an important role: the more high-level information on the design is available, the faster the verification can be done. The authors re-designed a simple RISC processor, the DLX [1], with respect to verifiability. The design includes the complete pipe control and forwarding logic. The function... |
| File Format | |
| Language | English |
| Publisher | Springer |
| Publisher Date | 2000-01-01 |
| Publisher Institution | In GI Jahrestagung 2000 |
| Access Restriction | Open |
| Subject Keyword | Control Logic Important Role Complete Microprocessor Complete Pipe Control High-level Information Point Unit Formal Verification Design Process Correct Microprocessor Status Result Current Microprocessor Design Verified Design Formal Method Error-prone Process Simple Risc Processor Correctness Criterion Complete 32-bit Risc Microprocessor System Pvs Formal Definition Microprocessor Verification Project Introduction Microprocessor Design |
| Content Type | Text |
| Resource Type | Article |
