基于形式驗(yàn)證的多周期路徑檢測技術(shù)

朱秋巖

(北京航天自動(dòng)控制研究所，北京 100854)

0 引言

隨著集成電路復(fù)雜度和規(guī)模的日益增加，芯片集成度越來越高，時(shí)鐘頻率也不斷提高。因此，電路的時(shí)序分析和優(yōu)化在集成電路設(shè)計(jì)中也越來越關(guān)鍵。其中，多周期路徑約束作為修正建立和保持時(shí)間違例的方法，被廣泛應(yīng)用到芯片設(shè)計(jì)和驗(yàn)證中[1]。

在默認(rèn)的同步電路靜態(tài)時(shí)序分析中，都是按照單周期計(jì)算數(shù)據(jù)路徑的建立和保持時(shí)間，但是往往存在這樣的情況：一些數(shù)據(jù)不需要在下一個(gè)周期就穩(wěn)定下來，可能在數(shù)據(jù)發(fā)送后的幾個(gè)時(shí)鐘周期之后才被使用；針對(duì)這種情況，時(shí)序分析工具無法猜度出來[2]，時(shí)序約束工具會(huì)按照單周期路徑檢查方法執(zhí)行，虛報(bào)時(shí)序違例。多周期路徑約束是用來解決這個(gè)問題的。多周期路徑約束是指電路中信號(hào)從寄存器A傳遞到寄存器B的輸入端，允許延遲一個(gè)以上的CLK時(shí)鐘周期的路徑約束。

在以往時(shí)序分析中，這種虛報(bào)時(shí)序違例造成其他布局布線資源侵占和設(shè)計(jì)迭代反復(fù)[3]。提出了多周期路徑施加約束的方法，但是對(duì)于因多周期路徑約束錯(cuò)誤導(dǎo)致的時(shí)序違例，需要驗(yàn)證人員通過分析設(shè)計(jì)意圖和動(dòng)態(tài)仿真測試的方法，逐一確認(rèn)是否為虛報(bào)，這樣需要驗(yàn)證人員對(duì)所有的電路內(nèi)部細(xì)節(jié)功能和輸入輸出情況分析和仿真，提高了驗(yàn)證難度，也極大降低驗(yàn)證效率，增加了驗(yàn)證周期[1]。雖然在設(shè)計(jì)中添加斷言來提高多周期路徑的檢測效率，但是仍然采用動(dòng)態(tài)仿真測試的方法確認(rèn)多周期路徑[4]。采用D算法分析了組合邏輯電路的敏感路徑，卻沒有準(zhǔn)確找出多周期路徑[5]。采用智能的靜態(tài)時(shí)序分析工具添加約束，可以降低多周期路徑誤報(bào)，但是無法100%準(zhǔn)確的消除多周期路徑誤報(bào)[6]。采用聲明虛假路徑的辦法，消除誤報(bào)，但是這種過于寬松的約束會(huì)造成時(shí)序違例的漏報(bào)[7-8]。

本文通過分析多周期路徑的產(chǎn)生機(jī)理和設(shè)計(jì)驗(yàn)證中的常見問題，對(duì)多周期路徑進(jìn)行分類與歸納，提出一種基于形式驗(yàn)證和靜態(tài)時(shí)序分析相結(jié)合的方法，用純靜態(tài)的方式，無需深入分析和動(dòng)態(tài)仿真電路功能，即可檢測設(shè)計(jì)中的多周期路徑，用于靜態(tài)時(shí)序分析約束。

1 多周期路徑的分類

多周期路徑根據(jù)應(yīng)用場景的不同，可以分為相同時(shí)鐘的多周期路徑和不同時(shí)鐘間的多周期路徑。

