基于形式验证的毛刺检测技术

朱秋岩，李东方

(北京计算机技术及应用研究所， 北京 100854)

0 引 言

SoC(system on chip)设计的功能验证是SoC设计中最复杂也是最重要的任务。传统检测毛刺是在时序仿真阶段，仿真对象为添加延迟文件的布局布线后网表，所以难以在RTL(register transfer level)验证阶段有效发现毛刺及其对功能的影响[1]。此外标准RTL仿真不能模拟毛刺的影响，由于毛刺导致的错误在RTL没有得到解决，导致SoC验证后期出现功能错误，造成了设计迭代并影响产品的上市时机。

近些年形式验证技术迅速发展，在集成电路验证中得到了广泛应用。在模型验证中，首先使用时态逻辑来描述设计意图，其次使用数学推理来验证设计意图在实现(RTL)中是否得以贯彻。结合形式验证的方法，文献[2]提出了跨时钟域中毛刺的检测方法，但需要额外使用时钟路径区分控制信号，而且该方法设计的检测电路，仅能证明时钟路径区分控制信号有效时无毛刺，用于纠正静态时序分析中误报的违例，不能用于检测是否产生毛刺。文献[3]提出了采用形式验证检查抖动错误的方法，仅对跨时钟域故障建模，没有对毛刺进行建模，也没有考虑故障模型的可观性。

在本文中，提出一种使用形式验证技术在RTL级检测毛刺的方法，本文在文献[2]作者提出的利用静态时序分析方法基础上，设计一种毛刺检测电路，采用形式验证断言的方式描述该电路属性，用于在RTL级检测组合逻辑中可能产生的毛刺，并且不需要额外的控制信号，能够实现自动检测；然后提出描述毛刺影响的等价电路，用以在RTL级验证中准确体现毛刺现象的实际影响。为验证毛刺检测电路和故障注入电路的有效性，本文还分析了毛刺故障传播模型，在可观测点验证毛刺的影响。

1 毛刺检测电路设计

本节首先分析毛刺产生机理，然后设计了一种毛刺检测电路，并通过形式验证技术实现该检测电路在RTL级对毛刺的检测。

1.1 基于断言的形式验证技术

本文在静态时序分析结果的基础上，采用基于断言的形式验证技术，用自动化的手段检测组合逻辑毛刺。形式验证是穷尽式数学技术，能够从算法上穷尽检查所有可能随时间变化的输入值，而仿真是完全经验主义的做法，验证人员通过反复实验试图设计全面的测试输入向量，要花相当多的时间尝试所有可能的组合，因此永远不会完整。形式验证没有必要考虑如何设计激励或创建多种条件来实现较高的覆盖率和可控性，在RTL级测试覆盖更加全面，检测毛刺的可靠性优于基于测试激励的时序仿真。

1.2 毛刺产生电路分析

组合逻辑中，逻辑门输入信号的路径延时不同，到达门的时间也不一致，可能导致电路输出信号中出现“毛刺”。布尔表达式由3种类型的基本布尔逻辑门组成：单输入反相器，双输入与门和双输入或门。对于反相器，仅有一个输入，不会发生竞争冒险带来毛刺，所以本文仅分析逻辑与门和逻辑或门毛刺的产生情况：

(1)逻辑与门：逻辑与门如图1所示，a和b在产生竞争冒险时才会产生毛刺，与门的输入与毛刺的关系真值见表1。

图1 逻辑与门

由表1可知，仅当a与b同时变化，且输入值相反时，输出c端可能因逻辑门延时不同产生毛刺，逻辑与门毛刺产生时序如图2所示。

(2)逻辑或门：逻辑或门如图3所示，a和b在产生竞争冒险时才会产生毛刺，或门的输入与毛刺的关系真值见表2。

表1 逻辑与门产生毛刺的情况

图2 逻辑与门产生毛刺时序

图3 逻辑或门

表2 逻辑或门产生毛刺的情况

由表2可知，仅当a与b同时变化，且输入值相反时，输出c端可能因逻辑门延时不同产生毛刺，逻辑或门毛刺产生时序如图4所示。

图4 逻辑或门产生毛刺时序

根据上面对组合逻辑毛刺电路分析可知，在与门和或门输入端，两路输入信号同时变化，且输入值相反时，才可能产生毛刺，其它输入情况不会引起电路毛刺。

1.3 毛刺检测方法

由以上分析可知，在时序仿真时才能发现的毛刺，在RTL级，可以通过验证与门和或门的a、b两路输入是否同时产生反向的变化来判断。在此基础上，本文初步设计的检测电路如图5方框中所示。设计思路为：当a信号发生变化时(a!=past(a))，b信号也发生变化(b!=past(b))，并且a与b的值不同(a!=b)，当这3个条件同时成立时，电路会产生毛刺。所以检测电路中将a与a的上一周期的值进行异或，发生变化时，输出结果为1，同理将b与b的上一周期的值进行异或，同时，将a与b的值异或，如果a与b不同，输出结果为1，将3个结果进行与运算，表明当这3个条件同时发生时，输出结果为1。RTL级的行为，可以用形式验证的方法描述，在形式检验中，设计规范的描述被称为电路的属性(property)，采用基于断言的验证(assertion based verification，ABV)方法就是指采用断言描述电路属性，用断言描述上述属性为：

