基于自動機最簡化的時序電路等價性驗證方法

張留宛

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

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

中圖分類號：TP301 文獻標識碼：A

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

1概述

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

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

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

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

3時序電路等價性定義

時序電路等同于自動機理論中的有限狀態(tài)機。有限狀態(tài)機是表示有限個狀態(tài)與在狀態(tài)之間的轉移和動作等行為的數(shù)學模型，可以用其來描述時序電路系統(tǒng)的輸入輸出。本文采用Mealy型狀態(tài)機來描述時序電路。Mealy型狀態(tài)機描述如下：路上的輸入符號均產(chǎn)生相同的輸出符號。由此得出兩個狀態(tài)是否等價需滿足的條件是：①在所有的輸入條件下，兩個狀態(tài)所對應的輸出是相同的;②在所有的輸入條件下，兩個狀態(tài)的轉移結果相同。等價狀態(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)的可達狀態(tài)空間形成的子狀態(tài)轉換圖來表示時序電路。兩時序電路是否等價的驗證等同于驗證兩時序電路對應的狀態(tài)轉換圖是否同構。如何判斷兩狀態(tài)轉換圖是否同構，就是在一個狀態(tài)轉換圖上隨意取一頂點均能在另一狀態(tài)轉換圖上找出與之等價的頂點，由此可以推斷出兩個狀態(tài)轉換圖所表示的時序電路是等價的。

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

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

對于一個時序電路的狀態(tài)轉換圖如圖2，構造一個可區(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)用“一”來進行標記，其他的表項用空來標記。圖2相對應的可區(qū)分狀態(tài)矩陣表結構如下表1所示：

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

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

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

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

由此可見001和011是同一狀態(tài)?；唸D2中的時序電路圖所示的狀態(tài)轉換圖：也就是要刪除圖2中的狀態(tài)011，刪除后的狀態(tài)轉換圖即為圖3所示。狀態(tài)S00與S10即構成了待驗證狀態(tài)對。S00的下一個狀態(tài)01與s10的下一個狀態(tài)001相匹配，在輸入0時即輸出都為l，在輸入1時即輸出都為0，因此叭與001即構成了待驗證狀態(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)轉換圖的所有狀態(tài)已經(jīng)驗證結束，每一個待驗證狀態(tài)對的上一個狀態(tài)對和下一個狀態(tài)對都構成了待驗證狀態(tài)對，所有的待驗證狀態(tài)對均是等價狀態(tài)對，因此圖1和圖2的狀態(tài)轉換圖所表示的時序電路是等價的。

5結束語

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