相同時(shí)鐘間的多周期路徑，也是最常見的多周期路徑，源觸發(fā)器和目的觸發(fā)器使用同一個(gè)時(shí)鐘信號(hào)，但源觸發(fā)器與目的觸發(fā)器之間的組合邏輯延遲大于一個(gè)時(shí)鐘周期，如圖1所示。其中源觸發(fā)器和目的觸發(fā)器之間的慢速組合邏輯延遲2 個(gè)或多個(gè)時(shí)鐘周期，在數(shù)據(jù)到達(dá)目的觸發(fā)器之前，目的觸發(fā)器使能ENA 端應(yīng)維持無效，目的觸發(fā)器輸出端Q的值只有在數(shù)據(jù)到達(dá)后才會(huì)更新。

圖1 同一時(shí)鐘間多周期路徑示意圖

不同時(shí)鐘之間的多周期路徑如圖2 所示。源觸發(fā)器和目的觸發(fā)器由不同的時(shí)鐘信號(hào)驅(qū)動(dòng)，因?yàn)殪o態(tài)時(shí)序分析主要針對(duì)同源時(shí)鐘分析，所以這里不同的時(shí)鐘為同源的、具有固定相位關(guān)系的時(shí)鐘，根據(jù)其時(shí)鐘頻率關(guān)系的不同又可以分為快時(shí)鐘到慢時(shí)鐘的多周期路徑和慢時(shí)鐘到快時(shí)鐘的多周期路徑兩種。

圖2 不同時(shí)鐘間多周期路徑示意圖

2 多周期路徑的時(shí)序分析

靜態(tài)時(shí)序分析的對(duì)象包括：觸發(fā)器和觸發(fā)器之間的路徑、I/O之間、 I/O和觸發(fā)器之間的路徑、異步復(fù)位和觸發(fā)器之間的路徑。由于時(shí)序分析是針對(duì)時(shí)鐘驅(qū)動(dòng)電路進(jìn)行的，所以分析的對(duì)象一定是“觸發(fā)器-觸發(fā)器”對(duì)。在分析涉及I/O的時(shí)序關(guān)系對(duì)時(shí)，看似缺少一個(gè)觸發(fā)器分析對(duì)象，其實(shí)是穿過FPGA(field-programmable gate array)的I/O引腳，在FPGA外部虛擬了一個(gè)觸發(fā)器作為分析對(duì)象。所以，靜態(tài)時(shí)序分析的所有類型的路徑，都可以用“觸發(fā)器-觸發(fā)器”的路徑分析方法表示。

2.1 相同時(shí)鐘間的多周期路徑時(shí)序分析

根據(jù)對(duì)多周期路徑的分類，相同時(shí)鐘間的多周期路徑時(shí)序分析如圖3所示，不設(shè)置多周期路徑時(shí)，默認(rèn)的建立時(shí)間路徑setup設(shè)置為1個(gè)時(shí)鐘周期，CLK1信號(hào)Tx時(shí)刻發(fā)生翻轉(zhuǎn)，即需在Tx+1處檢查CLK1時(shí)鐘域信號(hào)的建立保持時(shí)間(虛線為單周期路徑setup和hold時(shí)間要求)，如果將該路徑設(shè)置為setup為2，hold為1的多周期路徑，則在Tx+2時(shí)刻檢查setup時(shí)間， setup和hold時(shí)間均放寬松1個(gè)時(shí)鐘周期(實(shí)線為多周期路徑setup和hold時(shí)間要求)。

圖3 相同時(shí)鐘間多周期路徑時(shí)序分析圖

2.2 不同時(shí)鐘間的多周期路徑時(shí)序分析

不同時(shí)鐘間的多周期路徑，從慢時(shí)鐘到快時(shí)鐘的多周期路徑時(shí)序分析如圖4所示，不設(shè)置多周期路徑時(shí)，CLK1時(shí)鐘域信號(hào)Tx時(shí)刻發(fā)生翻轉(zhuǎn)，雖然Tx到Tx+1不滿足一個(gè)時(shí)鐘周期，但是分析工具為了方便，仍將setup定為1個(gè)時(shí)鐘周期，即在Tx+1處檢查CLK1時(shí)鐘域信號(hào)的建立保持時(shí)間(虛線為單周期路徑setup時(shí)間要求)，如果將該路徑設(shè)置為setup為2，hold為1的多周期路徑，則在Tx+2時(shí)刻采樣有效數(shù)據(jù)，setup和hold時(shí)間均放寬松1個(gè)時(shí)鐘周期(實(shí)線為多周期路徑setup和hold時(shí)間要求)。

