Property Specification Language Tutorial

Previous: Verification and Modeling Layers

Miscelleneous

Built in functions

PSL provides built-in functions to detect value changes, some of the commonly used functionalities etc. Most of these functions can be used inside property expressions.

rose(arg)

This function returns a Boolean result that is true when there is transition from 0 to 1. Else the result is false. Example:

default clock = (posedge clk);
property start_cell = always {rose (SOC)} |=> { payload; EOC};

fell(arg)

This function is opposite to that of rose. The result is true when there is transition from 1 to 0. Else the result is false.

prev(arg [,N])

This function returns the value of the argument in the previous clock. The argument can be any expression. The optional argument N specifies how many clock cycles to look back in the history and is defaulted to 1.

stable(arg)

This function returns a Boolean result. If there is no change in the value of the expression from the previous cycle then the result is true. Otherwise it is false.

countones(arg)

Counts the number of ones in the argument.

onehot(arg), onehot0(arg)

Returns true if the argument has exactly/atmost one bit set to 1.

Comments

Comments can be added to PSL code using the same style as the underlying HDL. For example, in Verilog flavor one can use '//' for single line comments and '/*..*/' for multi-line comments. In VHDL flavor, '--' is used to add comments.

Previous: Verification and Modeling Layers