張留宛

摘要：為了提高時序電路等價性驗證速度，提出了一種并行的驗證方法。時序電路就是一種有限狀態(tài)機(jī)，本文借鑒有限狀態(tài)機(jī)的并行最簡化方法來設(shè)計一種并行的時序電路等價性驗證方法，并以實例證明了該方法的有效性和可行性。

關(guān)鍵詞：時序電路;有限狀態(tài)機(jī);等價性

中圖分類號：TP301 文獻(xiàn)標(biāo)識碼：A

文章編號：1009-3044（2019）29-0235-03

1概述

隨著IC產(chǎn)業(yè)的不斷發(fā)展，出現(xiàn)了超大規(guī)模的集成電路，因此化簡時序電路并進(jìn)行等價性驗證變得越來越重要。由于數(shù)字電路不同的邏輯功能特點(diǎn)，可以將其分為組合電路和時序電路兩大類。其中組合電路具有任意時刻的輸出僅取決于當(dāng)前時刻的輸入，和電路原有的狀態(tài)無關(guān)的邏輯功能特點(diǎn)。而時序電路具有任意時刻的輸出不僅取決于該時刻的輸入，而且還取決于電路原有的狀態(tài)，也就意味著，還與以前的輸人有關(guān)的邏輯功能特點(diǎn)。

因此，化簡時序電路并驗證其等價性是本文所要研究的內(nèi)容，因為減少其狀態(tài)數(shù)即可減少時序電路中的存儲元件和觸發(fā)器的數(shù)量，從而達(dá)到降低成本、減少電路規(guī)模、加快電路開關(guān)速度的效果。本文提出了一種并行的時序電路等價性驗證方法，該方法借鑒了有限狀態(tài)機(jī)的并行最簡化方法，并以實例證明了其有效性和可行性。

2傳統(tǒng)的時序等價性算法介紹

為了驗證時序電路的等價性，文獻(xiàn)[1]提出一種改進(jìn)的基于時間幀展開的時序電路等價驗證算法。文獻(xiàn)[2]將存儲元素映射方法應(yīng)用到時序電路等價性驗證中。文獻(xiàn)[3]將隨機(jī)仿真、局部BDD、寄存器匹配和狀態(tài)遍歷等多種技術(shù)相結(jié)合來進(jìn)行時序電路的等價性驗證。文獻(xiàn)[4]提出時序電路等價驗證的觸發(fā)器匹配。文獻(xiàn)[5]提出了一種基于粒計算的狀態(tài)化簡算法。文獻(xiàn)[6]提出了基于等價關(guān)系的完全確定時序邏輯電路狀態(tài)化簡算法，其構(gòu)建狀態(tài)轉(zhuǎn)移系統(tǒng)矩陣來化簡時序邏輯電路，利用等價關(guān)系將相同的列進(jìn)行合并，得到最小化狀態(tài)表。

3時序電路等價性定義

時序電路等同于自動機(jī)理論中的有限狀態(tài)機(jī)。有限狀態(tài)機(jī)是表示有限個狀態(tài)與在狀態(tài)之間的轉(zhuǎn)移和動作等行為的數(shù)學(xué)模型，可以用其來描述時序電路系統(tǒng)的輸入輸出。本文采用Mealy型狀態(tài)機(jī)來描述時序電路。Mealy型狀態(tài)機(jī)描述如下：路上的輸入符號均產(chǎn)生相同的輸出符號。由此得出兩個狀態(tài)是否等價需滿足的條件是：①在所有的輸入條件下，兩個狀態(tài)所對應(yīng)的輸出是相同的;②在所有的輸入條件下，兩個狀態(tài)的轉(zhuǎn)移結(jié)果相同。等價狀態(tài)是具有傳遞性的。也就是如果第1個狀態(tài)和第2個狀態(tài)等效，第2個狀態(tài)和第3個狀態(tài)等效，那么，一定有第1個狀態(tài)和第3個狀態(tài)等效。記作（s1，s2）（s2，s3）→（S1，S3）。

本文所提出的方法適用于已經(jīng)給出開始狀態(tài)的時序電路。在知道電路開始狀態(tài)的情況下，可以使用開始狀態(tài)和在此開始狀態(tài)的可達(dá)狀態(tài)空間形成的子狀態(tài)轉(zhuǎn)換圖來表示時序電路。兩時序電路是否等價的驗證等同于驗證兩時序電路對應(yīng)的狀態(tài)轉(zhuǎn)換圖是否同構(gòu)。如何判斷兩狀態(tài)轉(zhuǎn)換圖是否同構(gòu)，就是在一個狀態(tài)轉(zhuǎn)換圖上隨意取一頂點(diǎn)均能在另一狀態(tài)轉(zhuǎn)換圖上找出與之等價的頂點(diǎn)，由此可以推斷出兩個狀態(tài)轉(zhuǎn)換圖所表示的時序電路是等價的。

