Formality：比较点的验证状态和整体验证状态
相关阅读
Formalityhttps://blog.csdn.net/weixin_45791458/category_12841971.html?spm=1001.2014.3001.5482
比较点的验证状态
在使用verify命令进行验证后，参考设计和实现设计所有匹配的比较点（如果使用特定选项，也可以验证任意两个比较点）会各自进行验证，每对比较点的结果如下所示。
| 状态 | 描述 |
| Passing | 表示一对比较点通过了验证，即意味着Formality确定这两个比较点所属的逻辑锥是功能等价的。 |
| Failing | 表示一对比较点验证失败，即意味着Formality认为这两个比较点所属的逻辑锥是不功能等价的。 |
| Aborted | 表示Formality未能将比较点判定为通过或不通过，原因可能是存在Formality无法自动打破的组合循环，或者比较点难以验证。 |
| Unverified | 表示未验证的比较点，未验证的比较点发生在验证过程时当达到失败点个数限制（由变量verification_failing_point_limit控制，默认为20个）、超出时间限制（由变量verification_timeout_limit控制，默认为36小时）或用户主动Ctrl+C时停止验证。 |
| 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
所有的比较点都通过了验证，实现设计被确定为在功能上等价于参考设计。
Failed
Formality找到了至少一对失败的比较点，实现设计被确定为在功能上不等价于参考设计。如果验证被中断，例如因为失败点限制、超出时间限制或用户主动Ctrl+C停止验证，并且在中断之前至少检测到一个失败点，Formality会报告验证结果为失败。
Inconclusive
Formality无法确定参考设计和实现设计是否等价，这种情况在以下情况中可能发生：
1、所有比较点验证完成，但比较点过于复杂，无法验证，导致出现中止的比较点，并且在设计的其他部分没有发现失败点。
2、验证被中断，例如因为失败点限制、超出时间限制或用户主动Ctrl+C停止验证，并且在中断之前没有检测到失败点。
Not Run
因为一些问题或错误，Formality没有进行任何比较点的验证，一个例子是使用set_dont_verify_points命令设置所有比较点不验证后使用verify命令；还有一个例子是当设计中不存在Unverified或Aborted状态的比较点（即已全部归类为Passing、Failing或Not Compared状态）时使用verify命令，此时还会出现FM-397错误。