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