圖4 慢時(shí)鐘到快時(shí)鐘間多周期路徑時(shí)序分析圖

從快時(shí)鐘到慢時(shí)鐘的多周期路徑時(shí)序分析如圖5所示，不設(shè)置多周期路徑時(shí)，CLK1時(shí)鐘域信號(hào)Tx時(shí)刻發(fā)生翻轉(zhuǎn)，在Tx+1處檢查CLK1時(shí)鐘域信號(hào)的建立保持時(shí)間，如果將該路徑設(shè)置為setup為2，hold為1的多周期路徑，則在Tx+2時(shí)刻采樣有效數(shù)據(jù)，setup和hold時(shí)間均放寬松1個(gè)時(shí)鐘周期(實(shí)線為多周期路徑setup和hold時(shí)間要求)。

圖5 快時(shí)鐘到慢時(shí)鐘間的多周期路徑時(shí)序分析圖

I/O之間和I/O到觸發(fā)器之間，可以等效為不同時(shí)鐘間的多周期路徑，時(shí)序分析與不同時(shí)鐘間的多周期路徑相同。

3 多周期路徑檢測

本文采用一種用靜態(tài)時(shí)序分析和形式驗(yàn)證結(jié)合來查找設(shè)計(jì)中的多周期路徑的方法，該方法先用靜態(tài)時(shí)序分析的方法查找出違例路徑，然后分析違例路徑目的觸發(fā)器時(shí)能端，通過檢測目的觸發(fā)器使能控制信號(hào)有效時(shí)間來判斷該路徑是否為多周期路徑。檢測流程如圖6所示。

圖6 多周期路徑檢測流程

3.1 靜態(tài)時(shí)序分析查找多周期路徑

通過對(duì)不同類型單周期路徑和多周期路徑的靜態(tài)時(shí)序分析可知，如果靜態(tài)時(shí)序分析時(shí)，不設(shè)置多周期路徑，實(shí)際多周期路徑電路時(shí)序分析約束錯(cuò)誤，會(huì)產(chǎn)生建立時(shí)間或保持時(shí)間違例的誤報(bào)，所以，驗(yàn)證人員需要查找設(shè)計(jì)中的多周期路徑，設(shè)置正確的約束，使靜態(tài)時(shí)序分析結(jié)果準(zhǔn)確無誤。

首先，通過使用靜態(tài)時(shí)序分析，查找出時(shí)序違例的路徑(不產(chǎn)生違例的多周期路徑不需要關(guān)注，因?yàn)椴粫?huì)導(dǎo)致時(shí)序分析違例誤報(bào))[9]，而這些路徑包括單周期路徑和多周期路徑，單周期路徑是實(shí)際真正的違例電路，多周期路徑是需要檢測和重新設(shè)置的[10]。傳統(tǒng)的方法是通過動(dòng)態(tài)仿真測試的方法確認(rèn)這些路徑哪些為多周期路徑，但是動(dòng)態(tài)仿真測試需要人工分析和確認(rèn)，花費(fèi)大量時(shí)間和精力。

3.2 形式驗(yàn)證檢測多周期路徑

本文在靜態(tài)時(shí)序分析結(jié)果的基礎(chǔ)上，設(shè)計(jì)了一種多周期路徑檢測電路，插入需要檢測的路徑，采用基于斷言的形式驗(yàn)證，用自動(dòng)化的手段檢測多周期路徑。形式驗(yàn)證技術(shù)用時(shí)態(tài)邏輯來描述設(shè)計(jì)意圖，通過有效的搜索方法來檢查給定的系統(tǒng)是否滿足設(shè)計(jì)意圖，將使用數(shù)學(xué)推理來驗(yàn)證設(shè)計(jì)意圖在RTL(register transfer level)實(shí)現(xiàn)中是否得以貫徹。形式驗(yàn)證是窮盡式數(shù)學(xué)技術(shù)，能夠從算法上窮盡檢查所有隨時(shí)間可能變化的輸入值，沒有必要考慮如何設(shè)計(jì)激勵(lì)或創(chuàng)建多種條件來實(shí)現(xiàn)較高的可覆蓋率和可控性[11]，使多周期路徑的查找更加快速可靠。