如下圖1是時序電路1的狀態(tài)轉(zhuǎn)換圖，圖2是時序電路2的狀態(tài)轉(zhuǎn)換圖，其圖上的頂點(diǎn)代表狀態(tài)，頂點(diǎn)與頂點(diǎn)之間的箭頭表示狀態(tài)之間的轉(zhuǎn)換關(guān)系，且轉(zhuǎn)換關(guān)系的條件在箭頭上標(biāo)注出來，其標(biāo)注的格式為輸入/輸出。為了區(qū)別圖l和圖2中的頂點(diǎn)，本文采用不同的編號來表示圖1和圖2的頂點(diǎn)。S00和S10分別是圖1和圖2的開始頂點(diǎn)。

（4）刪去狀態(tài)集中的所有不可達(dá)狀態(tài)，可得簡化后的時序電路狀態(tài)轉(zhuǎn)換圖。

對于一個時序電路的狀態(tài)轉(zhuǎn)換圖如圖2，構(gòu)造一個可區(qū)分狀態(tài)矩陣表。分別將狀態(tài)001，011，100用S11，S12，s13來表示，狀態(tài)表的第一列是按順序排列的狀態(tài)并刪除第一個狀態(tài)，相反狀態(tài)表的最后一行是按順序排列的狀態(tài)并去掉最后一個狀態(tài)。對于任意的狀態(tài)對（q，p），判斷它們是不是可以合并的，即判斷他們是不是等價的。本文中（q，p）與（p，q）表示相同的狀態(tài)對，即（q，p）=（p，q），因此在可區(qū)分狀態(tài)矩陣表中只需要考慮對角線以下的狀態(tài)對，矩陣中對角線以上的狀態(tài)用“一”來進(jìn)行標(biāo)記，其他的表項用空來標(biāo)記。圖2相對應(yīng)的可區(qū)分狀態(tài)矩陣表結(jié)構(gòu)如下表1所示：

對于上述可區(qū)分狀態(tài)矩陣表進(jìn)行分析，根據(jù)狀態(tài)對之間的關(guān)系，首先對輸出為1的狀態(tài)對進(jìn)行分析;其次處理輸出為0的狀態(tài)對;第三，輸出既有0又有1的狀態(tài)對可以同時進(jìn)行區(qū)分。然后對已區(qū)分出的狀態(tài)對相關(guān)聯(lián)的狀態(tài)對可以一起被區(qū)分?？梢圆⑿谢幚砘诖岁P(guān)系的可區(qū)分狀態(tài)對。

對于未標(biāo)記的狀態(tài)對（s10，s12），（s10，S11），（s11，S12）執(zhí)行do-while語句的第一次循環(huán)，每個狀態(tài)對分別輸入0、1，對所得到的狀態(tài)對分別同時進(jìn)行考察，假定有被標(biāo)記過的狀態(tài)對，則此狀態(tài)對用“×”來標(biāo)注，其所得結(jié)果如表3所示：

對剩下的沒有標(biāo)記的狀態(tài)對（s11，s12）也執(zhí)行上述操作步驟，得到的結(jié)果與表3相同，可區(qū)分狀態(tài)矩陣表不再有任何變化，循環(huán)結(jié)束，由此得到最終的可區(qū)分狀態(tài)矩陣表，如表3所示。

在表3中可以找出未標(biāo)記的狀態(tài)對（S11，S12）該狀態(tài)是等價的，從而可以得到最簡化的時序電路狀態(tài)轉(zhuǎn)換圖，如圖3所示：

由此可見001和011是同一狀態(tài)。化簡圖2中的時序電路圖所示的狀態(tài)轉(zhuǎn)換圖：也就是要刪除圖2中的狀態(tài)011，刪除后的狀態(tài)轉(zhuǎn)換圖即為圖3所示。狀態(tài)S00與S10即構(gòu)成了待驗證狀態(tài)對。S00的下一個狀態(tài)01與s10的下一個狀態(tài)001相匹配，在輸入0時即輸出都為l，在輸入1時即輸出都為0，因此叭與001即構(gòu)成了待驗證狀態(tài)對。狀態(tài)01和001在輸入1時輸出都為0，在輸入0時輸出都為1，下一個狀態(tài)分別是10和100。10和100匹配，在輸入0時輸出都為0，因此10和100為待驗證狀態(tài)對。它們的下一個狀態(tài)分別為s00和S10，而s00和s10已匹配成待驗證對。因此時序電路2中的狀態(tài)轉(zhuǎn)換圖的所有狀態(tài)已經(jīng)驗證結(jié)束，每一個待驗證狀態(tài)對的上一個狀態(tài)對和下一個狀態(tài)對都構(gòu)成了待驗證狀態(tài)對，所有的待驗證狀態(tài)對均是等價狀態(tài)對，因此圖1和圖2的狀態(tài)轉(zhuǎn)換圖所表示的時序電路是等價的。

5結(jié)束語

文中提出一種基于STG（狀態(tài)轉(zhuǎn)換圖）的并行驗證方法，并借鑒有限自動機(jī)并行最簡化原理，該方法利用并行算法將復(fù)雜的時序電路狀態(tài)轉(zhuǎn)換圖轉(zhuǎn)換成最簡化的時序電路，然后再驗證兩狀態(tài)轉(zhuǎn)換圖是否同構(gòu)即兩時序電路是否等價?？朔藚⒖嘉墨I(xiàn)[7]中采用遞歸的方法驗證兩狀態(tài)轉(zhuǎn)換圖是否同構(gòu)，減少了算法的時間復(fù)雜度。