A formal approach to hardware analysis

Abstract

Electronic circuits are entering many aspects of our daily lives. Considerations of safety and cost have prompted a good deal of interest in verifying that they function as expected. This thesis explores several ways of conducting such verifications using a formal, mathematical calculus. The calculus is based on sequences of events and has a simple semantics. One of the most important influences on hardware designs is time. A variety of temporal concepts are therefore represented in the calculus, including multilevel clocks, clock skew and others. Moving between different granularities of time is easily accomplished, thus providing support for temporally as well as spatially structured designs. Consequences of design decisions may not be immediately obvious, so it is important to have a way of investigating their ramifications. Accordingly, techniques are developed for experimenting on designs, as are several mechanisms for analyzing the results. Some exploit basic properties of the calculus to increase the efficiency of a simulation at no extra cost. More formal methods of verification are also provided that permit a large difference in complexity between a specification and its implementation. To ensure that this difference does not unwittingly introduce design errors, a notion of constraints on the use of an implementation is introduced. This finds application in building libraries of pre-verified parts, as well as during the refinement of hierarchical designs. Finally, the techniques are illustrated through several examples, including a hardware implementation of a deck of playing cards and a simple CRT controller.