Home > Community > Forums > Functional Verification > Failure of liveness property

Email

* Required Fields

Recipients email * (separate multiple addresses with commas)

Your name *

Your email *

Message *

Contact Us

* Required Fields
First Name *

Last Name *

Email *

Company / Institution *

Comments: *

 Failure of liveness property 

Last post Wed, Feb 20 2013 6:06 AM by TAM1. 2 replies.
Started by Wesh 20 Feb 2013 05:52 AM. Topic has 2 replies and 708 views
Page 1 of 1 (3 items)
Sort Posts:
  • Wed, Feb 20 2013 5:52 AM

    • Wesh
    • Not Ranked
    • Joined on Wed, Jan 9 2013
    • Posts 2
    • Points 40
    Failure of liveness property Reply
    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?
    • Post Points: 35
  • Wed, Feb 20 2013 6:03 AM

    • StephenH
    • Top 25 Contributor
    • Joined on Tue, Sep 2 2008
    • Bristol, Avon
    • Posts 258
    • Points 4,100
    Re: Failure of liveness property Reply

    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') );

     

    Steve Hobbs / Applications Engineer / Cadence Functional Verification
    • Post Points: 5
  • Wed, Feb 20 2013 6:06 AM

    • TAM1
    • Top 75 Contributor
    • Joined on Thu, Jul 17 2008
    • HOME, PA
    • Posts 82
    • Points 1,085
    Re: Failure of liveness property Reply

     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') );

    • Post Points: 5
Page 1 of 1 (3 items)
Sort Posts:
Started by Wesh at 20 Feb 2013 05:52 AM. Topic has 2 replies.