英诺达亮相CCF Chip 2026大会，分享静态验证前沿方法

此次大会设置了"从约束求解到EDA形式化方法"论坛，该论坛汇聚了来自中国科学院、西北工业大学、华东师范大学等高校以及英诺达等EDA企业的多位专家学者，围绕约束求解（SAT/SMT）与EDA形式化验证的深度融合展开系统探讨，展示了学术界与产业界在EDA形式化方法领域的最新研究成果与工程实践。

探索静态验证中形式化辅助新路径

李英梦博士在报告中围绕BMC和PDR（IC3）两种主流符号模型检测技术展开。报告指出，BMC和PDR（IC3）各自针对不同的任务进行优化，英诺达在实践中探索出将这两种技术结合使用的方法，有效解决了静态检查工具产品中原本耗时较长的问题。

此外，针对传统布尔代数分析方法在复杂逻辑场景下通过构建精确模型用SAT求解时，出现的运行时间和内存占用指数增长问题，英诺达应用了一种启发式近似建模方法——通过构建与传统布尔结果高度接近的近似模型，并结合SAT求解，在满足验证准确性的同时，有效缓解了性能瓶颈，显著提升了验证效率。

这一技术思路与英诺达一贯坚持的工程化理念高度一致：让验证工具真正服务于设计团队的实际需求，在最短时间内交付可信赖的验证结果。

构建静态验证完整工具链

英诺达长期深耕静态验证领域，已构建起覆盖RTL Signoff全流程的EnAltius^®昂屹^®系列工具矩阵，包括：

•ELINT：RTL代码质量检查工具，提供语法、语义和规范检查

•ECDC：跨时钟域检查工具，近期新增跨复位域（RDC）检查功能，采用专有高精度算法，有效识别芯片设计中的潜在风险

•EDFTC：可测试性设计检查工具，确保设计在DFT部分达到交付标准

此外，英诺达还在低功耗设计领域形成了EnFortius®凝锋®系列工具，覆盖从RTL级到门级的功耗分析、优化与验证，包括“中国芯”EDA专项产品奖——低功耗设计全流程的静态检查工具ELPC等。