With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, tutorials, and more.

No credit card required

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

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

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, interactive tutorials, and more.

No credit card required