第六章Design Exploration 工具
Design Information
提供设计复杂度指标：
- Metrics Pane：显示寄存器数量、输入/输出数、状态空间估计
- Leveraging Metrics：利用指标识别复杂度瓶颈
Complexity Manager
帮助管理设计复杂度：
- Functional Type Icons：按功能类型（控制/数据/时钟/复位）标记模块
- 复杂度热图：可视化哪些模块最复杂
- 抽象建议：建议可以抽象或黑盒化的模块
Formal Profiler
形式分析性能分析工具：
- Use Flow：分析证明运行的时间分布
- Profiler GUI：显示哪些属性/引擎耗时最多
- 帮助优化证明策略（例如对耗时属性单独调优）
复杂度管理方法论
什么时候需要关注复杂度
不是每个设计都需要复杂度管理。以下信号出现时，说明你需要 Design Exploration 工具：
- 证明超时（time limit exceeded）且没有明确原因
- 内存爆炸（out of memory）
- 引擎无法收敛（跑了很久 still running 无进展）
- 少量属性 remaining，其他都 proven 了但这几个怎么都过不去
诊断流程
1Design Information 看规模
打开 Design Information 查看 flop 数、输入输出数、状态空间估计。如果 flop 数超过 2000，大概率需要抽象。
2Complexity Manager 找瓶颈
Complexity Manager 的热图按颜色显示模块复杂度：红色最热（最复杂）。展开最复杂的模块，判断它是否参与你要验证的属性。
3决定黑盒/抽象
不参与当前属性逻辑的复杂模块 → 黑盒化。参与但数据路径太宽 → 数据抽象。Blackbox Assistant 可以自动推荐最优黑盒策略。
4Formal Profiler 定位耗时属性
Profiler 报告显示哪些属性、哪些引擎最耗时。对最慢的属性单独调优（增加时间、换引擎、加辅助不变量）。
经验法则：复杂度控制不是一次性工作，而是迭代过程。黑盒一个模块 → 重跑 → 如果结果改善，继续优化；如果出现假反例，说明黑盒过度，回退。
来源文档
jaspergold_apps_userguide.pdf Ch.10