FORMAL VERIFICATION USING CONFORMAL LEC ( CADENCE TOOL)

[kitcha]

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

 

[Mike Treseler]

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

 

[Thomas Stanka]

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

 

[kitcha]

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?

 

[Thomas Stanka]

Hi,

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

 

[kitcha]

finally fixed the problem..thanks thomas