EEPW论坛

据日前参与设计自动化大会(DAC)小组讨论的人士称，形式验证对仿真是非常有价值的补充，但无法替代后者。来自IBM和英特尔的用户代表对此看法强烈表示有保留意见，而EDA公司的代表看起来更为赞成这一观点。 加州大学教授兼主持人Rajesh Gupta向与会者提出以下问题：是否形式验证缩减了对仿真的需求？形式工具如何适应验证策略？投资回报是什么？他指出每季度收入达9000万美元的仿真市场远远大于收入仅为1310万美元的形式验证市场。 英特尔高级工程师John O'Leary表示，形式验证有两大可能的应用领域，即发现RTL代码的错误，并确保流片前的零错误率。他表示：“我无法肯定是否将放弃仿真，因为我不知道是否有更好的方法用于在RTL中发现早期错误。形式验证有容量限制，发现不了所有的问题。” O'Leary指出，但形式工具能发现仿真器遗漏的错误。为了成功使用形式工具，设计师需要选择合适的问题，定义清晰的规格，明确何种形式工具最适合等效校验、模型校验、符号仿真和理论证明。IBM公司T.J. Watson研究部高级资深人士Daniel Beece表示：“仿真一直以来也将永远是我们最重要的验证工具，等效校验和用于测试覆盖的半形式方法重要性分列其后。”