|
Verification of a pipeline processor from the instruction set architecture (ISA)| old_uid | 7598 |
|---|
| title | Verification of a pipeline processor from the instruction set architecture (ISA) |
|---|
| start_date | 2009/11/13 |
|---|
| schedule | 15h-15h30 |
|---|
| online | no |
|---|
| location_info | couloir 55-65, salle 211 |
|---|
| summary | Verification is a critical and costly step in the design of processors. For high quality results, the verification should be based on formal techniques like model checking. But, this requires a significant manual effort for setting up a good property suite that covers all possible bugs. Furthermore, a high level of expertise is needed in contrast to traditional simulation based methods. In the past, several methods have been proposed to raise the degree of automation in the verification of processors. While some approaches focus on incremental design and verification, others concentrate on the automated checking of specific features of a processor such as out-of-order execution or the forwarding control logic of the pipeline.
In this talk, an approach will be presented for the complete verification of processors based on architectural models. There, the textual specification is transformed to a formal architecture description that captures the instruction set architecture (ISA). The user then needs to specify how the ISA is mapped to the register transfer level (RTL) implementation. This is done by implementing a number of predefined predicates and functions that describe the generic concepts of a correct pipelined processor. Using this information, a property suite is generated that is complete by construction, i.e. no bugs can be missed. The properties are checked on the design automatically using a commercial model checking tool. By using the proposed technique, the productivity of the verification can be increased significantly when compared to a manual approach.
The use of architectural models in the formal verification suggests further applications such as the automatic generation of instruction set simulators (ISSs) or the automatic synthesis of embedded software. A short overview on these supplementary techniques will also be given in the talk. |
|---|
| responsibles | Baerecke |
|---|
| |
|