TABLE OF CONTENTS Up until now, we have examined cycle-based traces we have not explicitly mentioned the clock. The clock operator allows you to describe traces that are based on "ticks" of one or more clock signals. For example, consider the requirement "two consecutive requests (assertions of signal req) are not allowed" in a design clocked on the rising edge of signal clk that behaves as shown in Trace 6.1(i). There are three "ticks" of the clock signal clk in Trace 6.1(i), each of them three cycles wide.
NOTE: The term cycle in PSL is defined as one iteration of the evaluation process, during which the state of the design is recomputed and may change. In other words, a cycle is the smallest granularity of time as seen by the trace in question. In a cycle-based environment, then, a PSL cycle corresponds to a clock cycle. In an event-based environment, a PSL cycle is different than a clock cycle. We will use the term cycle when we mean a PSL cycle, and clock cycle when we mean a clock cycle.
Getting back to our example, if we code an unclocked property expressing our specification, as in Property 6.1a, we find that it does not hold on Trace 6.1(i) (because req is asserted at the consecutive cycles 4 and 5, 5 and 6, 6 and 7, etc.). Despite the fact that Property...
