equivalent verilog gate level netlists?

[kris]

Hi

How do you check if 2 verilog gate level netlists are equivalent?

That is if I insert buffers (e.g. clock buffers) the functionality does not
change.

Is there any program to do this?

Kris

 

[Eyck Jentzsch]

kris wrote:

Hi

How do you check if 2 verilog gate level netlists are equivalent?

That is if I insert buffers (e.g. clock buffers) the functionality does not
change.

Is there any program to do this?

Kris



There are tools out there called Equivalence checker e.g. Verplex LEC

(now Cadence), Formality (Synopsys) and even more (try google or similar).

-Eyck

 

[Paddy McCarthy]

kris wrote:

Hi

How do you check if 2 verilog gate level netlists are equivalent?

That is if I insert buffers (e.g. clock buffers) the functionality does not
change.

Is there any program to do this?

Kris

If you can program, and have say the following restrictions on the

netlists that
you are comparing:
* flat, gate level, machine generated (regular), netlist.
* Same gate library for both netlists.

You could write a prog to read in and store each netlist, then compare
and discard nets with similar pinouts, then gates with similar net fanouts.
With information on what buffers and inverters are in you library you
could then apply this to the remaining netlist to compute boolean
equivalent nets/comps and discard them if any of their equivalents were
previously discarded.

I've done similar in the past (in awk, it was some time ago), it took
half a week, and should be simpler now if you program in a language that
makes the internal data structure manipulation easy. (Python maybe,
or Perl if you already know perl).
If choosing between using a good scripting language or
Perl/Python/Ruby/Skill then I'd use the scripting language for faster
development and easier maintenance (perl, hmmm .

If you have more flexible input netlist structure then it may be best to
buy a tool.

Rgds, Paddy.