“三个女巫” —— 避免 CDC 路径上的毛刺噩梦

形式化毛刺检测的优点

我们说明了各种类型 CDC 路径中的毛刺问题，然后概述一种基于形式化的自动毛刺检测方法2。该方法利用结构 CDC 分析、表达式分析和形式化方法来消除和证明设计中的真正毛刺。为了处理运行时间更长、更复杂的设计，我们将先前的方法分解为一个更灵活的层次化、多阶段和多处理流程。本文说明了该流程的各个阶段以及如何实现并行处理。

利用层次化多阶段和多处理，用户可以比以前更高效地执行门级 CDC 和毛刺分析。通过将 RTL 指令和豁免变换到门级，已经在 RTL 完成的艰巨工作可以得到重复利用，而无需重复执行。

这种多阶段、门级 CDC 和毛刺分析方法具有许多优点：

高质量的结果 基于形式化的毛刺验证方法产生的结果噪声更小，质量更高（数千条路径只有几个毛刺），因此调试和分类工作量显著减少。

易于调试 利用表达式分析和形式化方法，该工具可以识别导致毛刺场景的确切路径，并可以查明可能产生潜在毛刺的收敛点。

能够处理大型 SoC 可以采用层次化方法首先完成对 IP 模块的 CDC 和毛刺分析。IP 模块随后表示为灰盒，以便在顶层进行分析。

快速改进 多阶段门级 CDC 和毛刺分析过程支持逐步的改进，大幅缩短周转时间，并消除了单一过程中的故障。

多处理 由于毛刺分析可以在多台服务器上并行执行，因此可以更高效地利用服务器和内存。