|
|
|
|
|
|
|
|
|
|
|
Repetition Operators
|
|
|
When a sequence needs to be tested for repetion, then repetition operators are used. They are of three types as below. The min value can be less then 0 and max value as sees in earlier page is $. |
|
|
|
|
|
- Consecutive repetition ( [* ): Consecutive repetition specifies finitely many iterative matches of the operand sequence, with a delay of one clock tick from the end of one match to the beginning of the next. The overall repetition sequence matches at the end of the last iterative match of the operand.
- Goto repetition ( [-> ): Goto repetition specifies finitely many iterative matches of the operand boolean expression, with a delay of one or more clock ticks from one match of the operand to the next successive match and no match of the operand strictly in between. The overall repetition sequence matches at the last iterative match of the operand.
- Nonconsecutive repetition ( [= ): Nonconsecutive repetition specifies finitely many iterative matches of the operand boolean expression, with a delay of one or more clock ticks from one match of the operand to the next successive match and no match of the operand strictly in between. The overall repetition sequence
|
|
|
|
|
|
|
|
|
Empty Sequence : An empty sequence is one that does not match over any positive number of clock ticks. The following rules apply for concatenating sequences with empty sequences. An empty sequence is denoted as empty, and a sequence is denoted as seq. |
|
|
|
|
|
- (empty ##0 seq) does not result in a match.
- (seq ##0 empty) does not result in a match.
- (empty ##n seq), where n is greater than 0, is equivalent to (##(n-1) seq).
- (seq ##n empty), where n is greater than 0, is equivalent to (seq ##(n-1) 'true).
|
|
|
|
|
|
Example : Consective repetition Operators
|
|
|
|
|
|
We will be modeling assertion for following waveform. |
|
|
|
|
|
|
|
|
|
|
|
Code |
|
|
|
|
|
1 //+++++++++++++++++++++++++++++++++++++++++++++++++
2 // DUT With assertions
3 //+++++++++++++++++++++++++++++++++++++++++++++++++
4 module repetition_assertion();
5
6 logic clk = 0;
7 always #1 clk ++;
8
9 logic req,busy,gnt;
10 //=================================================
11 // Sequence Layer
12 //=================================================
13 sequence boring_way_seq;
14 req ##1 busy ##1 busy ##1 gnt;
15 endsequence
16
17 sequence cool_way_seq;
18 req ##1 busy [*2] ##1 gnt;
19 endsequence
20
21 sequence range_seq;
22 req ##1 busy [*1:5] ##1 gnt;
23 endsequence
24
25 //=================================================
26 // Property Specification Layer
27 //=================================================
28 property boring_way_prop;
29 @ (posedge clk)
30 req |-> boring_way_seq;
31 endproperty
32
33 property cool_way_prop;
34 @ (posedge clk)
35 req |-> cool_way_seq;
36 endproperty
37 //=================================================
38 // Assertion Directive Layer
39 //=================================================
40 boring_way_assert : assert property (boring_way_prop);
41 cool_way_assert : assert property (cool_way_prop);
42
43 //=================================================
44 // Generate input vectors
45 //=================================================
46 initial begin
47 req <= 0; busy <= 0;gnt <= 0;
48 @ (posedge clk);
49 req <= 1;
50 @ (posedge clk);
51 busy <= 1;
52 req <= 0;
53 repeat(2) @ (posedge clk);
54 busy <= 0;
55 gnt <= 1;
56 @ (posedge clk);
57 gnt <= 0;
58 // Now make the assertion fail
59 req <= 0; busy <= 0;gnt <= 0;
60 @ (posedge clk);
61 req <= 1;
62 @ (posedge clk);
63 busy <= 1;
64 req <= 0;
65 repeat(3) @ (posedge clk);
66 busy <= 0;
67 gnt <= 1;
68 @ (posedge clk);
69 gnt <= 0;
70 #30 $finish;
71 end
72
73 endmodule
You could download file repetition_assertion.sv here
|
|
|
|
|
|
Note : We can use range instead of [*3], something like [*1:3]. |
|
|
|
|
|
Simulation : Consective Repetition Operators
|
|
|
|
|
|
"repetition_assertion.sv", 32: boring_way_assert:
started at 13s failed at 19s
Offending 'gnt'
"repetition_assertion.sv", 33: cool_way_assert:
started at 13s failed at 19s
Offending 'gnt'
|
|
|
|
|
|
|
|
|
|
|
|
Example : Goto repetition Operators
|
|
|
|
|
|
We will be modeling assertion for following waveform. |
|
|
|
|
|
|
|
|
|
|
|
Code |
|
|
|
|
|
1 //+++++++++++++++++++++++++++++++++++++++++++++++++
2 // DUT With assertions
3 //+++++++++++++++++++++++++++++++++++++++++++++++++
4 module goto_assertion();
5
6 logic clk = 0;
7 always #1 clk ++;
8
9 logic req,busy,gnt;
10 //=================================================
11 // Sequence Layer
12 //=================================================
13 sequence boring_way_seq;
14 req ##1 (( ! busy[*0:$] ##1 busy) [*3]) ##1 gnt;
15 endsequence
16
17 sequence cool_way_seq;
18 req ##1 (busy [->3]) ##1 gnt;
19 endsequence
20
21 //=================================================
22 // Property Specification Layer
23 //=================================================
24 property boring_way_prop;
25 @ (posedge clk)
26 req |=> boring_way_seq;
27 endproperty
28
29 property cool_way_prop;
30 @ (posedge clk)
31 req |=> cool_way_seq;
32 endproperty
33 //=================================================
34 // Assertion Directive Layer
35 //=================================================
36 boring_way_assert : assert property (boring_way_prop);
37 cool_way_assert : assert property (cool_way_prop);
38
39 //=================================================
40 // Generate input vectors
41 //=================================================
42 initial begin
43 // Pass sequence
44 gen_seq(3,0);
45 repeat (20) @ (posedge clk);
46 // Fail sequence (gnt is not asserted properly)
47 gen_seq(3,1);
48 // Terminate the sim
49 #30 $finish;
50 end
51 //=================================================
52 /// Task to generate input sequence
53 //=================================================
54 task gen_seq (int busy_delay,int gnt_delay);
55 req <= 0; busy <= 0;gnt <= 0;
56 @ (posedge clk);
57 req <= 1;
58 @ (posedge clk);
59 req <= 0;
60 repeat (busy_delay) begin
61 @ (posedge clk);
62 busy <= 1;
63 @ (posedge clk);
64 busy <= 0;
65 end
66 repeat (gnt_delay) @ (posedge clk);
67 gnt <= 1;
68 @ (posedge clk);
69 gnt <= 0;
70 endtask
71
72 endmodule
You could download file goto_assertion.sv here
|
|
|
|
|
|
Simulation : Goto Repetition Operators
|
|
|
|
|
|
"goto_assertion.sv", 33: boring_way_assert:
started at 61s failed at 75s
Offending 'gnt'
"goto_assertion.sv", 34: cool_way_assert:
started at 61s failed at 75s
Offending 'gnt'
|
|
|
|
|
|
Example : NonConsective repetition Operators
|
|
|
|
|
|
We will be modeling assertion for following waveform. |
|
|
|
|
|
|
|
|
|
|
|
Code |
|
|
|
|
|
1 //+++++++++++++++++++++++++++++++++++++++++++++++++
2 // DUT With assertions
3 //+++++++++++++++++++++++++++++++++++++++++++++++++
4 module noncon_assertion();
5
6 logic clk = 0;
7 always #1 clk ++;
8
9 logic req,busy,gnt;
10 //=================================================
11 // Sequence Layer
12 //=================================================
13 sequence boring_way_seq;
14 req ##1 (( ! busy[*0:$] ##1 busy) [*3]) ##1 ! busy[*0:$] ##1 gnt;
15 endsequence
16
17 sequence cool_way_seq;
18 req ##1 (busy [=3]) ##1 gnt;
19 endsequence
20
21 //=================================================
22 // Property Specification Layer
23 //=================================================
24 property boring_way_prop;
25 @ (posedge clk)
26 req |-> boring_way_seq;
27 endproperty
28
29 property cool_way_prop;
30 @ (posedge clk)
31 req |-> cool_way_seq;
32 endproperty
33 //=================================================
34 // Assertion Directive Layer
35 //=================================================
36 boring_way_assert : assert property (boring_way_prop);
37 cool_way_assert : assert property (cool_way_prop);
38
39 //=================================================
40 // Generate input vectors
41 //=================================================
42 initial begin
43 // Pass sequence
44 gen_seq(3,0);
45 repeat (20) @ (posedge clk);
46 // This was fail in goto, but not here
47 gen_seq(3,1);
48 repeat (20) @ (posedge clk);
49 gen_seq(3,5);
50 // Lets fail one
51 repeat (20) @ (posedge clk);
52 gen_seq(5,5);
53 // Terminate the sim
54 #30 $finish;
55 end
56 //=================================================
57 /// Task to generate input sequence
58 //=================================================
59 task gen_seq (int busy_delay,int gnt_delay);
60 req <= 0; busy <= 0;gnt <= 0;
61 @ (posedge clk);
62 req <= 1;
63 @ (posedge clk);
64 req <= 0;
65 repeat (busy_delay) begin
66 @ (posedge clk);
67 busy <= 1;
68 @ (posedge clk);
69 busy <= 0;
70 end
71 repeat (gnt_delay) @ (posedge clk);
72 gnt <= 1;
73 @ (posedge clk);
74 gnt <= 0;
75 endtask
76
77 endmodule
You could download file noncon_assertion.sv here
|
|
|
|
|
|
Simulation : NonConsective Repetition Operators
|
|
|
|
|
|
"noncon_assertion.sv", 33: boring_way_assert:
started at 189s failed at 205s
Offending 'gnt'
"noncon_assertion.sv", 34: cool_way_assert:
started at 189s failed at 205s
Offending 'gnt'
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|