Unexpected behaviour of implication operator in SVA

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