Formality：组合逻辑环的处理

相关阅读

Formalityhttps://blog.csdn.net/weixin_45791458/category_12841971.html?spm=1001.2014.3001.5482

目录

组合逻辑环的断开

高亮组合逻辑环

仅显示组合逻辑环

组合逻辑环的断开

Formality：匹配(match)是如何进行的？一文中谈到，组合逻辑环会被Formality识别为被识别为Loop，并成为一个新的比较点，本文将详细讨论关于组合逻辑环的处理细节。

默认情况下，Formality会自动断开组合逻辑环并在preverify阶段Building verification models时提示"Info: 1 (1) cycles broken in reference (implementation) design; see formality.log for list."，用户还可以使用report_loops命令进行报告。

组合逻辑环的自动断开由verification_auto_loop_break变量（默认值为true）控制，该功能的处理方式非常保守。如果两个组合逻辑环之间存在任何结构差异，Formality就会放弃自动断开组合逻辑环，转而执行功能更强大、但也更加复杂的环路分析，并在验证时提示"Info: Unrolled Combinational Loop(s) in Reference/Implementation design."

有些情况下，组合逻辑环甚至能导致比较点的验证状态出现Aborted，具体可参考下面的博客。

Formality：比较点的验证状态和整体验证状态https://blog.csdn.net/weixin_45791458/article/details/145133977?ops_request_misc=elastic_search_misc&request_id=85cb4e5a80db1285a314908c702083b4&biz_id=0&utm_medium=distribute.pc_search_result.none-task-blog-2~all~ElasticSearch~search_v2-3-145133977-null-null.541^v3^pc_search_result_blog1&utm_term=Loop&spm=1018.2226.3001.4450后面两节将展示如何在逻辑锥视图中高亮和查看组合逻辑环。在此之前，用户需要在match、verify或debug界面点击Get Loop Data按钮，如图1到图3所示。

图1 match界面

图2 verify界面

图3 debug界面

在点击Get Loop Data按钮后，用户可以在Loops选项卡下查看组合逻辑环及其是否被断开（即创建Loop比较点），如图4所示。

图4 查看Loop报告

高亮组合逻辑环

在逻辑锥视图中，点击Edit -> Highlight Loops或右键并点击Highlight Loops即可让组合逻辑环高亮紫色显示，如图5所示。

图5 高亮显示组合逻辑环

仅显示组合逻辑环

在逻辑锥视图中，点击Edit -> Prune/Restore -> Isolate Loops或右键并点击Prune/Restore -> Isolate Loops即可仅显示组合逻辑环，如图6所示。

图6 仅显示组合逻辑环