Assertions Check if Signal is High when it enters a state and Stays High

I want to check If my Signal A is high as long as I am in the FSM ‘FSM_WAIT’ State. If A goes low anywhere in this State I should flag an error. The Assertion should also check that the signal is High when it enters the FSM_WAIT state

I tried a sample Code somewhat like this.

 @(posedge clk )
        disable iff (!reset)
       (fsm_state==FSM_WAIT ) && A |-> A until (fsm_state!=FSM_WAIT );
    endproperty : p_try  

But this will not be active if A is low when it enters the FSM Wait State. So it will not flag an error correct ?

In reply to pagarwa5:

use until_with.

In reply to dave_59:


// Is this what you need? 
//  A           0  0  1  1  1  1  1  X 
// FSM_WAIT     0  0  0  1  1  1  1  0
 $rose(fsm_state==FSM_WAIT)  |-> $past(A) and 
           A until_with (fsm_state!=FSM_WAIT );

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home.html
** 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: Component Design by Example FREE BOOK: Component Design by Example … A Step-by-Step Process Using VHDL with UART as Vehicle | Verification Academy
    Real Chip Design and Verification Using Verilog and VHDL($3) Amazon.com
  3. Papers:

In reply to pagarwa5:

A throughout fsm_check matches along a finite interval of consecutive clock ticks provided fsm_check matches along the interval and A evaluates to true at each clock tick of the interval.

sequence fsm_check;
	fsm_state == FSM_WAIT;  
endsequence

property fsmcheck;
  @(posedge clk) disable iff(!reset)
  A throughout fsm_check;
endproperty