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

CHAPTER 10

More Verification Case Studies

In this chapter we discuss some additional verification case studies, further illustrating the application of the major tools discussed in Chapters 4–6.

10.1 VERIFICATION OF COMBINATIONAL LOGIC

As indicated in Chapter 1, the major part of this book deals with the event-based approach to the specification, description, and verification of circuits and systems. However, we also devote a small part of this text to the level-based approach, particularly in connection with the use of Full LOTOS (see Section 4.9).

Indeed, in Section 4.9.1 we illustrated the application of Full LOTOS to the description of the NOT-gate, using a level-based approach. In this section we continue our use of Full LOTOS to the level-based descriptions of two-input combinational gates.

10.1.1 The AND Gate

We start with the AND-gate. This gate has two inputs, say in1 and in2. When stable, the output becomes out = in1 ∧ in2. The AND operator ∧ is referred to in the library ‘BOOLEAN’ (see Section 4.9) as ‘and’.

The following is one way of specifying a (non-terminating) two-input AND-gate using Full LOTOS:

File ANDgate.lotos
specification ANDgate[in1,in2,out]:noexit
library BOOLEAN endlib
behaviour
      ANDgate[in1,in2,out]
where
     process ANDgate[in1,in2,out]:noexit:=
               (in1 ?x:Bool;
               in2 ?y:Bool;
               out! (x and y);
               ANDgate[in1,in2,out])
               []
               (in2 ?y:Bool;
               in1 ?x:Bool;
               out! (y and x);
               ANDgate[in1,in2,out])
      endproc
endspec
___________

In this version of the AND-gate, the two gate inputs ...