I have written below code to understand how within operator in SV works. Also following it I have put the partial simulation log.
What I am not able to figure out is that why s2_7_s3_6 ends at 85ns rather than 75ns. I expected s2_7_s3_6 to finish at 75 ns along with s2_7.
From the log I can see that the property was asserted at 85 with the message ‘Property asserted’. But here I was expecting it to get asserted at 75. Please help me to understand this.
There are two sequences defined in below code that I have used with ‘within’ operator.
- s2_7 ;
sequence s2_7;
(state == 2) ##1 (state == 3) ##1 (state == 4) ##1 (state == 5) ##1 (state == 6);
endsequence
- s3_6; .
sequence s3_6;
(state == 3) ##1 (state == 4) ##1 (state == 5) ;
endsequence
Property
property within_check;
(state==STATE2) |=> s2_7_s3_6;
endproperty
Directive
test_1: assert property ( @(posedge clk) within_check)
$display("%t, Property asserted",$time());
Below is the full code
// Code your testbench here
// or browse Examples
module top;
bit clk;
bit reset;
bit[2:0] count;
typedef enum bit [2:0] {STATE1, STATE2, STATE3, STATE4, STATE5, STATE6, STATE7, STATE8} state_e;
state_e state;
always
#5 clk = ~clk;
initial
$monitor("%t, state = %s, reset =%b, count = %d", $time(), state.name(), reset, count);
initial
begin
clk = 0;
reset = 0;
@(negedge clk ) reset = 1;
end
initial
begin
wait(state== STATE8);
#1 $finish();
end
always@(posedge clk)
begin
if(!reset)
begin
state = STATE1;
count <=0;
end
else
begin
count <= count + 1;
case(count)
'd0 : state <= STATE1;
'd1 : state <= STATE2;
'd2 : state <= STATE3;
'd3 : state <= STATE4;
'd4 : state <= STATE5;
'd5 : state <= STATE6;
'd6 : state <= STATE7;
'd7 : state <= STATE8;
endcase
end
end
//Clock will be set implicitly or explicitly by the property layer.
sequence s2_7;
(state == 2) ##1 (state == 3) ##1 (state == 4) ##1 (state == 5) ##1 (state == 6);// ##1 (state == 7);
endsequence
sequence s3_6;
(state == 3) ##1 (state == 4) ##1 (state == 5) ;//##1 (state == 6);
endsequence
sequence s2_7_s3_6;
s3_6 within s2_7;
endsequence
property within_check;
(state==STATE2) |=> s2_7_s3_6;
endproperty
test_1: assert property ( @(posedge clk) within_check)
$display("%t, Property asserted",$time());
endmodule
Partial LOg
0, state = STATE1, reset =0, count = 0
10, state = STATE1, reset =1, count = 0
15, state = STATE1, reset =1, count = 1
25, state = STATE2, reset =1, count = 2
35, state = STATE3, reset =1, count = 3
45, state = STATE4, reset =1, count = 4
55, state = STATE5, reset =1, count = 5
65, state = STATE6, reset =1, count = 6
75, state = STATE7, reset =1, count = 7
85, Property asserted
85, state = STATE8, reset =1, count = 0
