An Introduction to

Formal Hardware Verification

Carl-Johan Seger
Department of Computer Science
University of British Columbia
Vancouver, B.C., CANADA V6T 1Z2

e-mail: [email protected]

Abstract

Formal hardware verification has recently attracted considerable interest. The need for correct" designs in safety-critical applications, coupled with the major cost associated with products delivered late, are two of the main factors behind this. In addition, as the complexity of the designs increase, an ever smaller percentage of the possible behaviors of the designs will be simulated. Hence, the confidence in the designs obtained by simulation is rapidly diminishing. This paper provides an introduction to the topic by describing three of the main approaches to formal hardware verification: theorem-proving, model checking, and symbolic simulation. We outline the underlying theory behind each approach, we illustrate the approaches by applying them to simple examples, and we discuss their strengths and weaknesses. We conclude the paper by describing current on-going work on combining the approaches to achieve multi-level verification approaches.

1 Introduction

Design validation involves taking steps to guarantee that a design will perform according to its specification. There are at least three levels of validation:

1. Design validation|have we designed what we intended to design?

2. Implementation validation|have we actually implemented our design?

3. Manufacturing validation1|have we actually manufactured our implementation?

In this paper we will concern ourselves only with design validation. Of course, we can never hope to verify that we have met our intentions, since intentions are, at best, vague and imprecise and not something we can write down and reason about (in any formal mathematical sense anyway). However, what we would like to achieve is that we can verify that our design has some verifiable properties.

1Traditionally called testing.