Formality：比较点的验证状态和整体验证状态

相关阅读Formalityhttps://blog.csdn.net/weixin_45791458/category_12841971.html?spm1001.2014.3001.5482比较点的验证状态在使用verify命令进行验证后参考设计和实现设计所有匹配的比较点如果使用特定选项也可以验证任意两个比较点会各自进行验证每对比较点的结果如下所示。状态描述Passing表示一对比较点通过了验证即意味着Formality确定这两个比较点所属的逻辑锥是功能等价的。Failing表示一对比较点验证失败即意味着Formality认为这两个比较点所属的逻辑锥是不功能等价的。Aborted表示Formality未能将比较点判定为通过或不通过原因可能是存在Formality无法自动打破的组合循环或者比较点难以验证。Unverified表示未验证的比较点未验证的比较点发生在验证过程时当达到失败点个数限制由变量verification_failing_point_limit控制默认为20个、超出时间限制由变量verification_timeout_limit控制默认为36小时或用户主动CtrlC时停止验证。Not Compared由于常量触发器、用户设置或不可读等原因Formality不对这些比较点进行验证。Passing使用report_passing_points命令或者如图1所示在Debug窗口点击Passing Points即可查看所有通过验证的比较点。图1 查看通过的比较点Failing使用report_failing_points命令或者如图2所示在Debug窗口点击Failing Points即可查看所有验证失败的比较点。图2 查看不通过的比较点Aborted使用report_aborted_points命令或者如图3所示在Debug窗口点击Failing Points即可查看所有中止的比较点。图3 查看中止的比较点Unverified使用report_unverified_points命令或者如图4所示在Debug窗口点击Unverified Points即可查看所有未验证的比较点。图4 查看未验证的比较点Not Compared如果使用set_dont_verify命令设置一对比较点不验证则Formality不对这些比较点进行验证使用report_dont_verify_points命令进行报告。如果一对比较点的值为相同的常量则Formality不对这些比较点进行验证。如果一对比较点中存在至少一个不可读的比较点则Formality默认不对这些比较点进行验证可通过verification_verify_unread_compare_points变量改变。使用report_not_compared_points命令可以报告上面三种不验证的情况。整体验证状态Succeeded所有的比较点都通过了验证实现设计被确定为在功能上等价于参考设计。FailedFormality找到了至少一对失败的比较点实现设计被确定为在功能上不等价于参考设计。如果验证被中断例如因为失败点限制、超出时间限制或用户主动CtrlC停止验证并且在中断之前至少检测到一个失败点Formality会报告验证结果为失败。InconclusiveFormality无法确定参考设计和实现设计是否等价这种情况在以下情况中可能发生1、所有比较点验证完成但比较点过于复杂无法验证导致出现中止的比较点并且在设计的其他部分没有发现失败点。2、验证被中断例如因为失败点限制、超出时间限制或用户主动CtrlC停止验证并且在中断之前没有检测到失败点。Not Run因为一些问题或错误Formality没有进行任何比较点的验证一个例子是使用set_dont_verify_points命令设置所有比较点不验证后使用verify命令还有一个例子是当设计中不存在Unverified或Aborted状态的比较点即已全部归类为Passing、Failing或Not Compared状态时使用verify命令此时还会出现FM-397错误。