This tutorial explores semantic differences between some of the most commonly used PSL operators. The assertions in this tutorial have been kept very simple, so that it is easy to see the differences between the operators. It is important to understand these distinctions before attempting to write practical, real world assertions.

For all the examples in this tutorial, we use two input signals (SIG0 and BUS[7:0]) and all the assertions are clocked off the positive edge of CLK0. The assertions will make a new match attempt on each positive edge of CLK0, even though previous match attempts by the assertion are still in progress. When such overlapping match attempts occur, additional "overflow" signals will be created to display the resulting transaction records without overlapping them on a single result signal. These overlap signals are creating dynamically as needed during the simulation, and get cleaned up automatically at the beginning of any new simulation run.

The above image shows all of the results for the following equations:

•Match all occurrences of simple pattern one_SIG0 = {SIG0}

•Match consecutive occurrences with Concatenation Operator two_SIG0 = {SIG0;SIG0}

•Match with consecutive Repetition Operator  three_SIG0 = {SIG0[*3]}

•Match with non-consecutive Repetition Operator   three_SIG0_nonconsecutive = {SIG0[=3]}

•Bit-slices and the Boolean operators and_ with_bitslice = {BUS[1:0] & BUS[3:2]}

•Implication operator  implication = {{SIG0} |-> {SIG0}}

•Implication Next-Cycle operator  implication_next_cycle = {{SIG0} |=> {SIG0}}

•PSL Property  until_SIG0 = ((BUS > 2) until SIG0)