Stats

  • Locked Locked
  • Replies 15
  • Subscribers 67
  • Views 5417
  • 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

Questions about IFV - PLS Help! - New to IFV

alexlop

 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.

 

  • 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,

  • 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.

  •  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 

  • 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.

  • I had initialised certain signals first using cutpoints and then giving them constraints in the tcl file.

    Yet, the values of these signals is shown as 'Z' in the waveform.

    Could anyone please help me out where I have missed something? 

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.