如今，降低功耗已成为IC设计的主要目标之一，而CMOS IC消耗的功耗主要有两个组成部分：由亚阈值导电引起的漏电流功耗和晶体管开关过程引起的动态功耗。其中，为了最大限度降低动态功耗，我们SoC设计引入了时钟门控，然而，另一方面，这也大大增加了对传统验证方法的挑战，从以下就能看出。

时钟门控逻辑可以通过工具自动插入或设计师人为插入：

• 时钟门控逻辑可以通过综合工具自动插入RTL代码；

• 时钟门控逻辑可以通过时钟门控工具自动插入RTL；

• 时钟门控逻辑，也可以通过设计师人为插入（通常作为模块级时钟门控）。

设计中会有大量的时钟门控单元，而要验证这些时钟门控逻辑的正确性，在仿真中实现全面覆盖（test case 遍历所有的时钟门控单元）和自动检查，是一个巨大的挑战。

解决方案

解决问题前，先附上时钟门控的结构，也是我们要验证的DUT，因为时钟门控的原理并非本文中心，读者可先自己查阅相关资料：

言归正传，为了应对这一验证方面挑战，我们结合仿真、结构分析和形式验证，创建了一个系统的验证时钟门控的方法。我们的方法的主要思想是生成针对每一个使用门控时钟触发低层次的形式验证，这减少了对每一个形式属性（property）的影响，而这些形式属性都是形式验证工具必须处理的，因此增加了在适当时间内证明或者反证的可能性。

我们创作的脚本也是核心：脚本通过形式验证工具的API接口，分析RTL设计时钟门控单元格的逻辑，并自动提取属性。首先，检查时钟门控单元与仪器功能覆盖特性，这些属性的形式证明可以确保没有明显的设计错误存在。当然，相同的覆盖性质，也可以在仿真中使用。第二，对于每个时钟门控，我们的脚本会分析时钟树，报告这个时钟门控负载的触发器数量。第三，我们的脚本会综合分析被gated的触发器的源头和目的地。对于每一个时钟门控单元，该脚本都会在时钟树中提取扇入和扇出，并自动产生可用于检查错误情况的属性。

软件控制的时钟门控形式验证

时钟要求

我们的SoC的各个子系统有一个共同的微架构如下图 时钟和复位发生器（亦称CLKGEN）是分开的核心逻辑。我们的低功耗设计方法要求所有的保持触发器时钟在进入保持状态前置为低电平。只要时钟使能信号被驱动为低，所述时钟门控单元输出信号保证为低。

然而，在现实中这个时钟要求给验证工作带来了很大的负担，由软件控制的使能信号往往不能直接驱动使能信号。验证这一点，所面临的挑战是多方面的：

• 一旦时钟使能位被软件置为0，计数器逻辑被添加以保持时钟继续运行一个周期。

• 许多设计模块可以有自己的时钟分频器和或时钟门控逻辑。

• 这些要求可以适用于需要不同复位要求的子系统。

• 每个子系统可以衍生出数量庞大的时钟。

• 未知的大量功能配置/模式 -时钟源选择，时钟分频器因子值，不同的时钟门控技术。

• 第三方IP设计与内在的逻辑，这是非常难甄别且无法改变。此外，还有可能没有关于内部设计文档。

问题说明

该问题简化为以下伪断言：

assert “~resetn & ~enable [*N] |=> $flop_clock == 0”

基本策略

我们进行的实验尝试直接证明上述性质，但运行时间是不能容忍的，而且许多断言没有完全证实。最后，我们采取了两个步骤的方法，利用黑盒抽象技术，以提高运行时间，提高收敛证明的可能性。原始断言被分成两个部分：

1. 第一部分是证明门控时钟单元的所有时钟输出在使能信号为disable时为低电平。伪代码如下所示。为了证明这一说法中，芯可以被视为黑盒：
   assert "~resetn & ~enable[*N] |=> $root_clock==0 ##1 $root_clock == 0"

2. 第二部分是要证明，如果核输入时钟为低电平，则派生触发器的时钟信号也应该为低电平。伪代码如下所示。为了证明这一说法，该CLKGEN可以被视为黑盒子：
   assert “$root_clock == 0 |=> $flop_clock == 0”

