spyglass question on equivalence checking

[vcnvcc]

Hi friends,

I have question on equivalence checking.

1. Is equivalence checking and formal verification is same?
--I say yes, in cadence term it is equivalence checking and in synopsys term it is formal verification, am I right?

2. Is spyglass is used for equivalence checking/formal verification?
-- I dont know, if you have any idea pls share.

Thanks in advance.

 

[ritvik]

formal verification is a method of comparing a design with a model and reporting whether the design satisfies the model.
The model could be in different format (e.g. RTL, Assertions etc)
Formal verification in general terms is used when the model is assertion based.
Equivalence checking is a subset of formal verification where the model is either an RTL or netlist (Most probably generated from the reference RTL

 

[vijay.mani884]

Hi friends,

I have question on equivalence checking.

1. Is equivalence checking and formal verification is same?
--I say yes, in cadence term it is equivalence checking and in synopsys term it is formal verification, am I right?

1> yes you are right. in cadence it is also called confromal LEC(Logic Equivalence Checking)

2. Is spyglass is used for equivalence checking/formal verification?
-- I dont know, if you have any idea pls share.
2> Nope spyglass doens't perform LEC. Its just a linting tool provided by atrenta and other vendors. In implementation terms it is called PLDRC (Pre Layout Design Rule Checking)


Cheers