用Formality做大规模设计的RTL vs APR ECO网表的signoff等价性检查通常难度很大。即使有svf的帮助也会经常不过，因为这时我们一共有两到三个svf：老RTL综合的svf，新RTL综合的svf，后端icc2优化产生svf（如果用icc2做后端实现），还有新旧两版rtl diff差异的svf。这些svf同时被读进formality后，有些accept，有些reject，这些reject通常很难一条一条的拿出来review为什么会被reject。另一方面，由于dft、（icc2以外的）后端工具优化、自动或者手工eco等都会导致formality不能正确mapping。

形式化验证是一种基于数学分析方法的验证技术，它通过算法引擎建立模型，对待测设计的状态空间进行穷尽分析的验证。在芯片设计中，形式化验证主要用于综合前后的等价性检查和RTL设计的功能验证。形式化验证的优势在于它可以提供精确、确定的结论，帮助开发人员减少迭代设计和测试的时间和成本 。