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.
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 ...