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