Automatisierte Verifikationstechniken bei unvollständiger Information
| project staff
| cooperation partners
| project description | project target | publications
|
| Chair of Computer Architecture | |
| Bernd Becker, Prof. Dr. | |
| Chair of Operating Systems | |
| Christoph Scholl, Prof. Dr. | |
| Computer Architecture and Operating Systems | |
| Stefan Disch, Dipl.-Inf. | |
| former employee Chair of Computer Architecture | |
| Marc Herbstritt, Dr. | |
|
| |
| Chair of Operating Systems | |
| Tobias Nopper, Dipl.-Inf | |
| former employee of studygroup Operating Systems | |
| Mathias Büche | |
Technological improvements enable an ever increasing chip complexity. Thus current ASICs may contain up to 100 millions of transistors. Besides the actual design process the proof of correctness is evolving to a challenge. The costs of this step sometimes comprise more than half of the overall design costs. Due to the fact that pure simulation on larger systems only covers a very small part of the system behavior, formal methods to prove the correctness of circuits has gained in importance over the last 10 years enormously. Commercial tools with integrated automatic formal verification approaches are available and used in industry. The methods can be classified as follows:
- Equivalence checking of combinational circuits
- Equivalence checking of sequential circuits
- Proof of properties for sequential circuits
While the combinational equivalence check is applicable on very large circuits with several millions of gates, the sequential equivalence check or property check aims at components with up to 100,000 gates. But all of this methods are nearly exclusively limited to the proof of the correctness of complete design descriptions. On the other hand, errors detected late in the design process in general lead to very high costs. Thus it is worthwhile to take actions for detection of (already) existing errors as early as possible. This means that there should be an effort to detect errors at a point in the design process, when the system description is still incomplete.
So far, in an industrial environment simulation based methods are used nearly exclusively, when used at al in the context of incomplete descriptionsl. First results show that through the usage of formal verification techniques already in early design stages a more exact error detection is possible. Thus, techniques to automaticaly verify incomplete designs in the areas of combinational equivalence checking, sequential equivalence checking and property checking should be developed and tested in realistic scenarios.
These techniques can also be used to perform error-diagnosis on erroneous circuits. The error-diagnosis should enable the designer to isolate possible error locations for error correction.
The goals of the project are:
- Further development of the combinational equivalence check for incomplete designs
- Equivalence tests for sequential circuits with incomplete information
- Proof of properties of sequential circuits with incomplete information
|
C. Scholl, B. Becker Checking Equivalence for Circuits Containing Incompletely Specified Boxes |
|
C. Scholl, B. Becker Checking Equivalence for Partial Implementations |
|
T. Nopper, C. Scholl Approximate Symbolic Model Checking for Incomplete Designs |