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

CHAPTER 3

From Digital Hardware to Processes

In accordance with our event-based approach, we use processes (see Chapter 2) to represent specifications as well as implementations. For the purpose of verification, we use the toolsets listed in Section 1.4. This chapter is intended to introduce our verification approach, prior to the application of the above toolsets.

3.1 THE C-ELEMENT

In this section we review various hardware components, which will play an important role in the sequel. The C-Element (or CEL-circuit) is an example of such a component. It was introduced originally by D.E. Muller (1), and is frequently referred to as the “Muller C-Element.” It is sequential, i.e., it has a memory and its output is not uniquely determined by its current inputs.

3.1.1 The 2-Input CEL-Circuit

The 2-Input CEL-circuit has two binary inputs (ranging over 0 and 1), namely A and B, and one binary output Z. The circuit is stable iff A ≠ B or A = B = Z. A circuit is stable iff its output will not change as long as its inputs do not change. Assuming that the initial conditions are A = B = Z, its event-based (dynamic) behavior is represented by the following Blot expression:

Here (and later on) we use lower-case letters to denote a transition (both up and down) of the input or output denoted by the corresponding upper-case letter. If we wish to distinguish between the two types of transitions, ...