Propertyglitch_Detection_1;

@(posedge clk)

(a!=$past(a))|->(b!=$past(b))&& (a!=b);

Endproperty

根据以上断言描述，当a与b同时、反向变化时，属性为真，提示“通过”，但是实际验证中，当a保持不变的情况下，无法触发进入属性判断的条件，也会提示“通过”，称之为假通过。所以在设计中，还需考虑如何排除假通过的情况。文献[4]中介绍了专门检测信号保持不变的断言描述，如果将信号保持断言和上述毛刺检测断言结合检测毛刺，则需要用两个断言来检测毛刺，过于复杂。因此，本文的方法为在初步设计的毛刺检测电路的输出端增加一个反相器，如图5所示。

图5 毛刺检测电路设计

用断言描述图5属性为：

property glitch_Detection_2;

@(posedge clk)

(a!=$past(a))|->!((b!=$past(b))&& (a!=b));

Endproperty

即等价于：

property glitch_Detection_2;

@(posedge clk)

(a!=$past(a))|->(b==$past(b))|| (a==b);

Endproperty

含义为：①当a发生变化时，如果b保持不变或者a等于b，不会产生毛刺，该属性“通过”；②当a发生变化时，如果b不属于上一条的情况，即为产生毛刺的情况，该属性“不通过”；③当a保持不变时，该属性“通过”。这样就把产生毛刺的情况单独分为一类，即“不通过”。形式验证可以根据设计意图遍历所有的输入情况，在组合逻辑与或门处插入上述断言，可以检测毛刺的产生，当断言不通过时毛刺可能产生。

2 基于毛刺检测电路的故障分析

SoC设计时，会尽力避免组合逻辑做寄存器的reset、clear、clock、gate端，虽然寄存器的输入端对毛刺并不敏感，但是当毛刺出现在时钟沿并且影响到数据的建立时间和保持时间时，也会导致寄存器输出错误，所以本节重点研究毛刺在时序电路中的故障注入。为有效验证毛刺影响，本节首先描述毛刺在时序电路RTL级产生功能错误的原因，然后基于RTL级毛刺检测电路，描述毛刺现象的等价电路，分析毛刺故障的传播模型和评价方法，用于验证毛刺故障注入电路的有效性。

2.1 毛刺功能错误分析

在时序电路中，如果毛刺发生在目的寄存器的时钟沿，并且影响到了数据的建立保持时间，则可能造成输出的亚稳态或采样错误。文献[1]分析了亚稳态现象和影响，在此基础上，本文分析毛刺在时序电路的影响。如图6所示，R1为CLKA时钟域信号组合逻辑产生的毛刺信号，被CLKB时钟域的寄存器采样。由于CLKA和CLKB是异步时钟，R1可能发生在CLKB时钟域寄存器的建立时间或保持时间内。如果R1影响CLKB时钟域寄存器的建立和保持时间，则CLKB时钟域寄存器将进入亚稳定状态[5]。虽然亚稳态时CLKB时钟域寄存器的输出信号R2最终会稳定到逻辑0或逻辑1，但结果不可预测，毛刺对目的时钟域的影响为一个或者两个时钟周期[6]，最终稳定到正确值。如果毛刺被采样(表现为cycle2的一个单脉冲或cycle3的一个单脉冲，不考虑亚稳态更多影响周期的情况)，则会在时序电路传播，可能导致电路功能错误。

2.2 毛刺故障等价电路

文献[1]设计了亚稳态的等价电路，需要由外部的Sel信号控制发生亚稳态的时刻。本文根据1节毛刺检测电路和2.1节毛刺在时序电路影响分析，设计了一种RTL级毛刺故障等价电路，在RTL级用目的时钟域的单脉冲模拟毛刺引起的故障，该故障等价电路融合了毛刺检测电路，故障注入时刻与真实毛刺发生时刻一致。

图6 毛刺在时序逻辑影响

相同时钟下与门毛刺故障等价电路如图7所示，该电路由原电路A、毛刺检测电路D(取反)、毛刺采样电路S和毛刺注入电路M组成，等价电路中各个信号时序关系如图8所示，与门存在竞争冒险产生毛刺时，输出R2为cycle1的一个CLK周期单脉冲，输出R3为cycle2的一个CLK周期单脉冲，模拟毛刺被采样的情况。将毛刺引起的单脉冲R2、R3与原电路A做或操作(out1和out2分别表示两种错误情况)，即可模拟原电路产生毛刺故障影响的情况。

图7 相同时钟下毛刺故障等价电路

图8 故障等价电路时序关系

当逻辑与门输出被另外一个时钟域采样，根据目的时钟域时钟与源时钟域时钟的关系，更改毛刺采样电路S的设计即可；同时，逻辑或门毛刺故障等价电路可以通过更改毛刺注入电路M完成。

