Putting it all together – Formal verification of the VAMP |
| |
Authors: | Sven Beyer Christian Jacobi Daniel Kröning Dirk Leinenbach Wolfgang J. Paul |
| |
Affiliation: | 1. OneSpin Solutions GmbH, 80339, Munich, Germany 3. IBM Deutschland Entwicklung GmbH, 71032, B?blingen, Germany 4. ETH Zürich, Computer Systems Institute, Zürich, Switzerland 2. Computer Science Department, Saarland University, 66123, Saarbrücken, Germany
|
| |
Abstract: | In the verified architecture microprocessor (VAMP) project we have designed, functionally verified, and synthesized a processor with full DLX instruction set, delayed branch, Tomasulo scheduler, maskable nested precise interrupts, pipelined fully IEEE compatible dual precision floating point unit with variable latency, and separate instruction and data caches. The verification has been carried out in the theorem proving system PVS. The processor has been implemented on a Xilinx FPGA. A shorter version of this article with the title “Instantiating uninterpreted functional units and memory system: functional verification of the VAMP” appeared in [8]. The work reported here was done while all the authors were with Saarland University. |
| |
Keywords: | Formal methods Complete microprocessor verification Floating point unit Tomasulo scheduler Cache memory interface Theorem proving Model checking |
本文献已被 SpringerLink 等数据库收录! |
|