朱秋巖
(北京航天自動控制研究所,北京 100854)
隨著集成電路復(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ù)不需要在下一個周期就穩(wěn)定下來,可能在數(shù)據(jù)發(fā)送后的幾個時(shí)鐘周期之后才被使用;針對這種情況,時(shí)序分析工具無法猜度出來[2],時(shí)序約束工具會按照單周期路徑檢查方法執(zhí)行,虛報(bào)時(shí)序違例。多周期路徑約束是用來解決這個問題的。多周期路徑約束是指電路中信號從寄存器A傳遞到寄存器B的輸入端,允許延遲一個以上的CLK時(shí)鐘周期的路徑約束。
在以往時(shí)序分析中,這種虛報(bào)時(shí)序違例造成其他布局布線資源侵占和設(shè)計(jì)迭代反復(fù)[3]。提出了多周期路徑施加約束的方法,但是對于因多周期路徑約束錯誤導(dǎo)致的時(shí)序違例,需要驗(yàn)證人員通過分析設(shè)計(jì)意圖和動態(tài)仿真測試的方法,逐一確認(rèn)是否為虛報(bào),這樣需要驗(yàn)證人員對所有的電路內(nèi)部細(xì)節(jié)功能和輸入輸出情況分析和仿真,提高了驗(yàn)證難度,也極大降低驗(yàn)證效率,增加了驗(yàn)證周期[1]。雖然在設(shè)計(jì)中添加斷言來提高多周期路徑的檢測效率,但是仍然采用動態(tài)仿真測試的方法確認(rèn)多周期路徑[4]。采用D算法分析了組合邏輯電路的敏感路徑,卻沒有準(zhǔn)確找出多周期路徑[5]。采用智能的靜態(tài)時(shí)序分析工具添加約束,可以降低多周期路徑誤報(bào),但是無法100%準(zhǔn)確的消除多周期路徑誤報(bào)[6]。采用聲明虛假路徑的辦法,消除誤報(bào),但是這種過于寬松的約束會造成時(shí)序違例的漏報(bào)[7-8]。
本文通過分析多周期路徑的產(chǎn)生機(jī)理和設(shè)計(jì)驗(yàn)證中的常見問題,對多周期路徑進(jìn)行分類與歸納,提出一種基于形式驗(yàn)證和靜態(tài)時(shí)序分析相結(jié)合的方法,用純靜態(tài)的方式,無需深入分析和動態(tài)仿真電路功能,即可檢測設(shè)計(jì)中的多周期路徑,用于靜態(tài)時(shí)序分析約束。
多周期路徑根據(jù)應(yīng)用場景的不同,可以分為相同時(shí)鐘的多周期路徑和不同時(shí)鐘間的多周期路徑。
相同時(shí)鐘間的多周期路徑,也是最常見的多周期路徑,源觸發(fā)器和目的觸發(fā)器使用同一個時(shí)鐘信號,但源觸發(fā)器與目的觸發(fā)器之間的組合邏輯延遲大于一個時(shí)鐘周期,如圖1所示。其中源觸發(fā)器和目的觸發(fā)器之間的慢速組合邏輯延遲2 個或多個時(shí)鐘周期,在數(shù)據(jù)到達(dá)目的觸發(fā)器之前,目的觸發(fā)器使能ENA 端應(yīng)維持無效,目的觸發(fā)器輸出端Q的值只有在數(shù)據(jù)到達(dá)后才會更新。
圖1 同一時(shí)鐘間多周期路徑示意圖
不同時(shí)鐘之間的多周期路徑如圖2 所示。源觸發(fā)器和目的觸發(fā)器由不同的時(shí)鐘信號驅(qū)動,因?yàn)殪o態(tài)時(shí)序分析主要針對同源時(shí)鐘分析,所以這里不同的時(shí)鐘為同源的、具有固定相位關(guān)系的時(shí)鐘,根據(jù)其時(shí)鐘頻率關(guān)系的不同又可以分為快時(shí)鐘到慢時(shí)鐘的多周期路徑和慢時(shí)鐘到快時(shí)鐘的多周期路徑兩種。
圖2 不同時(shí)鐘間多周期路徑示意圖
靜態(tài)時(shí)序分析的對象包括:觸發(fā)器和觸發(fā)器之間的路徑、I/O之間、 I/O和觸發(fā)器之間的路徑、異步復(fù)位和觸發(fā)器之間的路徑。由于時(shí)序分析是針對時(shí)鐘驅(qū)動電路進(jìn)行的,所以分析的對象一定是“觸發(fā)器-觸發(fā)器”對。在分析涉及I/O的時(shí)序關(guān)系對時(shí),看似缺少一個觸發(fā)器分析對象,其實(shí)是穿過FPGA(field-programmable gate array)的I/O引腳,在FPGA外部虛擬了一個觸發(fā)器作為分析對象。所以,靜態(tài)時(shí)序分析的所有類型的路徑,都可以用“觸發(fā)器-觸發(fā)器”的路徑分析方法表示。
根據(jù)對多周期路徑的分類,相同時(shí)鐘間的多周期路徑時(shí)序分析如圖3所示,不設(shè)置多周期路徑時(shí),默認(rèn)的建立時(shí)間路徑setup設(shè)置為1個時(shí)鐘周期,CLK1信號Tx時(shí)刻發(fā)生翻轉(zhuǎn),即需在Tx+1處檢查CLK1時(shí)鐘域信號的建立保持時(shí)間(虛線為單周期路徑setup和hold時(shí)間要求),如果將該路徑設(shè)置為setup為2,hold為1的多周期路徑,則在Tx+2時(shí)刻檢查setup時(shí)間, setup和hold時(shí)間均放寬松1個時(shí)鐘周期(實(shí)線為多周期路徑setup和hold時(shí)間要求)。
圖3 相同時(shí)鐘間多周期路徑時(shí)序分析圖
不同時(shí)鐘間的多周期路徑,從慢時(shí)鐘到快時(shí)鐘的多周期路徑時(shí)序分析如圖4所示,不設(shè)置多周期路徑時(shí),CLK1時(shí)鐘域信號Tx時(shí)刻發(fā)生翻轉(zhuǎn),雖然Tx到Tx+1不滿足一個時(shí)鐘周期,但是分析工具為了方便,仍將setup定為1個時(shí)鐘周期,即在Tx+1處檢查CLK1時(shí)鐘域信號的建立保持時(shí)間(虛線為單周期路徑setup時(shí)間要求),如果將該路徑設(shè)置為setup為2,hold為1的多周期路徑,則在Tx+2時(shí)刻采樣有效數(shù)據(jù),setup和hold時(shí)間均放寬松1個時(shí)鐘周期(實(shí)線為多周期路徑setup和hold時(shí)間要求)。
圖4 慢時(shí)鐘到快時(shí)鐘間多周期路徑時(shí)序分析圖
從快時(shí)鐘到慢時(shí)鐘的多周期路徑時(shí)序分析如圖5所示,不設(shè)置多周期路徑時(shí),CLK1時(shí)鐘域信號Tx時(shí)刻發(fā)生翻轉(zhuǎn),在Tx+1處檢查CLK1時(shí)鐘域信號的建立保持時(shí)間,如果將該路徑設(shè)置為setup為2,hold為1的多周期路徑,則在Tx+2時(shí)刻采樣有效數(shù)據(jù),setup和hold時(shí)間均放寬松1個時(shí)鐘周期(實(shí)線為多周期路徑setup和hold時(shí)間要求)。
圖5 快時(shí)鐘到慢時(shí)鐘間的多周期路徑時(shí)序分析圖
I/O之間和I/O到觸發(fā)器之間,可以等效為不同時(shí)鐘間的多周期路徑,時(shí)序分析與不同時(shí)鐘間的多周期路徑相同。
本文采用一種用靜態(tài)時(shí)序分析和形式驗(yàn)證結(jié)合來查找設(shè)計(jì)中的多周期路徑的方法,該方法先用靜態(tài)時(shí)序分析的方法查找出違例路徑,然后分析違例路徑目的觸發(fā)器時(shí)能端,通過檢測目的觸發(fā)器使能控制信號有效時(shí)間來判斷該路徑是否為多周期路徑。檢測流程如圖6所示。
圖6 多周期路徑檢測流程
通過對不同類型單周期路徑和多周期路徑的靜態(tài)時(shí)序分析可知,如果靜態(tài)時(shí)序分析時(shí),不設(shè)置多周期路徑,實(shí)際多周期路徑電路時(shí)序分析約束錯誤,會產(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)椴粫?dǎo)致時(shí)序分析違例誤報(bào))[9],而這些路徑包括單周期路徑和多周期路徑,單周期路徑是實(shí)際真正的違例電路,多周期路徑是需要檢測和重新設(shè)置的[10]。傳統(tǒng)的方法是通過動態(tài)仿真測試的方法確認(rèn)這些路徑哪些為多周期路徑,但是動態(tài)仿真測試需要人工分析和確認(rèn),花費(fèi)大量時(shí)間和精力。
本文在靜態(tài)時(shí)序分析結(jié)果的基礎(chǔ)上,設(shè)計(jì)了一種多周期路徑檢測電路,插入需要檢測的路徑,采用基于斷言的形式驗(yàn)證,用自動化的手段檢測多周期路徑。形式驗(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ì)激勵或創(chuàng)建多種條件來實(shí)現(xiàn)較高的可覆蓋率和可控性[11],使多周期路徑的查找更加快速可靠。
通過同一時(shí)鐘間多周期路徑電路圖1和時(shí)序分析圖3可知,如果源觸發(fā)器和目的觸發(fā)器之間存在多周期路徑,目的觸發(fā)器使能信號ENA可以利用計(jì)數(shù)器、移位寄存器及狀態(tài)機(jī)等方法實(shí)現(xiàn)對目的觸發(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)違例的路徑處插入檢測電路,如果輸入信號d_in在Tx時(shí)刻發(fā)生變化,由0->1,則用D1處信號作為時(shí)鐘,可在Tx+1時(shí)刻檢測ENA,期望結(jié)果為0,說明ENA在Tx+1時(shí)刻為無效,D2處信號作為時(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的使能信號,用d_in有效后的CLK2的第一個時(shí)鐘沿,檢測ENA,期望結(jié)果為0,說明ENA在Tx+1時(shí)刻為無效。將d_in用CLK2作一級寄存后輸出D2,D2信號上升沿即為Tx+2時(shí)刻,用D2信號作為時(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作為使能信號,用d_in有效后的CLK2的第一個時(shí)鐘沿,檢測ENA,期望結(jié)果為0,說明ENA在Tx+1時(shí)刻為無效。將d_in用CLK2作一級寄存后輸出D2,D2信號上升沿即為Tx+2時(shí)刻,用D2信號作為時(shí)鐘,可在Tx+2時(shí)刻檢測ENA,期望結(jié)果為1,說明ENA在Tx+2處為有效。分析可知,快時(shí)鐘到慢時(shí)鐘多周期路徑檢測電路與圖7相同,斷言屬性描述也與慢時(shí)鐘到快時(shí)鐘相同。
本文采用Synopys公司的Primetime靜態(tài)時(shí)序分析工具,用以查找時(shí)序分析時(shí)出現(xiàn)的違例路徑。采用Candance公司的Jasper作為形式化驗(yàn)證工具,Jasper采用了高性能和大規(guī)模的形式驗(yàn)證技術(shù),能夠窮盡地驗(yàn)證模塊是否滿足斷言要求。Jasper使用數(shù)學(xué)算法,不需要使用仿真測試平臺或激勵。
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級電路如圖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級電路如圖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)問題。
文中對多周期路徑進(jìn)行了系統(tǒng)的分析研究,按照多周期路徑的分類,提出了基于形式化驗(yàn)證的自動化多周期路徑檢測方式,并通過Jasper形式化驗(yàn)證工具進(jìn)行實(shí)驗(yàn)驗(yàn)證,實(shí)驗(yàn)證明該方法無需驗(yàn)證人員深入了解設(shè)計(jì)者意圖和電路功能,就能有效可靠地檢測出多周期路徑,有助于測試人員減少對多周期路徑的錯誤處理,有助于提升驗(yàn)證和設(shè)計(jì)效率,縮短驗(yàn)證周期。