How to perform equivalence checking between RTL and gate-level netlist?

HI friends

I want to ask you how do you perform equivalence checking between RTL and gate-level netlist? If the design is large (thousands of gates), how do you divide and conquer the equivalence checking problem? Do you perform equivalence checking on module by module basis or are there other efficient ways of doing it?

Please explain your approach especially if you are working in the industry.

Thanks and let me know if there are further questions

Re: equivalence checking between RTL and gate-level netlist

which tool are you planning to use?

If you have larger design. I recommend you to divide the design into few blocks(not too many) and run LEC on it.It would be a lot easier to debug.
try to use scripts

Re: equivalence checking between RTL and gate-level netlist

Storm_1592

I have both cadence conformal and synopsys formality tools.

Please elaborate the term blocks. I have modules in my design. should i treat each module as a block or what?

- - - Updated - - -

Storm_1592

I have both cadence conformal and synopsys formality tools.

Please elaborate the term blocks. I have modules in my design. should i treat each module as a block or what?

Re: equivalence checking between RTL and gate-level netlist

I work (in the industry) with cadence conformal. I had it working on blocks with over 100,000 flops. It should have no significant problem working on large designs, though the LEC run for them can take between several hour to several days.
You can either do a "flat" LEC run which first fully synthesize the design, map it and then compare. Or hierarchical run which compares separately modules and then can copy them to other and save time.
If your design is very large you can thing about diving it to sub design or do hierarchical run.

Re: equivalence checking between RTL and gate-level netlist

@tariq786
"should i treat each module as a block or what?"

Block as in you can divide your design hierarchially into few blocks.

Find the image for example -

Choose "A" as Top along with its submodules associated as a single block.
and do an LEC on it. I hope you got this.

Re: equivalence checking between RTL and gate-level netlist

storm_1592 said:

@tariq786
"should i treat each module as a block or what?"

Block as in you can divide your design hierarchially into few blocks.

Find the image for example -

Choose "A" as Top along with its submodules associated as a single block.
and do an LEC on it. I hope you got this.

Click to expand...

Dude Where is the image? Please post and explain in detail.

Thanks a lot again

Re: equivalence checking between RTL and gate-level netlist

tariq786 said:

HI friends

I want to ask you how do you perform equivalence checking between RTL and gate-level netlist? If the design is large (thousands of gates), how do you divide and conquer the equivalence checking problem? Do you perform equivalence checking on module by module basis or are there other efficient ways of doing it?

Please explain your approach especially if you are working in the industry.

Thanks and let me know if there are further questions

Click to expand...

Ya ,you can consider each block.Its the most efficient way to perform LEC.

If you check module by module, then it becomes simpler and In LEC our main motive is that to check Whether the flip flops and latches we had made in RTL are required or some extra flops and latches are added which are not required there.Then if this thing is checked module by module then whole process becomes simpler.

in other terms LEC is used to check whether synthesized design(at gate level) which will further go in back-end is according to specification which were written in form of RTL, if we find any mismatch then its clear the RTL logic we had written is not fully according to specification.

You can use cadence conformal.


Regards
Amit

Re: equivalence checking between RTL and gate-level netlist

give me Synopsys formality manual & how to use tis tool for LEC.