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.

 

Parents

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

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.

Children
No Data

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.