Velocity Reviews - Computer Hardware Reviews

Velocity Reviews > Newsgroups > Programming > VHDL > FORMAL VERIFICATION USING CONFORMAL LEC ( CADENCE TOOL)

Reply
Thread Tools

FORMAL VERIFICATION USING CONFORMAL LEC ( CADENCE TOOL)

 
 
kitcha
Guest
Posts: n/a
 
      01-24-2006
I m working on formal verification. When i do a RTL vs Netlist
comparison i get CUT-POINTS.
How do i avoid it???

 
Reply With Quote
 
 
 
 
Mike Treseler
Guest
Posts: n/a
 
      01-24-2006
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
 
Reply With Quote
 
 
 
 
Thomas Stanka
Guest
Posts: n/a
 
      01-31-2006

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

 
Reply With Quote
 
kitcha
Guest
Posts: n/a
 
      01-31-2006
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?

 
Reply With Quote
 
Thomas Stanka
Guest
Posts: n/a
 
      02-06-2006
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

 
Reply With Quote
 
kitcha
Guest
Posts: n/a
 
      02-07-2006
finally fixed the problem..thanks thomas

 
Reply With Quote
 
 
 
Reply

Thread Tools

Posting Rules
You may not post new threads
You may not post replies
You may not post attachments
You may not edit your posts

BB code is On
Smilies are On
[IMG] code is On
HTML code is Off
Trackbacks are On
Pingbacks are On
Refbacks are Off


Similar Threads
Thread Thread Starter Forum Replies Last Post
Conformal LEC of a VHDL design (RTL Vs Netlist) sharatd VHDL 0 10-18-2006 01:57 PM
Conformal LEC of a VHDL design (RTL Vs Netlist) sharatd Hardware 0 10-18-2006 01:47 PM
How To Control The Z Modeling In Lec(formal Verification Tool)?? subhash VHDL 0 08-02-2006 02:24 PM
PSL: New 2nd Edition book: Using PSL for formal and dynamic verification ben cohen VHDL 0 01-27-2004 01:09 AM
Good websites for Formal Verification ? thewhizkid VHDL 3 10-07-2003 03:04 PM



Advertisments