FORMAL VERIFICATION USING CONFORMAL LEC ( CADENCE TOOL)

Discussion in 'VHDL' started by kitcha, Jan 24, 2006.

  1. kitcha

    kitcha Guest

    I m working on formal verification. When i do a RTL vs Netlist
    comparison i get CUT-POINTS.
    How do i avoid it???
    kitcha, Jan 24, 2006
    #1
    1. Advertising

  2. kitcha wrote:
    > I m working on formal verification. When i do a RTL vs Netlist
    > comparison i get CUT-POINTS.
    > How do i avoid it???
    >


    You could use a functional rather than
    structural approach to show equivalence.
    That is, compare canonical representations
    instead of proving the equivalence at
    testpoints.

    But consider running a sim first,
    to see if you are even close.

    -- Mike Treseler
    Mike Treseler, Jan 24, 2006
    #2
    1. Advertising

  3. kitcha schrieb:

    > I m working on formal verification. When i do a RTL vs Netlist
    > comparison i get CUT-POINTS.
    > How do i avoid it???


    Maybe you should ask, why the tool inserted cutpoints.
    Cadence should help you a bit more. Cut-Points need to be infered to
    split up bidirectional buffers or to break up combinatorial feedbacks.


    Cutpoints can be a problem, but are normaly needed to handle the design
    properly, so don't worry to much about them. But maybe you should worry
    about combinatorial feedbacks?

    bye Thomas
    Thomas Stanka, Jan 31, 2006
    #3
  4. kitcha

    kitcha Guest

    thomas..i m finding loops in my rtl for which the tool inserts cut
    points..but on the netlist side i m not able to find any loops...what
    is the possible solution for this?
    kitcha, Jan 31, 2006
    #4
  5. Hi,

    kitcha schrieb:

    > thomas..i m finding loops in my rtl for which the tool inserts cut
    > points..but on the netlist side i m not able to find any loops...what
    > is the possible solution for this?


    You say you have combinatorial feedbackloops in RTL, which you don't
    find in the netlist?

    In that case you should check wheter your code is ambigous or if
    there's a bug in one of your tools (synthesis or Conformal LEC).

    In most cases the "bug" results from bad coding style. But when using
    some "nonstandard" statements like generics of array type or similar I
    often feel like a beta-tester for EDA tools. I've allready seen some
    strange results in a greater variety of tools when using such code *g*,
    so it would be no surprise if there's a real bug left in either
    synthesis or formal verification.

    bye Thomas
    Thomas Stanka, Feb 6, 2006
    #5
  6. kitcha

    kitcha Guest

    finally fixed the problem..thanks thomas
    kitcha, Feb 7, 2006
    #6
    1. Advertising

Want to reply to this thread or ask your own question?

It takes just 2 minutes to sign up (and it's free!). Just click the sign up button to choose a username and then you can ask your own questions on the forum.
Similar Threads
  1. thewhizkid
    Replies:
    3
    Views:
    708
    Jerker Hammarberg \(DST\)
    Oct 7, 2003
  2. Sebastian Jaeger

    Formal Verification Survey

    Sebastian Jaeger, Oct 24, 2003, in forum: VHDL
    Replies:
    0
    Views:
    1,704
    Sebastian Jaeger
    Oct 24, 2003
  3. ben cohen
    Replies:
    0
    Views:
    770
    ben cohen
    Jan 27, 2004
  4. subhash
    Replies:
    0
    Views:
    641
    subhash
    Aug 2, 2006
  5. sharatd
    Replies:
    0
    Views:
    1,897
    sharatd
    Oct 18, 2006
Loading...

Share This Page