TABLE OF CONTENTS So now you know PSL. What are you going to do with it? In this chapter, we discuss the what, rather than the how, of specifying in PSL using three simple but real-world examples.
Suppose that the state machine shown in Figure 12.1 is part of your specification, and suppose that you are interested in writing PSL assertions to check the implementation. A common way to proceed would be to write an assertion about every transition in the state machine, like those shown in Figure 12.2. Such assertions are very low-level: they check that a few gates of the design function according to a few lines of the specification.
While low-level assertions can be useful, writing higher level assertions can be much more powerful. For instance, the low-level assertions do not ensure that processing ever completes. In all likelihood, that is an unspoken assumption of our specification. From Figure 12.1, we see that the signals controlling whether or not processing completes are continue, cancel, and done. We could write assertions about these signals and their relations to the states of our FSM, for instance, that if we are in state process1 or in state process2 we eventually get either a continue or a cancel, and if we are in state process3 we eventually get a done. However, there is a much...
