Saturday, March 03, 2012

Assertions - Sequences

Assertions - Sequences

A sequence is a list of boolean expressions in a linear order of increasing time. The sequence is true over time if the boolean expressions are true at the specific clock ticks. The expressions used in sequences are interpreted in the same way as the condition of a procedural if statement.

Here are some simple examples of sequences. The ## operator delays execution by the specified number of clocking events, or clock cycles.

a ##1 b // a must be true on the current clock tick and b on the next clock tick
a ##N b // Check b on the Nth clock tick after a
a ##[1:4] b // a must be true on the current clock tick and b on some clock tick between the first and fourth after the current clock tick

The * operator is used to specify a consecutive repetition of the left-hand side operand.

a ##1 b [*3] ##1 c // Equiv. to a ##1 b ##1 b ##1 b ##1 c
(a ##2 b) [*2] // Equiv. to (a ##2 b ##1 a ##2 b)
(a ##2 b)[*1:3] // Equiv. to (a ##2 b) or (a ##2 b ##1 a ##2 b) or (a ##2 b ##1 a ##2 b ##1 a ##2 b)

The $ operator can be used to extend a time window to a finite, but unbounded range.

a ##1 b [*1:$] ##1 c // E.g. a b b b b c.

The [-> or goto repetition operator specifies a non-consecutive sequence.

a ##1 b[->1:3] ##1 c // E.g. a !b b b !b !b b c

This means a is followed by any number of clocks where c is false, and b is true between 1 and three times, the last time being the clock before c is true.

The [= or non-consecutive repetition operator is similar to goto repetition, but the expression (b in this example) need not be true in the clock cycle before c is true.

a ##1 b [=1:3] ##1 c // E.g. a !b b b !b !b b !b !b c

Combining Sequences:

There are several operators that can be used with sequences:

The binary operator and is used when both operand expressions are expected to succeed, but the end times of the operand expressions can be different. The end time of the end operation is the end time of the sequence that terminates last. A sequence succeeds (i.e. is true over time) if the boolean expressions containing it are true at the specific clock ticks.

s1 and s2 // Succeeds if s1 and s2 succeed. The end time is the end time of the sequence that terminates last

If s1 and s2 are sampled booleans and not sequences, the expression above succeeds if both s1 and s2 are evaluated to be true.

The binary operator intersect is used when both operand expressions are expected to succeed, and the end times of the operand expressions must be the same.

s1 intersect s2 // Succeeds if s1 and s2 succeed and if end time of s1 is the same with the end time of s2

The operator or is used when at least one of the two operand sequences is expected to match. The sequence matches whenever at least one of the operands is evaluated to true.

s1 or s2 // Succeeds whenever at least one of two operands s1 and s2 is evaluated to true

The first_match operator matches only the first match of possibly multiple matches for an evaluation attempt of a sequence expression. This allows all subsequent matches to be discarded from consideration. In this example:

sequence fms;
first_match(s1 ##[1:2] s2);
endsequence

whichever of the (s1 ##1 s2) and (s1 ##2 s2) matches first becomes the result of sequence fms. The throughout construct is an abbreviation for writing:

(Expression) [*0:$] intersect SequenceExpr

i.e. Expression throughout SequenceExpr means that Expression must evaluate true at every clock tick during the evaluation of SequenceExpr.

The within construct is an abbreviation for writing:

(1[*0:$] ##1 SeqExpr1 ##1 1[*0:$]) intersect SeqExpr2

i.e. SequenceExpr1 within SequenceExpr2 means that SeqExpr1 must occur at least once entirely within SeqExpr2 (both start and end points of SeqExpr1 must be between the start and the end point of SeqExpr2 ).

No comments:

Post a Comment

Popular Posts