The sequence, which is the syntactic equivalent of the timing diagram, often provides the most convenient way to write properties in PSL, with time advancing as we move from left to right through the text. The Sequential Extended Regular Expression or SERE (which rhymes with beer) permits a compact abbreviation for many common timing relationships.
Consider the following assertion:
assert always {a;b} |-> {c;d};
As was explained above, the semicolon operator moves forward one cycle, whilst the suffix implication operator |-> means that the first sequence must always be followed by the second with an overlap of one cycle. (There is an alternative suffix implication operator |=> which requires that the two sequences do not overlap.)
SEREs permit longer sequences and families of related sequences to be written in a compact notation. For example:
{a[*2]} means {a;a}
{a[+]} means {a;a;...;a} with a repeated one or more times
{a[*]} means {a;a;...;a} with a repeated zero or more times
{[*]} matches any sequence whatsoever
{a[=2]} means {[*];a;[*];a;[*]}, i.e. non-consecutive repetition
{a[*1 to 3]} means {a} or {a;a} or {a;a;a}
There are also several operators that work with whole sequences:
{seq1} | {seq2} means that one or the other sequence must hold
{seq1} & {seq2} means that both sequences must hold
{seq1} && {seq2} means that both must hold and be of equal length
Next: Semantics
