Stats

  • Locked Locked
  • Replies 2
  • Subscribers 66
  • Views 13873
  • Members are here 0
This discussion has been locked.
You can no longer post new replies to this discussion. If you have a question you can start a new discussion

Failure of liveness property

Wesh
Hi everybody

I'm trying to verify the following property:
-- psl assert_p1: assert always ( (CS = st_idle) -> next eventually! ((CS = st_get_ack) or (CS = st_set_ack)) );

The section "Waveforms for Liveness Assertions" of chapter 9 on the document Formal Verifier User Guide says: "A failed liveness assertion has an associated counter-example in which there is an infinitely repeating sequence of non-satisfying states for the assertion." And this is exactly what the problem is. The property fails and the counter-example has a LoopMarker. I suppose I have to force IFV to verify for more time?

The DUT is a state machine implementation in which CS is a user-defined type signal representing the current state and st_idle, st_get_ack, st_set_ack, etc are states of the state machine. st_idle has a transition for itself until it matches a value for three different signals. The VHDL code of this behaviour is the following:

when st_idle =>

    if ready_i = '1' and busy_s = '0' then
        NS      <= st_get_ack;
    
    elsif ready_frame_i = '1' then
        NS      <= st_set_ack;

    else
        NS      <= st_idle;The property above checks if  

 
It's interesting that a property checking if states st_set_ack and st_get_ack are never achieved and failed as well:
-- psl assert_pn1: assert never ( (CS = st_get_ack) or (CS = st_set_ack) ); 
  
What can I do?

  • This is normal. You must also specify a fairness property (constraint) that tells the tool to eventually assert whatever input the design is waiting for. In you case I guess that's either ready_i or ready_frame_i, if those are the correct primary inputs.

    -- psl assume always ( eventually! (ready_i ='1' or ready_frame_i = '1') );

     

  •  It sounds like the tool is working as it should. For a property to fail, it only takes a single example in which it turns out to be untrue, no matter how many other scenarios exist in which it is true. From the code you've shown, if ready_frame never goes high and if ready_i and busy_s never take on the correct states, the state machine will stay in the idle state forever. 

     

    Usually you need a kind of condition called a "fairness constraint" to ensure that a liveness property does not get stuck in an infinite loop waiting for something to occur. A fairness constraint says that something will occur eventually if you wait long enough. For your example, you may need to add a constraint such as:

     

    -- psl ready_frame_fairness: assume always ( eventually! (ready_frame = '1') );

Community Guidelines

The Cadence Design Communities support Cadence users and technologists interacting to exchange ideas, news, technical information, and best practices to solve problems and get the most from Cadence technology. The community is open to everyone, and to provide the most value, we require participants to follow our Community Guidelines that facilitate a quality exchange of ideas and information. By accessing, contributing, using or downloading any materials from the site, you agree to be bound by the full Community Guidelines.