基于形式验证的多周期路径检测技术

朱秋岩

(北京航天自动控制研究所，北京 100854)

0 引言

随着集成电路复杂度和规模的日益增加，芯片集成度越来越高，时钟频率也不断提高。因此，电路的时序分析和优化在集成电路设计中也越来越关键。其中，多周期路径约束作为修正建立和保持时间违例的方法，被广泛应用到芯片设计和验证中[1]。

在默认的同步电路静态时序分析中，都是按照单周期计算数据路径的建立和保持时间，但是往往存在这样的情况：一些数据不需要在下一个周期就稳定下来，可能在数据发送后的几个时钟周期之后才被使用；针对这种情况，时序分析工具无法猜度出来[2]，时序约束工具会按照单周期路径检查方法执行，虚报时序违例。多周期路径约束是用来解决这个问题的。多周期路径约束是指电路中信号从寄存器A传递到寄存器B的输入端，允许延迟一个以上的CLK时钟周期的路径约束。

在以往时序分析中，这种虚报时序违例造成其他布局布线资源侵占和设计迭代反复[3]。提出了多周期路径施加约束的方法，但是对于因多周期路径约束错误导致的时序违例，需要验证人员通过分析设计意图和动态仿真测试的方法，逐一确认是否为虚报，这样需要验证人员对所有的电路内部细节功能和输入输出情况分析和仿真，提高了验证难度，也极大降低验证效率，增加了验证周期[1]。虽然在设计中添加断言来提高多周期路径的检测效率，但是仍然采用动态仿真测试的方法确认多周期路径[4]。采用D算法分析了组合逻辑电路的敏感路径，却没有准确找出多周期路径[5]。采用智能的静态时序分析工具添加约束，可以降低多周期路径误报，但是无法100%准确的消除多周期路径误报[6]。采用声明虚假路径的办法，消除误报，但是这种过于宽松的约束会造成时序违例的漏报[7-8]。

本文通过分析多周期路径的产生机理和设计验证中的常见问题，对多周期路径进行分类与归纳，提出一种基于形式验证和静态时序分析相结合的方法，用纯静态的方式，无需深入分析和动态仿真电路功能，即可检测设计中的多周期路径，用于静态时序分析约束。

1 多周期路径的分类

多周期路径根据应用场景的不同，可以分为相同时钟的多周期路径和不同时钟间的多周期路径。

相同时钟间的多周期路径，也是最常见的多周期路径，源触发器和目的触发器使用同一个时钟信号，但源触发器与目的触发器之间的组合逻辑延迟大于一个时钟周期，如图1所示。其中源触发器和目的触发器之间的慢速组合逻辑延迟2 个或多个时钟周期，在数据到达目的触发器之前，目的触发器使能ENA 端应维持无效，目的触发器输出端Q的值只有在数据到达后才会更新。

图1 同一时钟间多周期路径示意图

不同时钟之间的多周期路径如图2 所示。源触发器和目的触发器由不同的时钟信号驱动，因为静态时序分析主要针对同源时钟分析，所以这里不同的时钟为同源的、具有固定相位关系的时钟，根据其时钟频率关系的不同又可以分为快时钟到慢时钟的多周期路径和慢时钟到快时钟的多周期路径两种。

图2 不同时钟间多周期路径示意图

2 多周期路径的时序分析

静态时序分析的对象包括：触发器和触发器之间的路径、I/O之间、 I/O和触发器之间的路径、异步复位和触发器之间的路径。由于时序分析是针对时钟驱动电路进行的，所以分析的对象一定是“触发器-触发器”对。在分析涉及I/O的时序关系对时，看似缺少一个触发器分析对象，其实是穿过FPGA(field-programmable gate array)的I/O引脚，在FPGA外部虚拟了一个触发器作为分析对象。所以，静态时序分析的所有类型的路径，都可以用“触发器-触发器”的路径分析方法表示。

2.1 相同时钟间的多周期路径时序分析

根据对多周期路径的分类，相同时钟间的多周期路径时序分析如图3所示，不设置多周期路径时，默认的建立时间路径setup设置为1个时钟周期，CLK1信号Tx时刻发生翻转，即需在Tx+1处检查CLK1时钟域信号的建立保持时间(虚线为单周期路径setup和hold时间要求)，如果将该路径设置为setup为2，hold为1的多周期路径，则在Tx+2时刻检查setup时间， setup和hold时间均放宽松1个时钟周期(实线为多周期路径setup和hold时间要求)。

图3 相同时钟间多周期路径时序分析图

2.2 不同时钟间的多周期路径时序分析

不同时钟间的多周期路径，从慢时钟到快时钟的多周期路径时序分析如图4所示，不设置多周期路径时，CLK1时钟域信号Tx时刻发生翻转，虽然Tx到Tx+1不满足一个时钟周期，但是分析工具为了方便，仍将setup定为1个时钟周期，即在Tx+1处检查CLK1时钟域信号的建立保持时间(虚线为单周期路径setup时间要求)，如果将该路径设置为setup为2，hold为1的多周期路径，则在Tx+2时刻采样有效数据，setup和hold时间均放宽松1个时钟周期(实线为多周期路径setup和hold时间要求)。

