K
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???
comparison i get CUT-POINTS.
How do i avoid it???
Navigation
Install the app
How to install the app on iOS
Follow along with the video below to see how to install our site as a web app on your home screen.
Note: This feature may not be available in some browsers.
More options
You are using an out of date browser. It may not display this or other websites correctly.
You should upgrade or use an alternative browser.
You should upgrade or use an alternative browser.
M
Mike Treseler
Guest
kitcha wrote:
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
You could use a functional rather thanI m working on formal verification. When i do a RTL vs Netlist
comparison i get CUT-POINTS.
How do i avoid it???
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
T
Thomas Stanka
Guest
kitcha schrieb:
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
Maybe you should ask, why the tool inserted cutpoints.I m working on formal verification. When i do a RTL vs Netlist
comparison i get CUT-POINTS.
How do i avoid it???
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
K
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?
points..but on the netlist side i m not able to find any loops...what
is the possible solution for this?
T
Thomas Stanka
Guest
Hi,
kitcha schrieb:
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 schrieb:
You say you have combinatorial feedbackloops in RTL, which you don'tthomas..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?
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
K
kitcha
Guest
finally fixed the problem..thanks thomas