基于形式驗證的多周期路徑檢測技術

朱秋巖

(北京航天自動控制研究所，北京 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形式化驗證工具進行實驗驗證，實驗證明該方法無需驗證人員深入了解設計者意圖和電路功能，就能有效可靠地檢測出多周期路徑，有助于測試人員減少對多周期路徑的錯誤處理，有助于提升驗證和設計效率，縮短驗證周期。