O'Reilly logo

Verification of Systems and Circuits Using LOTOS, Petri Nets, and CCS by Rakefet Kol, Michael Yoeli

Stay ahead with the world's most comprehensive technology and business learning platform.

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

Start Free Trial

No credit card required

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

Start Free Trial

No credit card required