通過同一時(shí)鐘間多周期路徑電路圖1和時(shí)序分析圖3可知，如果源觸發(fā)器和目的觸發(fā)器之間存在多周期路徑，目的觸發(fā)器使能信號(hào)ENA可以利用計(jì)數(shù)器、移位寄存器及狀態(tài)機(jī)等方法實(shí)現(xiàn)對(duì)目的觸發(fā)器捕獲周期的控制，最終表現(xiàn)為ENA在Tx+1時(shí)刻應(yīng)維持無效，如果是2周期路徑，則ENA受控制，在Tx+2時(shí)刻有效。所以，可以通過判斷ENA的有效時(shí)刻來判斷多周期路徑，在圖3的Tx+1、Tx+2時(shí)刻處檢查ENA的有效值，可以檢測該路徑是否為2周期路徑。根據(jù)以上分析，設(shè)計(jì)的檢測電路如圖7所示，在被測電路出現(xiàn)違例的路徑處插入檢測電路，如果輸入信號(hào)d_in在Tx時(shí)刻發(fā)生變化，由0->1，則用D1處信號(hào)作為時(shí)鐘，可在Tx+1時(shí)刻檢測ENA，期望結(jié)果為0，說明ENA在Tx+1時(shí)刻為無效，D2處信號(hào)作為時(shí)鐘，可在Tx+2時(shí)刻檢測ENA，期望結(jié)果為1，說明ENA在Tx+2處為有效，檢測結(jié)果通過組合邏輯輸出為CHECK_OUT[12]。

圖7 同一時(shí)鐘間多周期路徑檢測電路

根據(jù)圖7檢測電路設(shè)計(jì)，用斷言描述該屬性如下所示[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時(shí)刻檢查ENA無效，Tx+3時(shí)刻檢查ENA有效，則可檢測3周期路徑。

慢時(shí)鐘到快時(shí)鐘多周期路徑電路圖2和時(shí)序分析圖4所示，以2周期路徑為例，最終表現(xiàn)為使能端ENA在圖4的Tx+1時(shí)刻應(yīng)維持無效，Tx+2時(shí)刻有效，通過判斷ENA有效時(shí)刻，來判斷是否為多周期路徑。但是由于源觸發(fā)器和目的觸發(fā)器使用時(shí)鐘不同，所以在設(shè)計(jì)中插入檢測電路不同，慢時(shí)鐘到快時(shí)鐘多周期路徑檢測電路如圖8所示，如果要在圖4的Tx+1時(shí)刻檢測ENA是否有效，則用輸入d_in作為觸發(fā)器A的使能信號(hào)，用d_in有效后的CLK2的第一個(gè)時(shí)鐘沿，檢測ENA，期望結(jié)果為0，說明ENA在Tx+1時(shí)刻為無效。將d_in用CLK2作一級(jí)寄存后輸出D2，D2信號(hào)上升沿即為Tx+2時(shí)刻，用D2信號(hào)作為時(shí)鐘，觸發(fā)器B可在Tx+2時(shí)刻檢測ENA，期望結(jié)果為1，說明ENA在Tx+2處為有效。

圖8 慢時(shí)鐘到快時(shí)鐘間多周期路徑檢測電路

根據(jù)圖8檢測電路設(shè)計(jì)，用斷言屬性描述該行為如下所示：

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);

