Fachgebiet Entwurf Informationstechnischer Systeme (EIS)

Exercises to the lecture "Verification of Digital Systems"

General Information

The exercises will be held as a computer lab. In the exercises you will get to know an industrial software tool for formal property checking of digital systems. First you will make yourself familiar with the usage of the input language of the tool by some smaller exercises. Later on you will work on a slightly more complex verification task, verifying the functional correctness of a simple RISC processor.

Requirements

To understand the contents of the lecture and to be able to do the exercises, you will need an adequate knowledge in digital systems. You should know how to model and synthesize combinatorial and sequential circuits. You should be familiar with Boolean functions and the basic terminology of finite state machine design. For example, you should know AND-Gates, D-Flipflops and state diagrams.

In the exercises digital circuits will be modelled using the hardware description language VHDL. You do not need to create circuit models in VHDL by yourself. However, you have to be able to understand the described models well enough to formulate and verify the desired properties of the systems. Therefore, you will need a basic knowledge in VHDL that you can aquire during the course.

There is comprehensive literature dealing with VHDL, in form of books as well as in the internet. For example, you may refer to:

Furthermore, the temporal behavior of digital circuits will be specified using SystemVerilog Assertions (SVA). At the beginning of the semester a tutorial on this language will be given. As a supplement of this tutorial, the students may refer to: