Catalogue : Reviews
Reviews
|
Ulrich Kühne Advanced Automation in Formal Verification of Processors ISBN: 978-3-8322-8619-4 Price: 48,80 € / 97,60 SFR |
|---|---|
| This thesis addresses automation and enhanced user support in functional verification of digital systems with a special focus on processors. Verification is an important issue in the design process of digital systems. In contrast to traditional simulation based methods, formal verification can provide a mathematical correctness proof. But, up to today, these methods are dificult to use in practice without a strong background in formal techniques. This thesis aims at improving the usability and increasing the productivity of formal hardware verification. The functional verification of digital systems can be attacked bottom-up or top-down. For an ad hoc verification of single components or simple hardware systems, the specification is formalized step by step in a bottom-up manner. Thereby, the verification engineer is faced with the task to identify the implementation principles of the design and to capture the behavior in temporal logic properties. In this thesis, techniques are presented to speed up this process. This includes an easy to use coverage check that gives feedback about the quality of the written properties. The process of writing the properties can be supported by strengthening properties automatically. Another approach automatically generated properties for a given expected behavior of the design. When facing the verification of a restricted class of designs, further automation can be achieved in a top-down flow. In particular, for processors the task is to find a mapping between the instruction set architecture - the abstract programmer´s view - and the implementation. In this thesis, it is examined how parts of this process can be automated. The presented approach provides a guided verification flow, starting with a formal architecture description that is then related to the implementation. The use of architectural models in a structured verification flow can increase the productivity significantly. Further applications of such high-level models include the automatic generation of instruction set simulators and the automatic synthesis of embedded software. These issues are also addressed in this thesis. | |
| Source: Zentralblatt MATH 1190 - 1 | |
| go to details ... | |