Name
Abstract | ||
|---|---|---|
The correctness of processors is a key for their application. Although some verification methods were developed and successfully applied to conventional microprocessors, only a few of them were used in context of application specific devices. This work introduces a formal verification approach for a reconfigurable microprocessor with extendable instruction set. The application of this approach is demonstrated using register transfer description of the CoMPARE processor and the Stanford Validity Checker as prover. Some undesired the verification process found side effects of different instructions that were not discovered during the simulation. In addition, some deficiencies of the hardware description notation as specification formalism were shown. |
Year | DOI | Venue |
|---|---|---|
2000 | 10.1109/ASAP.2000.862377 | ASAP |
Keywords | Field | DocType |
stanford validity checker,application specific device,formal verification approach,different instruction,conventional microprocessors,verification process,extendable instruction set,compare processor,verification method,hardware description notation,formal verification,register transfer description,registers,hardware description languages,application software,arithmetic,instruction sets,prototypes,field programmable gate arrays,side effect | Instruction set,Intelligent verification,Computer science,Parallel computing,Correctness,Verification,Application software,High-level verification,Formal verification,Embedded system,Hardware description language | Conference |
ISSN | ISBN | Citations |
1063-6862 | 0-7695-0716-6 | 1 |
PageRank | References | Authors |
0.40 | 10 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Sergej Sawitzki | 1 | 15 | 4.79 |
| Rainer G. Spallek | 2 | 137 | 25.30 |
| Jens Schönherr | 3 | 8 | 5.40 |
| Bernd Straube | 4 | 195 | 37.41 |