Question about Conformal Logic Equivalency Check

[andy_freak]

Hello,

I have recently started working on Logic Equivalency Check. I am using Conformal. I have some questions regarding it.

What does it mean when they say "mapping key points". I understand the term key points, but am confused what they mean when they say mapping key points.

What are mapped and unmapped points.

Can somebody explain briefly the exact flow, what conformal does starting with the files it takes in. (RTL, netlist and cell library).

Thanks in advance.

Andy

 

[Adam.Yakuvitz]

hi Andy,
if you want to get kickstarted on the Conformal Equivalency Checking, Cadence has created a series of online training classes for their front-end tools . . .

http://trainingondemand.cadence.com

You'll need Cadence Online Support (COS/Sourcelink) access to get into the site. i'm a CAD guy at a large company and a lot of users use this get kickstarted back on LEC.

-- ay

 

[lostinxlation]

Formal verifier maps the node in golden to the node in revised. The mapped point is what formal verifier thinks is logically corresponding point from golden and revised. Mostly, key points are sequential cells, input, and output. It checks the logic equivalency on the path starting at some key points and ending at some key points.

If it reports unmapped points, the tool couldn't determine the mappings. Typical example is there is some logic inferring a flop in RTL, but synthesis tool deletes it because it finds the flop redundant. This flop will be categorized as unmapped, beause it exists in RTL, but not in netlist.

 

[andy_freak]

Thanks a lot guys for your response.