图4 慢时钟到快时钟间多周期路径时序分析图

从快时钟到慢时钟的多周期路径时序分析如图5所示，不设置多周期路径时，CLK1时钟域信号Tx时刻发生翻转，在Tx+1处检查CLK1时钟域信号的建立保持时间，如果将该路径设置为setup为2，hold为1的多周期路径，则在Tx+2时刻采样有效数据，setup和hold时间均放宽松1个时钟周期(实线为多周期路径setup和hold时间要求)。

图5 快时钟到慢时钟间的多周期路径时序分析图

I/O之间和I/O到触发器之间，可以等效为不同时钟间的多周期路径，时序分析与不同时钟间的多周期路径相同。

3 多周期路径检测

本文采用一种用静态时序分析和形式验证结合来查找设计中的多周期路径的方法，该方法先用静态时序分析的方法查找出违例路径，然后分析违例路径目的触发器时能端，通过检测目的触发器使能控制信号有效时间来判断该路径是否为多周期路径。检测流程如图6所示。

图6 多周期路径检测流程

3.1 静态时序分析查找多周期路径

通过对不同类型单周期路径和多周期路径的静态时序分析可知，如果静态时序分析时，不设置多周期路径，实际多周期路径电路时序分析约束错误，会产生建立时间或保持时间违例的误报，所以，验证人员需要查找设计中的多周期路径，设置正确的约束，使静态时序分析结果准确无误。

首先，通过使用静态时序分析，查找出时序违例的路径(不产生违例的多周期路径不需要关注，因为不会导致时序分析违例误报)[9]，而这些路径包括单周期路径和多周期路径，单周期路径是实际真正的违例电路，多周期路径是需要检测和重新设置的[10]。传统的方法是通过动态仿真测试的方法确认这些路径哪些为多周期路径，但是动态仿真测试需要人工分析和确认，花费大量时间和精力。

3.2 形式验证检测多周期路径

本文在静态时序分析结果的基础上，设计了一种多周期路径检测电路，插入需要检测的路径，采用基于断言的形式验证，用自动化的手段检测多周期路径。形式验证技术用时态逻辑来描述设计意图，通过有效的搜索方法来检查给定的系统是否满足设计意图，将使用数学推理来验证设计意图在RTL(register transfer level)实现中是否得以贯彻。形式验证是穷尽式数学技术，能够从算法上穷尽检查所有随时间可能变化的输入值，没有必要考虑如何设计激励或创建多种条件来实现较高的可覆盖率和可控性[11]，使多周期路径的查找更加快速可靠。

通过同一时钟间多周期路径电路图1和时序分析图3可知，如果源触发器和目的触发器之间存在多周期路径，目的触发器使能信号ENA可以利用计数器、移位寄存器及状态机等方法实现对目的触发器捕获周期的控制，最终表现为ENA在Tx+1时刻应维持无效，如果是2周期路径，则ENA受控制，在Tx+2时刻有效。所以，可以通过判断ENA的有效时刻来判断多周期路径，在图3的Tx+1、Tx+2时刻处检查ENA的有效值，可以检测该路径是否为2周期路径。根据以上分析，设计的检测电路如图7所示，在被测电路出现违例的路径处插入检测电路，如果输入信号d_in在Tx时刻发生变化，由0->1，则用D1处信号作为时钟，可在Tx+1时刻检测ENA，期望结果为0，说明ENA在Tx+1时刻为无效，D2处信号作为时钟，可在Tx+2时刻检测ENA，期望结果为1，说明ENA在Tx+2处为有效，检测结果通过组合逻辑输出为CHECK_OUT[12]。

图7 同一时钟间多周期路径检测电路

根据图7检测电路设计，用断言描述该属性如下所示[13]：

property Check_clk_Multi_cycle_2;

@(posedge Clk)

rose(d_in)|-> 2 rose(ENA)；

endproperty

Sig_T:assert property(Check_clk_Multi_cycle_2);

如果断言属性如果为真，则该路径为2周期路径。依照此方法类推，如果Tx+1、Tx+2时刻检查ENA无效，Tx+3时刻检查ENA有效，则可检测3周期路径。

慢时钟到快时钟多周期路径电路图2和时序分析图4所示，以2周期路径为例，最终表现为使能端ENA在图4的Tx+1时刻应维持无效，Tx+2时刻有效，通过判断ENA有效时刻，来判断是否为多周期路径。但是由于源触发器和目的触发器使用时钟不同，所以在设计中插入检测电路不同，慢时钟到快时钟多周期路径检测电路如图8所示，如果要在图4的Tx+1时刻检测ENA是否有效，则用输入d_in作为触发器A的使能信号，用d_in有效后的CLK2的第一个时钟沿，检测ENA，期望结果为0，说明ENA在Tx+1时刻为无效。将d_in用CLK2作一级寄存后输出D2，D2信号上升沿即为Tx+2时刻，用D2信号作为时钟，触发器B可在Tx+2时刻检测ENA，期望结果为1，说明ENA在Tx+2处为有效。

