第六章Design Exploration 工具

Design Information

Design Information 窗口显示与 target 相关的树节点。target 可以是一个模块或实例，也可以是一个或多个 task、属性或信号；如果选中多个信号，窗口显示的是这些信号 COI 的并集。指标分为四类：

• Module Source Info：RTL 实例数、内嵌属性及其类型、代码行数
• Structural Metrics（结构指标）：设计逻辑结构方面的信息，例如寄存器、输入输出端口、门数
• Functional Metrics（功能指标）：设计的功能组件，例如计数器、有限状态机（FSM）、多维数组（含 FIFO）
• Current Task Metrics：当前 task 中的 stopat 数量

尺寸的表示约定：x(y) 中 x 是总数、y 是 bit 数之和；flop 用 x(y)(z property flop bits)，其中 z 是为 SVA 和 PSL 属性生成的 observer flop 的 bit 数之和。

Complexity Manager

Complexity Manager 显示设计统计数据，帮你了解 COI（cone of influence）并找出复杂度来源和潜在的抽象候选。它可以针对整个设计，也可以针对一个或多个属性的 COI，或一个 task 中所有属性的合并 COI。

• 统计 pane：有 nets、gates、registers 等列
• 详情 pane：包含 Signal Table 和 Functional View 两部分
• Functional Type Icons：Functional View 标签页中每个条目名称左边的图标，标示结构类型，共四种——FSM、FIFO、Multidimensional array（多维数组）、Counter（计数器）。鼠标悬停有 tooltip 说明类型

Formal Profiler

一般很难说清形式引擎为什么卡住、设计中哪些结构对引擎而言是难点。Formal Profiler 帮你理解引擎把力气花在了设计的哪些部分，从而把复杂度削减工作聚焦到那些地方。

• 它针对某一个特定属性分析形式引擎的活动，并按 bound 逐个报告引擎 B 或 M 所花的 effort。百分比数值越高，表示该引擎在这里花的力气越大
• 用得到的信息来决定：加抽象、加 helper assertion、做 reduction 等等

复杂度管理方法论

什么时候需要关注复杂度

不是每个设计都需要复杂度管理。以下信号出现时，说明你需要 Design Exploration 工具：

• 证明超时（time limit exceeded）且没有明确原因
• 内存爆炸（out of memory）
• 引擎无法收敛（跑了很久 still running 无进展）
• 少量属性 remaining，其他都 proven 了但这几个怎么都过不去

诊断流程