Property Specification Language Tutorial
Previous: Verification and Modeling Layers
Miscelleneous
Built in functions
PSL provides builtin 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 multiline comments.
In VHDL flavor, '' is used to add comments.
Previous: Verification and Modeling Layers