图8 慢时钟到快时钟间多周期路径检测电路

根据图8检测电路设计，用断言属性描述该行为如下所示：

property Check_clk1clk2_Multi_cycle_2;

@(posedge Clk2)

d_in|->stable(ENA) 1 rose(ENA)；

endproperty

Sig_T:assert property(Check_clk1clk2_Multi_cycle_2);

快时钟到慢时钟多周期路径电路图2和时序分析图5所示，以2周期路径为例，最终表现为ENA在图5的Tx+1时刻应维持无效，Tx+2时刻有效，检查原理与快时钟到慢时钟多周期路径检查原理一样，如果要在图5的Tx+1时刻检测ENA是否有效，则用输入d_in作为使能信号，用d_in有效后的CLK2的第一个时钟沿，检测ENA，期望结果为0，说明ENA在Tx+1时刻为无效。将d_in用CLK2作一级寄存后输出D2，D2信号上升沿即为Tx+2时刻，用D2信号作为时钟，可在Tx+2时刻检测ENA，期望结果为1，说明ENA在Tx+2处为有效。分析可知，快时钟到慢时钟多周期路径检测电路与图7相同，断言属性描述也与慢时钟到快时钟相同。

4 实验验证

本文采用Synopys公司的Primetime静态时序分析工具，用以查找时序分析时出现的违例路径。采用Candance公司的Jasper作为形式化验证工具，Jasper采用了高性能和大规模的形式验证技术，能够穷尽地验证模块是否满足断言要求。Jasper使用数学算法，不需要使用仿真测试平台或激励。

1)实验被测电路为相同时钟间多周期路径电路[14-15]，用Verilog HDL语言描述如下：

always@(posedge clk1)

begin

in1<=in;

end

assign in2=～in1;

assign in4=in2+in3;

assign in6=～in4+in5;

always@(posedge clk1)

begin

if(in1==0&&in==1)

counter<=2’b11;

else if(counter!=2’b00)

begin

counter<=counter-2’b01;

if(counter==2’b10)

ENA<=1;

end

end

always@(posedge clk1)

if(～ENA)

out<=0;

else

out<=in6;

选用器件为Xilinx的xc3s50-5-pq208，使用ISE综合工具综合后RTL级电路如图9所示[16]，采用静态时序分析工具违例结果如表1所示[17-18]，静态时序分析工具显示在触发器IN和触发器OUT间出现setup时间违例，建立时间余量为-0.039 ns。

图9 相同时钟被测电路1

表1 相同时钟静态时序分析违例结果

通过Jasper形式化验证，利用断言检测同时钟下触发器IN到触发器OUT是否为多周期路径。

property Check_Sameclk_Multi_cycle_3;

@(posedge Clk)

rose(d_in)|-> 3 rose(ENA)；

endproperty

Sig_T:assert property(Check_Sameclk_Multi_cycle_3);

形式验证结果为真，该路径为3周期路径。

2)实验被测电路为不同时钟多周期路径电路[19-20]，用Verilog HDL语言描述如下：

always@(posedge clk3)

begin

in1<=in;

end

assign in2=～in1;

assign in4=in2+in3;

assign in6=～in4+in5;

always@(posedge clk3)

begin

if(in1==0&&in==1)

counter<=2’b11;

else if(counter!=2’b00)

begin

counter<=counter-2’b01;

if(counter==2’b01)

ENA<=1;

end

end

always@(posedge clk2)

if(～ENA)

out<=0;

else

out<=in6;

clk clk_inst(

.CLKIN_IN(clk),

.RST_IN(1’b0),

.CLKDV_OUT(clk2),

.CLKIN_IBUFG_OUT(clk3),

.CLK0_OUT(clk1),

.LOCKED_OUT(lock));

选用器件仍为Xilinx的xc3s50-5-pq208，使用ISE综合工具综合后RTL级电路如图10所示，采用静态时序分析工具违例结果如表2所示，静态时序分析工具显示clk到CLKDV_OUT触发器建立时间违例，建立时间余量为-2.793 ns。

图10 不同时钟被测电路2

表2 不同时钟静态时序分析违例结果

通过Jasper形式化验证，利用断言检测不同时钟下触发器IN到触发器OUT是否为多周期路径。

property Check_clk1clk2_Multi_cycle_2;

@(posedge Clk2)

d_in|->stable(ENA) 1 rose(ENA)；

endproperty

Sig_T:assert property(Check_clk1clk2_Multi_cycle_2);

形式验证结果为真，该路径为2周期路径。

通过实验结果表明，本文提出的多周期路径查找方法，能够准确检测出多周期路径的存在，避免静态时序分析误报问题。

5 结束语

文中对多周期路径进行了系统的分析研究，按照多周期路径的分类，提出了基于形式化验证的自动化多周期路径检测方式，并通过Jasper形式化验证工具进行实验验证，实验证明该方法无需验证人员深入了解设计者意图和电路功能，就能有效可靠地检测出多周期路径，有助于测试人员减少对多周期路径的错误处理，有助于提升验证和设计效率，缩短验证周期。