TABLE OF CONTENTS In Chapter 6, we examined singly-clocked designs and multiply-clocked designs where all signals in a property are clocked on the same clock. Suppose now that we have the case shown in Figure 14.1. That is, we want to specify that signal b is a latched version of signal a, where signals a and b are clocked with different clocks. Obviously, we will have to write a property that contains multiple clocks. As we have seen in Chapter 6 for the case of singly clocked designs, the issue of whether the design is edge-triggered or level-sensitive is one of implementation the clocking can be performed in both cases by selecting PSL cycles in which the signals are guaranteed to be at a steady state.
Let's assume that the latches of Figure 14.1 are either edge-triggered on the rising edge of the clock, or level-sensitive to the high value of the clock. The solution in the case of the falling edge or sensitivity to the low value of the clock is of course similar. If the clocks are well-behaved that is, if they are interleaved then signals a and b might behave as shown in Trace 14.2(i). Intuitively, we'd like to look at pairs of cycles (2,7), (12,17), etc. Which PSL cycles should our clock operator filter in order to see these pairs? We would like...
