SVA Check for Illegal State transition

SystemVerilog
,
1

Hi All ,

I want to write an assertion that checks that State Transition of A => C => E => F doesn’t occur .

I tried the following :: edaplayground

(a) Using +define+M1 :: I observe 2 assertion failures , at T: 25 and T: 35 .
I expected the failure at T : 35 however I am not sure why is there an error at T:25 ?

(b) Using +define+M2 :: There is no illegal state transition yet an assertion failures occurs at T: 25 . Why is to so ?

(c) Using +define+M3 :: There is no illegal state transition yet 2 assertion failures occurs at T: 25 and T: 35. Any suggestions why ?

My understanding is that since multiple non-overlapping implication operator exists , only when the entire antecedent is True i.e

(  ps  ==  A )  |=>  (  ps  ==  C )  |=>  (  ps  ==  E ) // When  True

the consequent ( ps == F ) is checked else there would be a Vacuous pass .

(2) If user were to write ::


     property  state_trans ;
    
    @( ps )  not(  A  |=>  C  |=>  E  |=>  F  ) ;  
    
  endproperty  
    

  The  value  of  the  enum  state  i.e  A (0) , C (2) , E (4) and F (5)  would  be  used  to  evaluate  the  property  expression  instead  of  the  actual  present  state  right ?

(3) Since not makes the expression strong whereas ! would keep it weak by default , I tried using ! instead of not in the code .

 However  I  observe  a  compilation  error , not sure why
2

In reply to ben@SystemVerilog.us:
Too many implication operators


 property  state_trans ;    
    @(posedge clk )  not( 
      %rose(ps==A) |-> ##1 (ps==C) ##1  (ps==E) ##1  (ps==F) ) ;
  endproperty

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats | Verification Academy
  2. Free books:
  1. Papers:
    Understanding the SVA Engine,
    Verification Horizons - July 2020 | Verification Academy
    Reflections on Users’ Experiences with SVA, part 1
    Reflections on Users’ Experiences with SVA | Verification Horizons - March 2022 | Verification Academy
    Reflections on Users’ Experiences with SVA, part 2
    Reflections on Users’ Experiences with SVA, Part II | Verification Horizons - July 2022 | Verification Academy
    Understanding and Using Immediate Assertions
    Understanding and Using Immediate Assertions | Verification Horizons - December 2022 | Verification Academy
    SUPPORT LOGIC AND THE ALWAYS PROPERTY
    http://systemverilog.us/vf/support_logic_always.pdf
    SVA Alternative for Complex Assertions
    Verification Horizons - March 2018 Issue | Verification Academy
    SVA in a UVM Class-based Environment
    SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy
    SVA for statistical analysis of a weighted work-conserving prioritized round-robin arbiter.
    https://verificationacademy.com/forums/coverage/sva-statistical-analysis-weighted-work-conserving-prioritized-round-robin-arbiter.
    Udemy courses by Srinivasan Venkataramanan (http://cvcblr.com/home.html)
    https://www.udemy.com/course/sva-basic/
    https://www.udemy.com/course/sv-pre-uvm/