Check for Illegal State Transition

In reply to Have_A_Doubt:
Your code:


state_e  current_st ;  
  property  illegal_transitn ;    
    @( current_st )  $rose( current_st == State2 )  |=>   
       not(  ( current_st == State4 )  ##1  ( current_st == State6 )  );     
  endproperty
  

Your clocking event is the variable current_st. Is current_st clocked by a clock or is it an asynchronous machine?
Thus, from what you have, $rose( current_st == State2
the sampled value of the variable current_st is the value of that variable before current_st change state. The $past of that is the one even before that.
I believe what you want is


state_e  current_st ;  
  property  illegal_transitn ;    
    @(posedge clk)  $rose( current_st == State2 )  |=>   
       not(  ( current_st == State4 )  ##1  ( current_st == State6 )  );     
  endproperty
  

The not is a property operator.
Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.

or Cohen_Links_to_papers_books - Google Docs

Getting started with verification with SystemVerilog