基本介紹
- 中文名：算術電路
- 外文名：arithmetic circuity
- 分類：工學
結合半加圖的算術電路等價性驗證技術,電路實現方案提取算法,HAG提取算法,結合HAG的算術電路驗證,算術電路的等價性驗證,加法樹構架提取,驗證框架,實驗結果,
結合半加圖的算術電路等價性驗證技術
為了克服現有等價性驗證技術難以快速驗證複雜算術電路的局限性，提出了一種利用綜合引擎分析並再現算術電路最佳化過程的算法。該算法結合了乘法器的編碼方式識別技術、加法電路的半加樹提取技術和部分積加法電路的架構識別技術來提取乘法電路的實現結構，以此生成與實現電路結構相似且邏輯正確的網表。針對算術電路結構的相似性，僅分析低位輸出的電路架構以降低算法複雜度。實驗結果表明，與傳統的算術電路驗證算法相比，該算法可以明顯提高算術電路的驗證速度，並且可以直接結合到現有的暫存器傳輸級(RTL)和門級網表的驗證流程中，從而提高了算術電路的驗證能力。
電路實現方案提取算法
算術電路架構識別算法中m、n為循環次數，m為啟發值。首先構建電路的AIG，其次選擇輸出out，提取所對應的HAG，根據HAG拓撲結構確定電路的實現方案Πi，記錄Πi出現次數，返回出現次數最多的Πi。乘法電路中的編碼邏輯會引入‘’異或‘’運算，這部分邏輯會干擾HAG的提取，因此應該對這部分邏輯進行預處理。
HAG提取算法
提取HAG是以AIG為基礎，構建AIG的偽代碼如下。
Algorithm create vetex(p1，p2){Special case preprocess；If Hash lookup(p1，p2)does not find vertex p {Create vertex p；Add p to Hash table;} Returnp；}
其中，p1、p2 是待新建節點的2個輸入節點，在構建節點p之前，首先對特殊情況進行預處理，如判斷p1、p2是否為常數節點或是否互相等價等；然後進行哈希查找，判別待構建節點是否已經存在，如果存在則直接合併同構節點，反之則新建節點p；每個新建節點都將加入到一個哈希表中，此哈希表使用節點p的輸入p1、p2屬性作為關鍵字。
提取原始電路中的‘’異或‘’(XOR)關係。由AIG容易提取出大部分‘’異或‘’關係。因為A∧B =!(A∧～B)，所以還需要提取‘’異或非‘’(XNOR)關係。在提取出大部分‘’異或‘’(或‘’異或非‘’)運算後，剩餘的少量‘’異或‘’關係可以由可滿足性問題(satisfiabilityproblem，SAT)引擎和二值決策圖(binary decisiondiagram，BDD)引擎輔助得到。
根據已得‘’異或‘’關係尋找輸入對應的進位邏輯，添加半加器或全加器，同時需要注意由於常數輸入而引起的全加器退化。例如，對於全加器的實現邏輯為
sum=a∧b∧cin，cout=a&b+b &cin+cin &a，當cin=1時，其實現邏輯將退化為sum=～(a∧b)，cout=a+b。
在AIG上標記已經匹配的節點，由已得HAG繼續增量式地匹配未被匹配區域直至完成。若遇到加法部分的局部最佳化引起無法直接匹配加法器，則回溯電路，找出它對應的I集合，然後找出該集合對應的‘’和‘’節點，根據推論變化對應的HAG的結構，對電路進行局部擴展，直至其對應的輸出可以與未匹配的部分電路匹配。
結合HAG的算術電路驗證
算術電路是等價性驗證領域的瓶頸，商業工具為單獨驗證算術模組提供了黑匣子技術，用戶可以設定算術電路的實現方案。當用戶不了解算術模組的實現方案時，在黑匣子技術基礎上，算法可以直接結合到現有的RTL和門級網表的驗證流程。該流程不僅對乘法電路有效，對於其他以加法為基本實現單元的算術電路，只須進行HAG架構的提取，即可得到實現架構的相關信息。
在讀入的實現電路中選擇低5、6位的輸出作為起點，回溯電路構建AIG，同時標記各 節點對應的輸出編號，分組節點。分析高位輸出對應的輸入集合，根據電路性質確定電路的編碼方式。由輸出回溯電路，在AIG上提取‘’異或‘’關係，對乘法電路進行預處理，匹配半加器建立HAG，繼而識別原始運算元的性質，得到HAG架構。根據得到的編碼方式和HAG架構綜合參考電路，獲得與實現電路結構相似的參考電路網表。當提取編碼方式和HAG架構時，估算m×n(m>n)的並行乘法器的算法複雜度：乘法器涉及的加法器數目為О(m ×n)，m ×n個部分積的位。搜尋的輸出為5、6位，涉及的加法器個數為常數，並且這樣的搜尋是一次性的，因此該複雜度在實際的電路設計中可以忽略。根據這些特徵信息，綜合引擎可以生成與實現電路結構相似的網表，從而提高等價性驗證的效率。
算術電路的等價性驗證
提出了一種利用綜合引擎重現算術電路的最佳化過程的算法，提高了等價性驗證效率。ZDVF的綜合引擎首先識別乘法器的編碼方式，提取部分積的加法樹實現方案；然後根據這些信息生成與實現電路結構相似且邏輯正確的網表。算法可直接結合到現有的RTL和門級網表的驗證流程中，從而提高算術電路的驗證能力。
加法樹構架提取
乘法器的加法樹輸出在組織結構上具有相似性，因此只需針對部分低位輸出提取加法樹。由半加器的位置和運算元的性質即可識別加法樹的構架。
wallance tree結構的加法樹可由CSA(斜進位加法器，carry一save adder)實現，最後 一次輸出終值的加法採用了帶進位鏈的高速加法器。遠離輸出的CSA的運算元大多為部分積，而靠近輸出部分的CSA的運算元都基本是前級加法器的進位與和位。在陣列乘法器中其全加器的運算元除最後一次終值輸出之外，運算元都包括了I，S和C。從而可區分出乘法器的不同加法構架。實驗中，提取了低六位輸出的加法樹就可區分出不同的加法樹構架。
驗證框架
算術電路是等價性驗證領域的瓶頸，商業工具為單獨驗證算術模組提供了黑匣子(blackbox)技術，用戶通過其可設定算術電路的實現方案。當用戶對算術模組的實現方案不了解時，算法可在黑匣子技術基礎上，直接結合到現有的TRL和門級網表的驗證流程中。在提取編碼方式和加法樹構架時，估算m*n(>mn)的並行乘法器的算法複雜度：乘法器涉及到的加法器的數目為0(mn)，mn個部分積的位。搜尋的輸出為3～6位，涉及到的加法器個數為常數，並且這樣的搜尋是一 次性的，因此該複雜度在實際的電路設計中可忽略。根據這些特徵信息，綜合引擎可生成與實現電路結構相似的網表，從而提高等價性驗證的效率。
實驗結果
算法在ZDFV的邏輯綜合引擎上實現，分析實現電路，提取特徵信息並生成與實現電路的具有相同實現方案的網表。測試平台是Snu的Ultra一Sparc60工作站，其配置為雙CPU，ZG記憶體。乘法器的實現有CSA陣列乘法器，Wallace tree乘法器。
提取電路特徵時間，消耗集中於加法圖的提取，但該時間並不正比於電路規模。FORMALITY的驗證時間，實現電路是以對應實現方案實現的乘法電路，參考電路分別是陣列結構乘法器和引擎相應實現的綜合結果。當乘法器的位數達到14位時的網表檔案，FoRMALITY運行時間過長，所以給出的電路規模只到12位。算法還實驗了各種類型的表達式和乘法結構，有符號的、無符號的及布希算法，結果類似。
