FEST - Funktionale Verifikation von Systemen
| project staff | project description | project target | project structure
|
| Computer Architecture and Operating Systems | |
| Bernd Becker, Prof. Dr. | |
| Christoph Scholl, Prof. Dr. | |
| Frank Schmiedle, Dr.-Ing. | |
| Florian Pigorsch, Dipl.-Inf. | |
FEST is a project started within the scope of the support programme Ekompass, which ist supported by the Bundesministerium für Bildung und Forschung (BMBF) and the edacentrum GmbH. Besides the Albert-Ludwigs-Universität Freiburg, further project partners are the TU Darmstadt, Universität Frankfurt/Main, TU Ilmenau, Universität Kaiserslautern and Universität Tübingen. In the context of this project, we strive for solutions to provide the possibility for unique verification of SoCs (System On Chip). The know-how that is obtained by research will help Germany\'s semiconductor industry to keep the expertise of their design teams on the top level. Furthermore, new powerful methods will be provided and incorperated in industrial design plattforms. The contribution of the Freiburg work group mainly consists of the investigation and development of novel and successful approaches for black box model checking.
Further information can be found at the [ecacentrum Homepage].
There is an ongoing competition between design methodology on the one and improvement in semiconductor technology on the other side. To ensure progress, EDA innovations are essential to improve design productivity as much as necessary to follow the raise of technology quality. To the appropriate steps in order to achieve this goal, the Bundesministerium für Bildung und Forschung started the support programme Ekompass.
At present, commercial EDA tools do not meet the needs with respect to methods for formal verification. Hence, there is a design gap that has to be closed. Due to the complexity of today's designs, it is essential to replace the simulation based methods that are still widely used as main instrument for verification by formal verification techniques. Otherwise, it can not be ensured that semiconductor products like SoCs do not include any design errors.
In recent years, several promising verification methods have been reported. On the other hand, a methodical overall approach comprising verification from the system level down to the electrical level is still missing. This problem
is attacked by the project
Funktionale Verifikation von Systemen (FEST).
The six project partners develop new verification methods at different levels in order to integrate all of them them in one overall system. The network of different universities and the associated transfer of research knowledge is a basic requirement for the successful development of homogeneous verification tools of high quality that span several different levels of abstraction.
At the system level, methods for modelling time properties are investigated. By these techniques, the behavior of the whole system can be verified before implementation starts. Additionally, one focus of the project is to explore a unique HW-/SW-verification approach that allows to handle hardware and software components at the same time. This is an important task as well at the system level as at the architecture level. Furthermore, for the latter some improved model checking approaches are developed. Black/grey box techniques are utilized here to localize errors and generate counterexamples. Finally, the efficiency of verification methods for digital blocks is increased significantly, and development of a tool for mixed-signal model checking leads to further improvements of verification on very low levels of abstraction.
At the different levels of abstraction, there is a need for appropriate modeling to establish a basis for the verification methods that are about to be developed. According to this, the project is divided into
two work packages:
- modeling and abstraction
- methods and integration
Both packages include several tasks. For the first package modeling and abstraction these are:
- unique semantics for hardware and software
systems and extraction of properties
- models for mixed-signal-verification
- time properties and restrictions in models
- abstract models at the architecture level
- generation of models for block verification
The tasks of the university of Freiburg belong to the area methods and integration which is structured as follows:
- verifikation und analysis
- refinement of time restrictions
- transformation of time-evaluated models
- compositional verifikation at the architecture level
- algorithmens for verifikation of mixed-signal-systems
- black box techniques for model checking
Since the group of the university of Freiburg is responsible for the latter task, it strives for providing powerful black box techniques for model checking. Doing so, we consider two different points of view:
- black box techniques for counterexamples
- error localization for model checking