Check for Illegal State Transition

SystemVerilog
,
1

Hi ,
I am writing a SVA to check for Illegal state transition : S2 => S4 => S6 . This state transition should throw an Error .

My 1st attempt was using ’ not ’ operator : edalink

However unlike my expectations :

  1. For +define+M1 , assertion doesn’t Fail at T:84 although there is an illegal state transition : S2 => S4 => S6
  2. For +define+M2 , assertion doesn’t Pass at T:84 ( via not( 0 ) ) although the transition is legal
  3. For +define+M3 , my expectation is due to Incomplete assertion the assertion should Fail at end of simulation at T:59.
    However there is No Failure

[Q1] Any suggestions why is it so ?

Also I understand that using ’ not ’ operator in the consequent would make it strong , so an alternative would be to use :

... |=>  not (  strong (  .... )  ) ;

[Q2] On trying another alternative using unary operator ’ ! ’ , I observe a Compilation Error .
My guess is that for ’ ! ’ the expression should be a boolean expression ( similar to Dave’s comments in difference-between-0-and-assertions )

  Is  there  any  possible  solution  using  ' ! '  instead  of  ' not '  operator  in  consequent  ?
2

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

3

In reply to ben@SystemVerilog.us:

Hi Ben ,
My apologies , I should have specified that current_st is clocked to posedge of clk .
Since the current_st may have the same state across multiple clocks , I used current_st as clocking event for better simulation performance .

I tried changing property and added an always block for debugging :


property  illegal_transitn ;    
    
    @( current_st )  ( current_st == State2 )  |=>   ( current_st == State4 )  ##0 ( 1 , $display(" TIME:%2t ( current_st == State4 ) " , $time ) ) 
    
    ##1  ( current_st == State6 )  ##0 ( 1 , $display(" TIME:%2t ( current_st == State6 ) " , $time ) )  ##0  0 ;
    
  endproperty
  
  always @( current_st ) begin
    
    $display(" TIME:%2t  current_st  Changes  to  %0s " , $time , current_st.name()  ) ;
    
  end

For +define+M1 : The always block is triggered thrice as per expectations whereas the display for ( current_st == State4 ) is observed at T:84 instead of T:54

My understanding was for property :


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

For +define+M1 :
Antecedent is True at T:14 , then consequent is evaluated whenever current_st changes next .
So 1st part of consequent expression ( current_st == State4 ) should be True at T:54 ,
then the last part ( current_st == State6 ) should be True at T:84 .

However the assertion doesn’t seem to work this way , any suggestions why ?

4

In reply to Have_A_Doubt:
I modified your original code with the not. I don’t understand your ##0 0
Loks OK to me.
BTW, you way way overdo the spaces and the blank lines.
You’re making the code very difficult to read.
Avoid this in the future.
If it’s too hard to read, I’ll ignore the post; sorry!


module  state_transition;  
  typedef  enum  bit [2:0]  {State[8]}  state_e;  
  state_e  current_st;  
  property  illegal_transitn;    
    @(current_st)  $rose(current_st == State2)  |=>  
     not((current_st == State4)  ##1  (current_st == State6));    
  endproperty  
  assert  property(illegal_transitn)  $display(" TIME:%2t  Assertion  PASSes " , $time);    
                                   else  $display(" TIME:%2t  Assertion  FAILS " , $time); 
  
  initial  begin    
  //`ifdef  M1      
    //   Illegal  State  Transition  :  S2  =>  S4  =>  S6      
    #14;  current_st = State2;    
    #40;  current_st = State4;    
    #30;  current_st = State6;   
  //`elsif  M2      
    //   State  Transition  :  S2  =>  S4  =>  S5    
    #10;  current_st = State1;    
    #14;  current_st = State2;    
    #40;  current_st = State4;    
    #20;  current_st = State5;  
  //`elsif  M3      
    //   ONLY  2  State  Transitions  :  S2  =>  S4 
    #14;  current_st = State2;    
    #40;  current_st = State4;    
  //`endif    
    #5  $finish();    
  end  
endmodule

1874×815 80.2 KB

1874×815 80.2 KB

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
https://rb.gy/f3zhh