Unexpected behaviour of implication operator in SVA

SystemVerilog
,
1

I am trying to self educate myself about assertions in System Verilog. I have written a code to understand implication operator. The code can be found at Eda Play Ground

Code Summary

  1. In my code I have defined states corresponding to each count of a counter.
  2. I have defined a sequence s2_7 which is a sequence starting at (count == 2) and ending at (count == 7).

sequence s2_7;
(state == 2) ##1 (state == 3) ##1 (state == 4) ##1 (state == 5) ##1 (state == 6) ##1 ((state == 7));
endsequence
  1. I have defined a property directive with label ‘test_3:’ which asserts the sequence s2_7.
test_3: assert property ( @(posedge clk) (state==STATE2) |=>s2_7) $display("%0.0t, Property s2_7 is asserted.",$time());
  1. My code prints below line when the antecedent of the property is true.

35, Start property sequence s2_7 , state = STATE3

  1. My code prints below line when the sequence s2_7 has started.

45, Starting sequence s2_7 , state = STATE4

Below is the output from my code.

0, state = STATE1
25, state = STATE2
35, Start property sequence s2_7 , state = STATE3
35, state = STATE3
45, Starting sequence s2_7 , state = STATE4
45, state = STATE4
55, state = STATE5
65, state = STATE6
75, state = STATE7

Issue

I have trouble understanding below line of the output.

45, Starting sequence s2_7 , state = STATE4

Here I had never expected the consequent of the property to get evaluated . This is because the value of state after one clock cycle of the antecedent is STATE3. So the sequence s2_7 will never be started.

Plz someone explain this.

2

Ran your code with different vendors and got different results.
What you have is a tool issue. Rerun your code with various vendors and see what you get.
We do not address tool issues in this forum, thus I’ll not name any tool that has the issue.
Note that the “state” variable, when used in the property of the assertion, is the sampled value of state. When used in the action block it is incremented value performed in the NBA region. If you need the sampled value to be displayed in the action block then you need to the $sampled(variable_name). BTW, your tool may not support $sampled(state.name)
The correct result is


                   0, state = STATE1
#                   25, state = STATE2
#                   35, Start property sequence s2_7 , state = STATE2
#                   35, state = STATE3
#                   45, Starting sequence s2_7 , state = STATE3
#                   45, state = STATE4
#                   55, state = STATE5
#                   65, state = STATE6
#                   75, state = STATE7
#                   85, state = STATE8
# 95, Property s2_7 is asserted.
#                   95, Sequence s2_7 has finished
#                   95, state = STATE1

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr

  1. VF Horizons:PAPER: SVA Alternative for Complex Assertions | Verification Academy
  2. http://systemverilog.us/vf/SolvingComplexUsersAssertions.pdf
  3. “Using SVA for scoreboarding and TB designs”
    http://systemverilog.us/papers/sva4scoreboarding.pdf
  4. “Assertions Instead of FSMs/logic for Scoreboarding and Verification”
    October 2013 | Volume 9, Issue 3 | Verification Academy
  5. SVA in a UVM Class-based Environment
    SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy
3

In reply to ben@SystemVerilog.us:

Hi Ben,

Thanks a lot for the reply.
It would be very grateful if you can also explain my doubt below.

At time 45, the sampled value of ‘state’ is ‘STATE3’, so I am really confused as to how the sequence s2_7 did even start.

Thanks
Abhay

4

In reply to absingh:
You are correct in your observation: The assertion SHOULD FAIL because at time 45 state==3, yet the assertion expects a state==2.
The issue is the enumerated type. Works OK if you are more specific on the definition of the values for the enumeration.


   
  typedef enum bit [3:0] {STATE1=4'b0001, STATE2=4'b0010, STATE3=4'b0011, STATE4=4'b0100, STATE5=4'b0101, STATE6=4'b110, STATE7=4'b0111, STATE8=4'b1000} state_e;
   
   state_e state;
// simulation
                   0, state = 
                   5, state = STATE1
                  25, state = STATE2
                  35, Start property sequence s2_7 , state = STATE2
                  35, state = STATE3
"testbench.sv", 69: top.test_3: started at 35ns failed at 45ns
	Offending '(state == 2)'  // [Ben] <---------------------------------------
                  45, state = STATE4

1800’2017 6.19 Enumerations describes the enuneration types.
Coming from a VHDL background, I prefer to declare the enum types in a safe manner as shown above. Originally you had declared the type as 3 bits instead of 4, but that did not fix the problem. Your code looked OK otherwise. There must be a hidden explanation. I’ll dig into it with colleagues.
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home

  1. VF Horizons:PAPER: SVA Alternative for Complex Assertions - SystemVerilog - Verification Academy
  2. http://systemverilog.us/vf/SolvingComplexUsersAssertions.pdf
  3. “Using SVA for scoreboarding and TB designs”
    http://systemverilog.us/papers/sva4scoreboarding.pdf
  4. “Assertions Instead of FSMs/logic for Scoreboarding and Verification”
    https://verificationacademy.com/verification-horizons/october-2013-volume-9-issue-3
  5. SVA in a UVM Class-based Environment
    https://verificationacademy.com/verification-horizons/february-2013-volume-9-issue-1/SVA-in-a-UVM-Class-based-Environment
5

In reply to ben@SystemVerilog.us:

OK, the issue is the way you declared the value of the variable state. In the sequence declaration, you used state == 2 instead of state==STATE2
An easy mistake that is hard to detect. Though I far prefer SystemVerilog over VHDL, VHDL would not have allowed you to write state == 2, whereas SystemVerilog is more lenient (or lax), and that can lead to errors. BE CONSSITENT!

Works OK. sequence s2_7; (state == STATE2, …
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home

  1. VF Horizons:PAPER: SVA Alternative for Complex Assertions - SystemVerilog - Verification Academy
  2. http://systemverilog.us/vf/SolvingComplexUsersAssertions.pdf
  3. “Using SVA for scoreboarding and TB designs”
    http://systemverilog.us/papers/sva4scoreboarding.pdf
  4. “Assertions Instead of FSMs/logic for Scoreboarding and Verification”
    https://verificationacademy.com/verification-horizons/october-2013-volume-9-issue-3
  5. SVA in a UVM Class-based Environment
    https://verificationacademy.com/verification-horizons/february-2013-volume-9-issue-1/SVA-in-a-UVM-Class-based-Environment