LEC Vulnerability on Constant Propagation

摘要

LEC is the most widely used tool for formal equivalence verification and ECO generation, but there are gaps in modeling of constant in LEC which can lead to silicon bugs even though the verification has passed. This issue is observed in designs which have gone through ECO’s. This paper covers scenarios where there are potential bugs masked by LEC/ECO due to this limitation and proposes a methodology to mitigate it.