用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。
当然有一种折中的signoff LEC方案，如下图，分成两步分别做LEC，第一步New RTL vs New Syn，是一定PASS的，这是综合工具自己跑出来的结果；第二步，做New Syn vs APR ECO Netlist，这一步的优势是没有RTL，只是网表与网表的差异，这一步看似降低了Formality做LEC的难度，但因为没有合适的svf来指导，Formality也经常会Fail。
为了解决这一难题，在最新版的GOF中（NanDigits GOF 10.10正式发布，指导formality过signoff LEC），NanDigits利用GOF自身LEC引擎的算法优势，支持写出各种优化后的正确的mapping关系，包括dff phase inversion、跨层次的寄存器merge，手工ECO中的寄存器改名等关键信息。在Formality中，直接source GOF输出的config文件，即可快速速得到“Verification SUCCESSED”。
举个例子，具体使用方法如下：
# ...run_lec();write_compare_points("gof_compare_points.rpt");write_formality_help_files("fm_20240103");
这一步，支持任何工具产生的ECO网表，包括cadence conformal eco、手工eco。NanDigits GOF只是输出两个网表的差异。
在Formality的脚本中：
read_db ...read_verilog -r -05 { resyn.v }set_top r:/WORK/topread_verilog -i -05 { eco.v }set_top i:/WORK/top# bypass dft and others settings# source help file from gofsource -echo -verbose fm_20240103.config.tclmatchverify
关于NanDigits Design Automation
Nandigits Design Automation于2007年成立，公司总部位于美国硅谷圣何塞（San Jose）。2016年10月在中国大陆成立销售和技术支持部门。我们是完整的芯片网表解决方案提供商，主要产品有网表功能ECO工具GOF ECO、逻辑等价性检查工具GOF LEC，网表调试工具GOF Debug、汽车电子功能安全验证的GOF Formal。到目前，我们已经帮助全球数十家芯片设计公司Tapeout超过100个项目。
欢迎评估试用
中国大陆
技术支持：support@nandigits.cn
美国总部
技术支持：support@nandigits.co
欢迎联系评估和试用：https://nandigits.cn/license/getlic.php。
