formal验证是什么使用数学证明不靠仿真激励穷尽合法输入空间来证明属性 (Assertion) 永远成立。formal验证的优势是什么用来弥补仿真覆盖率缺口。什么样的场景适合用formal验证适合数据通路协议 FSM 状态机、控制逻辑、仲裁器、队列、握手协议 (AXI/APB)、计数器、数据校验、状态跳转、安全逻辑、复位逻辑中等规模模块建议模块层级不要直接丢整个 SoC大模块做切分分块 Formal把 RAM/ROM 做抽象模型。用formal验证有哪些注意的地方三种A要怎么写。assume假设约束输入告诉工具哪些输入是合法的不会去验证 assume约束输入空间。assert断言需要工具必须证明永远成立失败给出反例波形。坏事情一定不能发生safety好事情必然发生liveness。cover覆盖点证明存在某种场景可以发生看场景可达性关心的场景一定会发生。将SVA与RTL联系起来有哪两种方式1.bind方式。bind dut_module dut_sva u_dut_sva(.*);优势不污染rtl运行。可以复用sva文件。2.include方式。DUT 内部直接 include SVA不推荐污染 RTL 代码。formal验证环境的准备步骤。1.待测的rtl以及周围隔离的抽象model裁剪无关的逻辑。2.编写sva属性库。assume/assert/cover。assume做合法性约束。约束时序复位合法取值握手时序协议规则等。3.formal验证环境列表和编译配置文件列表包含DUT RTLSVA property 文件.sv包含 assume/assert/cover抽象模型 abs modelFormal 专用编译指令排除仿真代码jaspergold指令blackbox黑盒某些子模块不展开内部状态抑制状态爆炸abstract对存储、寄存器做抽象cutpoint切断部分信号传播边界做边界抽象bound设置证明深度有界模型检查 BMCBMC有界模型检查只证明 N 个时钟周期内属性成立 Prove无界证明证明永远成立算力消耗远大于 BMC。formal环境运行结果有哪些怎么分析proved属性被证明永远成立。Falsified找到反例 Counterexample工具输出波形复现 bug看波形来区分是 RTL bug还是 assume 写的不合理还是 assert 写的不对。修改 RTL / 修改 SVA 属性重新跑 prove。Undetermined状态爆炸算力耗尽无法得出结论需要做抽象、cutpoint、分块。Vacuous空洞 passassume 约束太强条件永远不会触发assert 空洞通过伪通过高危坑。空洞检查是 Formal 环境必做检查一定要看 cover 点是否可达。formal验证如何sign-off所有关键 Safety 属性 Proved关键 Cover 点全部可达无大量 vacuous 空洞Undetermined 的属性做抽象优化或者退而求其次 BMC 有界证明输出 Formal 报告记录 cutpoint、blackbox、抽象假设。formal验证过程中有哪些坑?1.Assume约束错误, 过度约束屏蔽 bugassert 全部 pass实际 RTL 有 bug。用 cover 点校验场景可达性达到双重保障。2.Vacuous 空洞通过条件永远不成立断言 “假的成立”。工具一般有选项打开空洞报告。3.状态爆炸 State Explosion。大 FIFO、RAM、大量寄存器、复杂乘法状态空间爆炸全部 Undetermined。模块切分分块 FormalRAM 抽象、blackboxcutpoint 切断信号路径使用 BMC 有界证明替代无界 prove4.复位处理不当SVA 必须加disable iff(!rst_n)否则复位阶段报虚假 falsified5.Liveness 活性属性证明失败。活性属性证明开销高很多时候需要额外 fairness assume公平假设比如输入不会永远 hold valid。6.仿真与 Formal 两套 SVA维护成本高。使用同一套 SVA既可以 UVM 仿真跑断言也可以 Formal 证明。7.Formal 报反例是不是一定 RTL 有 bug仅说明在当前 assume 约束集合下property 不成立。排查顺序反例的输入激励现实不会出现 →assume 约束问题激励合法RTL 行为符合 spec但断言报错 →property 属性 bug激励合法RTL 行为违反 spec →RTL bug配合jaspergold使用使用visualize打开 counterexample 波形重点看输入信号、property 内部子表达式哪里不满足。可以临时 disable 这条 assert单独检查中间信号行为看 DUT 实际输出是否符合 spec。将 counterexample 导出激励在仿真环境回放如果仿真同样报错大概率 RTL 问题仿真跑出来正常大概率 formal 约束 /property 问题。formal验证举例最近想总结一下看过的代码如有错误欢迎指正。我们从top文件开始看起。top module里总是有dut的例化以及dut和env的连接. 这点跟simulation验证平台一样。formal验证平台的pkg.sv文件包着所有的有关enum和type的定义也可以被其他文件以import pkg::*的方式使用simulation的验证平台是包了所有的验证平台下的文件以及引用的文件使用方式相同。formal验证平台的env里有clockreset的处理以及做的假设assume)interface的例化。agent和scoreboard的例化做补充检查。自己写的做逻辑判断的cover propertyassert property, assume property。设计数据流动的文件 master agent来驱动数据流到interfaceslave agent来监控interface的数据流。agent是经过vip例化出来的。parameter确定好后被放在define文件里。编辑japergold 适用的tcl文件里面有一些常规命令还有自己添加的assume假设assert和 cover应该也可以)。最后由makefile来确定整个验证平台怎么跑。确定好工作路径之后首先vcs编译pass。其次启动jaspergold运行命令。jg -fpv *.tcl这是一个仅用sv搭建的环境还没见过uvm的formal验证环境有机会补充一下。此环境是使用Cadence JasperGold工具来做formal验证也可以使用Synopsys VC‑Formal来做验证。
formal 验证
formal验证是什么使用数学证明不靠仿真激励穷尽合法输入空间来证明属性 (Assertion) 永远成立。formal验证的优势是什么用来弥补仿真覆盖率缺口。什么样的场景适合用formal验证适合数据通路协议 FSM 状态机、控制逻辑、仲裁器、队列、握手协议 (AXI/APB)、计数器、数据校验、状态跳转、安全逻辑、复位逻辑中等规模模块建议模块层级不要直接丢整个 SoC大模块做切分分块 Formal把 RAM/ROM 做抽象模型。用formal验证有哪些注意的地方三种A要怎么写。assume假设约束输入告诉工具哪些输入是合法的不会去验证 assume约束输入空间。assert断言需要工具必须证明永远成立失败给出反例波形。坏事情一定不能发生safety好事情必然发生liveness。cover覆盖点证明存在某种场景可以发生看场景可达性关心的场景一定会发生。将SVA与RTL联系起来有哪两种方式1.bind方式。bind dut_module dut_sva u_dut_sva(.*);优势不污染rtl运行。可以复用sva文件。2.include方式。DUT 内部直接 include SVA不推荐污染 RTL 代码。formal验证环境的准备步骤。1.待测的rtl以及周围隔离的抽象model裁剪无关的逻辑。2.编写sva属性库。assume/assert/cover。assume做合法性约束。约束时序复位合法取值握手时序协议规则等。3.formal验证环境列表和编译配置文件列表包含DUT RTLSVA property 文件.sv包含 assume/assert/cover抽象模型 abs modelFormal 专用编译指令排除仿真代码jaspergold指令blackbox黑盒某些子模块不展开内部状态抑制状态爆炸abstract对存储、寄存器做抽象cutpoint切断部分信号传播边界做边界抽象bound设置证明深度有界模型检查 BMCBMC有界模型检查只证明 N 个时钟周期内属性成立 Prove无界证明证明永远成立算力消耗远大于 BMC。formal环境运行结果有哪些怎么分析proved属性被证明永远成立。Falsified找到反例 Counterexample工具输出波形复现 bug看波形来区分是 RTL bug还是 assume 写的不合理还是 assert 写的不对。修改 RTL / 修改 SVA 属性重新跑 prove。Undetermined状态爆炸算力耗尽无法得出结论需要做抽象、cutpoint、分块。Vacuous空洞 passassume 约束太强条件永远不会触发assert 空洞通过伪通过高危坑。空洞检查是 Formal 环境必做检查一定要看 cover 点是否可达。formal验证如何sign-off所有关键 Safety 属性 Proved关键 Cover 点全部可达无大量 vacuous 空洞Undetermined 的属性做抽象优化或者退而求其次 BMC 有界证明输出 Formal 报告记录 cutpoint、blackbox、抽象假设。formal验证过程中有哪些坑?1.Assume约束错误, 过度约束屏蔽 bugassert 全部 pass实际 RTL 有 bug。用 cover 点校验场景可达性达到双重保障。2.Vacuous 空洞通过条件永远不成立断言 “假的成立”。工具一般有选项打开空洞报告。3.状态爆炸 State Explosion。大 FIFO、RAM、大量寄存器、复杂乘法状态空间爆炸全部 Undetermined。模块切分分块 FormalRAM 抽象、blackboxcutpoint 切断信号路径使用 BMC 有界证明替代无界 prove4.复位处理不当SVA 必须加disable iff(!rst_n)否则复位阶段报虚假 falsified5.Liveness 活性属性证明失败。活性属性证明开销高很多时候需要额外 fairness assume公平假设比如输入不会永远 hold valid。6.仿真与 Formal 两套 SVA维护成本高。使用同一套 SVA既可以 UVM 仿真跑断言也可以 Formal 证明。7.Formal 报反例是不是一定 RTL 有 bug仅说明在当前 assume 约束集合下property 不成立。排查顺序反例的输入激励现实不会出现 →assume 约束问题激励合法RTL 行为符合 spec但断言报错 →property 属性 bug激励合法RTL 行为违反 spec →RTL bug配合jaspergold使用使用visualize打开 counterexample 波形重点看输入信号、property 内部子表达式哪里不满足。可以临时 disable 这条 assert单独检查中间信号行为看 DUT 实际输出是否符合 spec。将 counterexample 导出激励在仿真环境回放如果仿真同样报错大概率 RTL 问题仿真跑出来正常大概率 formal 约束 /property 问题。formal验证举例最近想总结一下看过的代码如有错误欢迎指正。我们从top文件开始看起。top module里总是有dut的例化以及dut和env的连接. 这点跟simulation验证平台一样。formal验证平台的pkg.sv文件包着所有的有关enum和type的定义也可以被其他文件以import pkg::*的方式使用simulation的验证平台是包了所有的验证平台下的文件以及引用的文件使用方式相同。formal验证平台的env里有clockreset的处理以及做的假设assume)interface的例化。agent和scoreboard的例化做补充检查。自己写的做逻辑判断的cover propertyassert property, assume property。设计数据流动的文件 master agent来驱动数据流到interfaceslave agent来监控interface的数据流。agent是经过vip例化出来的。parameter确定好后被放在define文件里。编辑japergold 适用的tcl文件里面有一些常规命令还有自己添加的assume假设assert和 cover应该也可以)。最后由makefile来确定整个验证平台怎么跑。确定好工作路径之后首先vcs编译pass。其次启动jaspergold运行命令。jg -fpv *.tcl这是一个仅用sv搭建的环境还没见过uvm的formal验证环境有机会补充一下。此环境是使用Cadence JasperGold工具来做formal验证也可以使用Synopsys VC‑Formal来做验证。