快時(shí)鐘到慢時(shí)鐘多周期路徑電路圖2和時(shí)序分析圖5所示，以2周期路徑為例，最終表現(xiàn)為ENA在圖5的Tx+1時(shí)刻應(yīng)維持無效，Tx+2時(shí)刻有效，檢查原理與快時(shí)鐘到慢時(shí)鐘多周期路徑檢查原理一樣，如果要在圖5的Tx+1時(shí)刻檢測ENA是否有效，則用輸入d_in作為使能信號(hào)，用d_in有效后的CLK2的第一個(gè)時(shí)鐘沿，檢測ENA，期望結(jié)果為0，說明ENA在Tx+1時(shí)刻為無效。將d_in用CLK2作一級(jí)寄存后輸出D2，D2信號(hào)上升沿即為Tx+2時(shí)刻，用D2信號(hào)作為時(shí)鐘，可在Tx+2時(shí)刻檢測ENA，期望結(jié)果為1，說明ENA在Tx+2處為有效。分析可知，快時(shí)鐘到慢時(shí)鐘多周期路徑檢測電路與圖7相同，斷言屬性描述也與慢時(shí)鐘到快時(shí)鐘相同。

4 實(shí)驗(yàn)驗(yàn)證

本文采用Synopys公司的Primetime靜態(tài)時(shí)序分析工具，用以查找時(shí)序分析時(shí)出現(xiàn)的違例路徑。采用Candance公司的Jasper作為形式化驗(yàn)證工具，Jasper采用了高性能和大規(guī)模的形式驗(yàn)證技術(shù)，能夠窮盡地驗(yàn)證模塊是否滿足斷言要求。Jasper使用數(shù)學(xué)算法，不需要使用仿真測試平臺(tái)或激勵(lì)。

1)實(shí)驗(yàn)被測電路為相同時(shí)鐘間多周期路徑電路[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級(jí)電路如圖9所示[16]，采用靜態(tài)時(shí)序分析工具違例結(jié)果如表1所示[17-18]，靜態(tài)時(shí)序分析工具顯示在觸發(fā)器IN和觸發(fā)器OUT間出現(xiàn)setup時(shí)間違例，建立時(shí)間余量為-0.039 ns。

圖9 相同時(shí)鐘被測電路1

表1 相同時(shí)鐘靜態(tài)時(shí)序分析違例結(jié)果

通過Jasper形式化驗(yàn)證，利用斷言檢測同時(shí)鐘下觸發(fā)器IN到觸發(fā)器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);

形式驗(yàn)證結(jié)果為真，該路徑為3周期路徑。

2)實(shí)驗(yàn)被測電路為不同時(shí)鐘多周期路徑電路[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級(jí)電路如圖10所示，采用靜態(tài)時(shí)序分析工具違例結(jié)果如表2所示，靜態(tài)時(shí)序分析工具顯示clk到CLKDV_OUT觸發(fā)器建立時(shí)間違例，建立時(shí)間余量為-2.793 ns。

圖10 不同時(shí)鐘被測電路2

表2 不同時(shí)鐘靜態(tài)時(shí)序分析違例結(jié)果

通過Jasper形式化驗(yàn)證，利用斷言檢測不同時(shí)鐘下觸發(fā)器IN到觸發(fā)器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);

形式驗(yàn)證結(jié)果為真，該路徑為2周期路徑。

通過實(shí)驗(yàn)結(jié)果表明，本文提出的多周期路徑查找方法，能夠準(zhǔn)確檢測出多周期路徑的存在，避免靜態(tài)時(shí)序分析誤報(bào)問題。

5 結(jié)束語

文中對(duì)多周期路徑進(jìn)行了系統(tǒng)的分析研究，按照多周期路徑的分類，提出了基于形式化驗(yàn)證的自動(dòng)化多周期路徑檢測方式，并通過Jasper形式化驗(yàn)證工具進(jìn)行實(shí)驗(yàn)驗(yàn)證，實(shí)驗(yàn)證明該方法無需驗(yàn)證人員深入了解設(shè)計(jì)者意圖和電路功能，就能有效可靠地檢測出多周期路徑，有助于測試人員減少對(duì)多周期路徑的錯(cuò)誤處理，有助于提升驗(yàn)證和設(shè)計(jì)效率，縮短驗(yàn)證周期。