Home > Community > Forums > Functional Verification > Questions about IFV - PLS Help! - New to IFV

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: *

 Questions about IFV - PLS Help! - New to IFV 

Last post Thu, Jun 27 2013 11:07 PM by Kris4Rad. 15 replies.
Started by alexlop 20 Nov 2008 06:54 AM. Topic has 15 replies and 8152 views
Page 1 of 2 (16 items) 1 2 Next >
Sort Posts:
  • Thu, Nov 20 2008 6:54 AM

    • alexlop
    • Not Ranked
    • Joined on Thu, Nov 20 2008
    • Ashdod, 00-IL
    • Posts 7
    • Points 110
    Questions about IFV - PLS Help! - New to IFV Reply

     Hi,

    I am new to IFV (Formal Verifier), I've just started examining this tool a few days ago.

    In our company I am the first one to lern it so I have nobody to ask for help but you guys!

     

    Let's say I want to check some feature in the design.

    I have a state machine and  INPUT1 is "1" for one clock cycle then another clock cycle (on which I don't care about the inputs) followed by third clock cycle on which  INPUT2 is "1, now I want to check if after this sequence can the state machine be at (let's say) "state_7".

    First of all how can I  formulate the assumption for that kind of input sequence? I tried :

        sop_one_cycle : assume always {INPUT1} |-> {!INPUT1};
        short_packet : assume always {INPUT1} |-> {!INPUT2; INPUT2};

        coverS7 : cover {current_state == 7} @ (posedge clk);

    but as I understood from "ifvuser.pdf", {!INPUT2; INPUT2} will couse to contradiction as the IFV checks for INPUT2 and !INPUT2 at the same cycle of clock. (However it showed no error message)

    Anyway, how can I tell IFV that I want to check sequence of :INPUT1="1":nevermind:INPUT2="1":

    Thanks!!!

    P.S.

       If this is not the correct place to ask such a question please point me to the right forum.

     

    • Post Points: 35
  • Thu, Nov 20 2008 8:49 AM

    • FormalGuy
    • Not Ranked
    • Joined on Fri, Sep 26 2008
    • San Jose, CA
    • Posts 2
    • Points 155
    Re: Questions about IFV - PLS Help! - New to IFV Reply

     Hi Alexlop,

     You might want to get in touch with your Cadence support person for some IFV help. IFV has good support and they should help you get started on your formal verfication adventure.

    As far as your question goes - it looks like you are trying to shape a specific input stimulus through assumptions. This is a common mistake made by beginners who are familiar with simulation environments (I should know, I was one). Assumptions are used to inform the tool of the DUT's external environment - it is typically not a good idea to use assumptions to specify a directed input sequence like you are trying to do.

    Now, I think your intent is to do some design exploration. This is good and a cool application of IFV. To do this sort of thing - setup assumptions on your design inputs that capture the protocols for those inputs. For instance, if your design uses an AHB interface, then write a set of AHB assumptions so that the tool considers only valid AHB input sequences.

    Next, if you want to see if a specific sequence of events can occur, you write a cover statement like so -

    coverS7: cover {INPUT1 ; !INPUT1 ; INPUT2 ; current_state = 7} @(posedge clk);

    If this sequence is possible, within the set of assumptions on the design, then the tool will show you a trace demonstrating how this can happen. The nice thing about the trace is that if your inputs are not behaving as you (and the design) expect them to, then you can add more input assumptions. If it is not possible for the sequence to occur, then the tool will say that the cover Failed.

    Finally, this is the right forum for this type of question and you should find an adequate level of support here. Let me know if this helped.

    • Post Points: 5
  • Thu, Nov 20 2008 8:52 AM

    • FormalGuy
    • Not Ranked
    • Joined on Fri, Sep 26 2008
    • San Jose, CA
    • Posts 2
    • Points 155
    Re: Questions about IFV - PLS Help! - New to IFV Reply

     Further, if you wanted the second term of the cover to be"nevermind" then you can write it like so -

    s7: cover  {INPUT1; true; INPUT2; current_state= 7} @(posedge clk);

    • Post Points: 35
  • Mon, Nov 24 2008 12:15 AM

    • alexlop
    • Not Ranked
    • Joined on Thu, Nov 20 2008
    • Ashdod, 00-IL
    • Posts 7
    • Points 110
    Re: Questions about IFV - PLS Help! - New to IFV Reply

    Thank you FormalGuy.

    I haven't tried it yet because I am out of my office for a few days, but I try it as soon as I get back.

     

    • Post Points: 5
  • Thu, Nov 27 2008 6:58 AM

    • alexlop
    • Not Ranked
    • Joined on Thu, Nov 20 2008
    • Ashdod, 00-IL
    • Posts 7
    • Points 110
    Re: Questions about IFV - PLS Help! - New to IFV Reply

     Thanks FormalGuy! Everything worked just like I ment.

     

    Anyway for those who have no idea what is PSL and how to use it, I've found a nice tutorial: http://www.project-veripage.com/psl_tutorial_1.php

    (I find PSL easeir to lern than OVL)

    • Post Points: 5
  • Wed, Dec 3 2008 9:03 AM

    • alexlop
    • Not Ranked
    • Joined on Thu, Nov 20 2008
    • Ashdod, 00-IL
    • Posts 7
    • Points 110
    Re: Questions about IFV - PLS Help! - New to IFV Reply

     HELLO GUYS!

    I have another question.

    I am trying to tell IFV to assume that a packet starts with 'sop' and ends with 'eop' so that it will not look through options like 'eop' without 'sop' and 'sop' followed by 'sop'.

     I tried the following :

    assume_packet_length : assume always ({sop} => {(!sop && !eop)[*4:100];eop}) @ (posedge clk_l);

    but IFV doesn't like this, it shows vacuity problem.

    What is the reason for this and how can I solve this problem.

     Thanks!

    • Post Points: 20
  • Wed, Dec 3 2008 3:05 PM

    • ckomar
    • Not Ranked
    • Joined on Thu, Jul 17 2008
    • Phoenix, AZ
    • Posts 11
    • Points 100
    Re: Questions about IFV - PLS Help! - New to IFV Reply

    Hi,

     I would strongly encourage you to contact your local AE.  We have a training that will answer your questions. In addition, our training labs include an example that has an sop/eop protocol.  My guess is you'll be able to take those assertions from the lab, learn how/why they work and drop them into your design at the same time as learning all the other goodness about IFV.

     My guess is that this will be the fastest route to getting you going.

     Thanks,

    Chris

    • Post Points: 20
  • Thu, Jan 1 2009 4:48 AM

    • alexlop
    • Not Ranked
    • Joined on Thu, Nov 20 2008
    • Ashdod, 00-IL
    • Posts 7
    • Points 110
    Re: Questions about IFV - PLS Help! - New to IFV Reply

     Thanks ckomar.

     

    I have another question (to all of you).

    How can I check (if it is possible at all) that specific signal has or has not 'z' or 'x' values?

    Thanks.

    • Post Points: 20
  • Fri, Jan 2 2009 12:56 AM

    • JoergM
    • Top 500 Contributor
    • Joined on Thu, Jul 17 2008
    • Munich, Bavaria
    • Posts 28
    • Points 550
    Re: Questions about IFV - PLS Help! - New to IFV Reply

    Hi Alex,

    there is a built-in function in PSL and SVA: isunknown(<bit_vector>). It performs the check you are asking for. In IFV it will return false unless you configure IFV to evaluate Z on tristate signals.

    Joerg.

    • Post Points: 20
  • Thu, Feb 5 2009 9:20 AM

    • srinisv
    • Not Ranked
    • Joined on Thu, Feb 5 2009
    • Posts 2
    • Points 40
    Re: Questions about IFV - PLS Help! - New to IFV Reply

    Hi Guys,

           I  have one question. How can i check a combo module with the IFV. IFV ask for the clock.

    let say there 2 input signals and 2 o/p's

    IN1, IN2 , OUT1, OUT2

    the o/p depends on the both inputs as shown below.

    when ever (IN1 == x) && (IN2 == y) then (OUT1 == m) && (OUT == n)

     i had tried the following assertions.

    Lable_1: assert propery

    (

    (IN1 == x) && (IN2 == y))  |-> ((OUT1 == m) && (OUT == n))

    );

    the above assertion gives the error that clock is not spsified

    then i tried that

    assert always

    {

    (IN1 == x) && (IN2 == y))  |-> ((OUT1 == m) && (OUT == n))

    };

     the above assertion is not behaving in the intended way. please help me out

     Thanks

    Sri

     

    • Post Points: 20
  • Thu, Feb 5 2009 9:31 AM

    • JoergM
    • Top 500 Contributor
    • Joined on Thu, Jul 17 2008
    • Munich, Bavaria
    • Posts 28
    • Points 550
    Re: Questions about IFV - PLS Help! - New to IFV Reply

    Hi Sri

    I assume you want to describe the following property:

    // psl p1: assert always ((IN1 == x) && (IN2 == y))  -> ((OUT1 == m) && (OUT == n));

    Note the difference in the brackets ("()" for boolean and "{}" for sequences) and the implication operater "->" for booleans (rather than "|->" for sequences). The above syntax works without a clock. In SVA this is more difficult...

     Joerg.

    • Post Points: 20
  • Thu, Feb 5 2009 6:52 PM

    • srinisv
    • Not Ranked
    • Joined on Thu, Feb 5 2009
    • Posts 2
    • Points 40
    Re: Questions about IFV - PLS Help! - New to IFV Reply

    Hi Joerg,

            I had tried the as you said. but the IFV shows the assertion as fail. when i seen the waves i found that it is showing the

    the input condition as follow.

    IN1 == a and IN2 == b insted of x and  y respectively. can u please assess me on this.  how can i wrtie the same in SVA.

    Sri,

    • Post Points: 20
  • Fri, Feb 6 2009 1:02 AM

    • JoergM
    • Top 500 Contributor
    • Joined on Thu, Jul 17 2008
    • Munich, Bavaria
    • Posts 28
    • Points 550
    Re: Questions about IFV - PLS Help! - New to IFV Reply

    Hi Sri,

    there is no easy explanation why you see this in the waveform. The property can only fail if the condition left of the implication is true ((IN1 == x) && (IN2 == y)). Maybe you look at the wrong time in the waveform. I think it would be more efficient to conatct your local AE now and show him your waveform.

    Regards,
    Joerg.

    Filed under:
    • Post Points: 5
  • Thu, Jan 20 2011 4:53 PM

    • whitegold
    • Not Ranked
    • Joined on Fri, Jan 21 2011
    • Posts 1
    • Points 20
    Re: Questions about IFV - PLS Help! - New to IFV Reply

     Hi JoergM,

    I am using the function SVA "isunknown" and IFV ignored my assertion. Could you tell me how I could configure IFV to evaluate Z on tristate signals.

    Thanks 

    • Post Points: 20
  • Mon, Jan 24 2011 1:53 AM

    • JoergM
    • Top 500 Contributor
    • Joined on Thu, Jul 17 2008
    • Munich, Bavaria
    • Posts 28
    • Points 550
    Re: Questions about IFV - PLS Help! - New to IFV Reply

    Hi Whitegold,

    IFV has builtin support for the isunknown function already. Today $isunknown(net) maps to (net === 1'bz). In case of Boolean nets, this will be false. In case of a tristate signal or vector, it will check if any bit in the the vector can go to Z. Note that we do not check for X today.

    Please switch to a recent version of IFV if you do not observe this behavior.

    Regards,

    Joerg.

    • Post Points: 20
Page 1 of 2 (16 items) 1 2 Next >
Sort Posts:
Started by alexlop at 20 Nov 2008 06:54 AM. Topic has 15 replies.