结果

时钟信号维持低电平证明过程是在四个子系统上进行的。其中三个子系统恢复所有触发器，另一个仅仅恢复触发器的一个分支。第三方的IP被整合到子系统，许多时钟逻辑错误/问题被揭露。

• 作为形式验证的副产品，组合循环在一些模块里被发现。

• 我们发现了一些时钟被gated之后，在复位期间，依然翻转一个周期。原来，这是一个功能不是一个缺陷。

• 发现有些时钟花太长的时间才能停下来。例如，一个2.4兆赫时钟花了至少6.5us 才停下来。

• 一个随机值发生器模块的时钟不保证为低电平，这是一个不关心的情况。这一发现导致了充分保留设计的潜在优化成局部保留设计以节省面积和功率。同样地，另一个块被认为是无法满足时钟要求，但并不需要保留。

• 一个第三方IP有内部分频器，但已经不能保证停在低电平上（需要软件驱动修复）。

• 一个第三方IP有约7成存在内部时钟问题。

总之，所发现的所有潜在问题将是非常困难的。

硬件控制的时钟门控形式验证

介绍

在我们的设计中，许多时钟支持一种模式，即被硬件逻辑根据空闲/激活条件自动gated。硬件时钟门控逻辑使用公式如下:

CLKGATE.enable =~idle=~(idle1＆idle2&idlen)

在这个逻辑中潜在的漏洞可以分为以下几类:

1. idle始终为1，导致使能信号为零，gate掉时钟。

2. idle始终为0，使能信号为1，导致从不gate时钟。

3. idle有时候本来应该是0，但是为1。

4. idle有时候本来应该是1，但是为0。

时钟使能固定属性生成和证明

我们建议借助工具使用形式覆盖使能信号以及它取反信号来检测问题1和2。将两个SystemVerilog覆盖属性放到一个模块和时钟门控库模块边界，这样一来，当设计被编译时所有时钟门控的实例就都有了这些属性。

仿真覆盖模型

用于形式验证的覆盖代码同样可以用来仿真。功能覆盖数据提供了以下信息:在我们的仿真中有多少门控时钟逻辑。

结果

通常不应该有使能信号固定为0，假设仿真实现了好的覆盖率。我们发现一种情况是设计人员将没有用的块时钟使能绑定为0，综合工具会将其拿走。不管综合工具这种行为使得结果是否正确，我们认为这不是一个好的方法。其中一个后果是代码覆盖率低和浪费了大量时间在没有用的块上。

以下是存在于第三方IP一个真正的错误。CLKGATE.enable信号由edac_se_en驱动，被定义如下:

显然edac_se_live_not_zero和edac_se_live_is_zero的或结果始终为1。

时钟门控逻辑结构分析

在证明时钟门控属性时，我们发现一些时钟门控驱动了很少的触发器，这让我们怀疑它存在的价值，为了进一步分析，写了一个脚本，分析RTL里时钟树，报告出每一个时钟门控驱动的触发器数量。这有助于设计师审查他们加入时钟门控单元的效果。

下图是由脚本生成的报告的快照。在电子表格中的第二列打印出由在第一列中列出的时钟门输出驱动触发器的数目。设计者可以进行审查，以决定这是否是有意的。我们发现，其中一些时钟门控只驱动少数触发器的情况，它本身耗费的功耗可能比它省下的功耗多。一个第三方IP供应商告诉我们，他们有一个规则，如果能够驱动4个以上的触发器，会插入一个时钟门控单元，但他们违反了这个规则。

总结

综上所述，为了最大限度降低动态功耗，我们SoC设计引入时钟门控。其结果是这大大增加了对传统验证方法的挑战。我们创建了一个系统的验证时钟门控的方法：结合仿真、结构分析和形式验证。我们做了每种类型的时钟门控的检查，归纳在表格里。用我们的方法发现了一些有趣的结果。我们方法也需要进一步改进，以减少运行时间，并且在自动化流程中减少干扰。

您可以在手机移动端同步关注订阅号“路科验证”。

如需转载请联系路科验证，并注明出处“路科验证”。