What is Equivalence Checking?

[kukurigu]

Hello designers!

Could you tell me:
What is Equivalence Checking?
I know only that Cadence (Verplex) Conformal handles this task.

 

[saho]

equivalence checking <=> model checking.

it finds its application in comparing RTL vs RTL, RTL vs gate, gate vs gate after design changes (or more kinkily known as ECO, engineering change order). It helps designers by ensuring a minor design changes do not modify other modules's functionality. Ok, the alternative route is to run gate level simulation which detects discrepancies between pre-translated RTL and synthesised code/post place & route design code.

However, gate level is very time hungry. So, use formal equivalence checking. These formal tools are still infancy though, still requires user intervention some time in order to resolve warnings produced by the tool.

It uses the concept --logical cone as point of comparison. To find out more, perform google search. I have given you some background
as what is a formal equivalence checking and its benefits.


Tools commercially available:

mentor graphics - formalpro
synopsys - formality
prover technology (swedish start-up) - echeck
cadence (verplex) - conformal


Of course, formal verification covers 2 areas:

1. model checking/equivalence checking

2. property checking, where verification of design is aided by describing the signals behaviour along the time scale using some smart syntax. Notably SUGAR from IBM (Haifa, Israel), and now adopted as Property Specification Language, runned by Accellera committee. Currently, the LRM version is 1.10. Look for Accellera for more details.

 

[saho]

in addition to the above posting, please visit the site




It is about Writing Testbenches: HDL verification by Janick Bergeron.

In this post, there are materials on verification tools. I think it could be more precise than my descripton give above.


happy learning.

 

[gerade]

Hi,

addtion to saho,

after synthesis and layout, we can compare the equivalence between netlist and RTL. this will save simulation runtime dramatically. Usually it will take less than several hours, this can prevent wasting time to do the endless gatelevel simulation, especail for the huge designs.

regards

 

[zwj_seu]

Hi
I think is compare the RTL code and the layout circuit netlist.It's good for crack!

 

[yeewang]

equivalece checking can check the equivalence of every representation of your design, either RTL or netlist or even layout annotation.

 

[wadaye]

Hello designers!

Could you tell me:
What is Equivalence Checking?
I know only that Cadence (Verplex) Conformal handles this task.

Hi kukurigu:

I think what you mean is FORMAL check!

You will find it is very useful when you compare your RTL

code/Synthesis netlist/netlist after scan/netlist after ECO. But with LEC,

you can only compare the RTL code with netlist, if you wanna do other

level formal check you need to use LTX--another tool from verplex(now

cadence).

wang1

 

[tom123]

Equivalence Checking is verifying that different design file

has same logic function. it use mathematical principle

to do this, called BBD.

Hello designers!

Could you tell me:
What is Equivalence Checking?
I know only that Cadence (Verplex) Conformal handles this task.

 

[srik_naidu]

hi,
Its application is by comparing RTL vs RTL, RTL vs gate, gate vs gate after design changes.
it is helpful to find the synthesis tool problems.

with regards,
srik.

 

[spauls]

now a daya formal verificaiton is togher as many designs use IP and it is difficult ot change IP at RTL level,