Verification of Systems and Circuits Using LOTOS, Petri Nets, and CCS

CHAPTER 1

Introduction

Many present-day industrial hardware systems are of considerable complexity. Great efforts are required to produce such systems correctly at reasonable cost and within an acceptable time limit.

To achieve the above goals, it is important to detect design errors at an early stage, and particularly prior to the production process. The correction of design errors that have infiltrated the production process is very expensive and time-consuming.

In view of the above considerations, “formal verification” plays an important role. The purpose of formal verification is to ensure that the intended hardware design (the implementation) indeed meets the requirements of a given functional specification. Throughout this book, relevant concepts of formal verification will be discussed and made precise.

A number of publications have provided an introduction to some important aspects of formal verification. In particular, we refer the reader to References 1–5.

This book presents yet another approach to hardware verification. It deals with the verification of a wide selection of systems and circuits, and applies powerful toolsets for this purpose (see Section 1.4). It originates from the earlier work of Yoeli (6), who provided a step-by-step introduction to digital circuit verification. This book offers an introduction to the formal verification of combinational, iterative, synchronous, and asynchronous circuits. It also presents some valuable insight into approaching basic ...