« zurück

Advanced Automation in Formal Verification of Processors

This book focuses on the functional verification of digital systems with a special focus on processors, using formal techniques. With the increasing size and complexity of digital systems, verification has become a major bottleneck in the design flow. Furthermore, embedded systems are used more and more in safety critical applications like automotive or avionic control and in medical equipment.

While simulation based methods cannot exhaustively verify large systems, formal verification offers a very high level of confidence. But, up to today, formal methods are difficult to use in practice, as they require deep knowledge of the verified design as well as a high expertise in the applied techniques. Here, the automation of these formal techniques is addressed in order to raise the verification productivity while maintaining the high quality of the results.

The contributions are twofold: in the first part of the book, improvements for the traditional bottom-up verification flow for digital systems are presented. The second part deals with an innovative top-down verification flow for processors, where the starting point is an abstract architecture description.

When facing the functional verification of smaller digital systems, a bottom-up approach is applied. Here, Bounded Model Checking (BMC) is used in order to prove the correctness of single hardware blocks before moving on to the integration of these components on system level. Even for embedded software, BMC can be used efficiently. For arithmetics and memories, word level techniques are used to speed up the automated proofs.

In this bottom-up flow, a coverage check provides feedback to the user and points him or her to those scenarios that have not been verified yet. This provides a clear guideline for the verification, while ensuring that the whole functionality of a design has been verified as soon as the coverage check is passed.

On the way to full coverage, the user is supported in writing properties by two supplementary techniques. A property analysis determines redundant assumptions in a property. In this way, properties can be strengthened automatically in order to meet the coverage goals more quickly. Based on this analysis, with inverse property checking, valid properties can be generated automatically, that match a given proof goal or expected behavior. These generated properties are then validated by the user wrt. the specification.

Overall, the presented techniques offer an advanced user support in order to speed up the formulation of concise properties that cover the complete functionality of the design under verification.

When focusing on restricted classes of hardware designs, a higher degree of automation can be achieved in a top-down approach. In this book, this is demonstrated for the example of processors. The functional verification of a processor consists in finding a mapping between the instruction set architecture (ISA) - the programmer's view, given by the textual specification - and the register transfer level (RTL) implementation. The main difficulty in this process is caused by the various optimizations found in modern processors.

In this book, a top-down verification approach for processors is presented. It starts with an abstract architecture description that can easily be derived from the ISA specification. This architectural model is then mapped to the RTL implementation. For this step, the user needs to implement a number of given mapping functions and predicates. These functions reflect the concepts of a correct implementation of a pipelined processor.

Based on the architecture description and the mapping information, a property suite is generated automatically that is complete by construction, i.e. the ISA of the processor is verified exhaustively. It can be checked on the RTL design using the efficient property checking tool OneSpin 360 MV. The method is demonstrated on an industrial processor design from the automotive domain. Using the new approach, the verification productivity could be doubled compared to a manual verification.

Moreover, the use of architectural models in the formal verification offers further possibilities for automation in the design flow. In the book, it is shown how such models can be used both for the verification as well as for the automatic generation of an instruction set simulator (ISS). ISSs play an important role for the early software development and testing. By using a single source for verification and the ISS, a proven correct simulator can be obtained as soon as the verification is completed. It can easily be adapted if late changes in the design or the specification occur.

Overall, the presented techniques allow for a more efficient formal verification of processors. By reusing the architectural models, a further gain in productivity can be achieved.