2.3 故障传播模型

毛刺故障产生错误的采样后，在时序电路中传播，图9数据传播流图表示毛刺故障传播路径的一种情况，b代表起始点，为故障注入点，o代表可观点。如果R2受故障影响时，XCS保持为0，那R的毛刺故障就无法传播到o，因此并不是所有b点的故障都能传播到可观点，在可观察的情况下评估毛刺故障才有意义。

图9 数据传播流图

下面分类讨论时序逻辑中组合逻辑对毛刺故障传播的影响，组合逻辑下的毛刺故障传播是类似文献[7]中描述的标签模拟算法。

(1)逻辑门：

对于反相器，毛刺故障状态将从输入到输出直接传播。对于与门，从一个输入毛刺故障传播到输出的条件为其它输入为1。对于或门，从一个输入毛刺故障传播到输出的条件为其它输入为0。

(2)算术运算符：

考虑一个表达式v(F)=v(A)v(B)。A和B是算术运算符op的操作数，F是计算的结果。令v(AORI)表示原始值和v(AGLI)表示毛刺的值故障。然后计算v(FORI)=v(AORI)v(B)和v(FGLI)=v(AGLI)v(B)，当v(FORI)≠v(FCDC)时，毛刺从A传播到F。

(3)条件：

考虑以下条件逻辑：

if (F)

Out<=A;

else

Out<=B;

如果条件控制变量F发生毛刺故障，可能导致错误的分支。所以当A≠B时，毛刺故障从F到Out有效。如果条件输入变量A具有毛刺故障，如果F为真，毛刺故障将传播到Out[8]。

基于以上分析，可以通过计算毛刺故障对可视点的覆盖评估毛刺故障传播的影响[9]。

(1)毛刺故障起始点

使用CPf(v)来表示毛刺故障起始顶点。它被递归地定义为

对于起始顶点b∈B，插入毛刺故障并且没有前向顶点。

(2)监控值

对于可观察的顶点o∈O，用形式验证监控O的值，使用Value(o)来呈现一组监视器顶点O值。

(3)毛刺故障覆盖点

CovGLI(O)表示所有可观毛刺故障覆盖点。可观察顶点

其中，oj∈O，n=|O|，wjk∈Pre(oj)，m=|Pre(oj)|。

毛刺故障RTL级评估为毛刺故障覆盖点占所有可观测点的比例[10]。

3 实验验证

本文选用商业IP核ATA-5 IDE控制器作为实验用例，它包含一个异步FIFO用以实现AMBA AHB时钟域数据到IDE时钟域的数据传输，并选用Cadence公司的Jasper形式化验证工具做结果监控，使用SystemVerilog断言实现定义电路特性，采用形式验证的方法，可以避免测试向量不完整导致的毛刺故障难以检测问题。为了保证RTL级行为正确，使用AMBA VIP监控器和IDE设备监视器，以确保AHB和IDE接口正确。整个IP核可能存在毛刺的有5个层次结构模型：异步FIFO，异步FIFO控制，IDE时序控制和AMBA AHB DMA控制。把毛刺检测电路用形式验证的断言描述并插入到检测点：

property glitch_Detection_2(a,b);

@(posedge clk)

(a!=$past(a))|->!((b!=$past(b))&& (a!=b));

Endproperty

Sig_T:assert property(glitch_Detection_2(T1,T2));

……

根据形式验证工具报出的不通过，筛选出可能发生毛刺的组合逻辑，验证了毛刺检测电路有效性。

将毛刺故障等价电路插入到检测出的发生毛刺的组合逻辑中，同时进行形式化验证监控。毛刺故障覆盖被定义为所有监控点中受毛刺故障影响的点。表3显示了5个层次结构电路中，毛刺故障覆盖情况。实验中发现一个由于毛刺故障引起的功能错误，在UDMA读时序中，FIFO指针的毛刺故障会传播给NIOR，具有毛刺故障的FIFO指针会诱发一个FIFO满信号在错误的时候有效，导致读时序异常，违背了设计师的意图。

表3 毛刺故障覆盖率

毛刺故障覆盖率不是100%说明在起始顶点的毛刺故障并没有全部传播到监控顶点。

4 结束语

在本文中，介绍了毛刺检测技术及毛刺故障注入。首先基于形式验证技术，设计了一种在RTL级检测毛刺的电路及方法，该方法不需要控制信号，自动检测毛刺，并排除了信号保持不变，假通过的情况。其次，提出一种毛刺在时序电路传播的故障模型和故障等价电路，该毛刺故障等价电路不需要控制信号，可在毛刺发生时刻自动注入。最后，通过对故障传播模型的建立和研究，采用形式验证的方法，实验结果验证了毛刺检测方法和等价电路的有效性。本文提出的毛刺检测及故障注入方法，能够帮助验证人员在RTL级对毛刺故障做更多的验证工作，提早发现验证后期才可能发现的错误。