Unexpected behaviour of implication operator in SVA

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