CODEWITHSUNDEEP
validationsystem-verilogverificationassertionsystem-verilog-assertions
lboxa
lboxa

Reputation: 1

Meaning of [->1] in system verilog property definition

I haven't been able to find the meaning of the [->] expression. I am familiar with using ranges as [a:b] or sequences such as EVENT1|->EVENT2, but not with the one I mentioned at the beginning.

The context is an assert property that ensures that clk1 is always toggling when reset is low. 

@(clk2) disable iff(rst) !$stable(clk1)[->1];

Any idea on what [->] really means?

Thanks in advance!

Upvotes: 0

Views: 4694

Answers (3)

Srujan Patel
Srujan Patel

Reputation: 46

There are basically 3 repetition operators available in system verilog as stated and explained in other answers.

The code

    @(clk2) disable iff(rst) !$stable(clk1)[->1];

can be interpreted as follows:

'Disable' the assertion property if 'rst' is high. If not so, check if the 'clk1' is 'not' stable for '1' clk2 clock changes(either from high to low or low to high), not necessarily on successive clk2 clock changes.

which means that the assertion:

  • will get disabled(i.e neither pass nor fail) if rst is 1.

  • will pass if clk1 is not stable(remains in the state it is, i.e either high or low) for 1 clk2 clock change. But it is not necessary that clk1 has to be unstable on successive clk2 clock changes.

  • will fail otherwise.

It in the suggests that you want to check if clk1 is operating at a higher frequency than clk2.

Upvotes: 1

Karan Shah
Karan Shah

Reputation: 1992

There are basically 3 operators like this :

Consecutive Repetition [*n] - 

(a ##1 b[*2] ##1 c) = (a ##1 b ##1 b ##1 c)

This means that, a should be asserted, after that b should be asserted on consecutive 2 clock ticks, following assertion of c in the next clock tick.

Goto Repetition [->n] - 

(a ##1 b[->2] ##1 c) = (a ##1 ((!b[*0:$] ##1 b)[*2]) ##1 c)

This means that, a should be asserted, after that b should be asserted on 2 clock ticks, but not consecutively. And as soon as b is asserted on 2 clock ticks, on the next clock tick c should get asserted

Nonconsecutive Repetition [=n] - 

(a ##1 b[=2] ##1 c) = (a ##1 ((!b[*0:$] ##1 b)[*2]) ##1 !b[*0:$] ##1 c)

This means that, a should be asserted, after that b should be asserted on 2 clock ticks, but not consecutively. And as soon as b is asserted on 2 clock ticks, c should get asserted, before b again gets asserted 3rd time.

Remember, difference between [->n] & [=n] operator, is related to the last operand "c". In [->2], c should be asserted, on the next clock tick, as soon as b is asserted twice (non consecutively). But in [=2], c should be asserted, before b gets asserted 3rd time (non consecutively)

Upvotes: 3

Matthew
Matthew

Reputation: 13967

[->N] means "non-consecutive exact repetition". a[->N] means N non-consecutive repetitions of a, with the match occurring exactly after the Nth repetition of a.

So, for example, a ##1 b[->2] ##1 c will match

          _
a _______/ \_____________________
         |          _     _ 
b _________________/ \___/ \_____
         |                  _
c _________________________/ \___
         |                   |
         |                   |
match    |<----------------->|

but not

          _
a _______/ \___________________________
                    _     _ 
b _________________/ \___/ \___________
                                  _
c _______________________________/ \___

[=N] means "non-consecutive repetition". a[=N] means N non-consecutive repetitions of a, with the match occurring any time after the Nth repetition of a.

So, for example, a ##1 b[=2] ##1 c would match the second pattern, above.

Upvotes: 2

Related Questions