《面向通訊套用的自動對偶綜合方法研究》是依託中國人民解放軍國防科技大學，由沈勝宇擔任項目負責人的面上項目。
基本介紹
- 中文名：面向通訊套用的自動對偶綜合方法研究
- 項目類別：面上項目
- 項目負責人：沈勝宇
- 依託單位：中國人民解放軍國防科技大學
中文摘要,結題摘要,
中文摘要
通訊套用是半導體工業的主要推動力之一。在通訊晶片設計項目中，耗時最長且最容易出錯的工作，在於設計和驗證通訊協定棧的對偶電路。本項目的目標在於，在我們發表於ICCAD'09的初步研究成果基礎上，提出全新的理論框架，以自動產生對偶電路的暫存器傳輸級(RTL)代碼，從而提升通訊晶片的設計質量，並縮短設計周期。為達到上述目標，將從以下方面開展研究：首先，通過引進可滿足性模(SMT)方法，提升算法抽象層次，以降低算法時間開銷，並提升結果可讀性；其次，提出弱化的最終唯一概念，以支持對多參數組複雜電路進行對偶綜合；再次，提出基於時態變數劃分的解枚舉算法，以改善對偶電路的時序和面積；最後，提出面向冗餘數據流的對偶綜合算法，以提高對偶電路的可靠性。本項目提出的理論框架和實現技術，能極大的提升通訊晶片的設計效率和質量，具有重大的學術價值和套用前景。
結題摘要
在本項目執行期間，獲得了以下主要研究成果。 1、在我們發表於ICCAD09的原始對偶綜合算法基礎上，增加對環形路徑條件的檢測公式，將解碼器在有限長度上不存在的結論，擴展到無限長路徑上，從而解決了原始算法不停機的問題。研究成果發表於IEEE Transaction on CAD of Integrated Circuits and Systems(TCAD),2011年第10期。 2、提出了自動推導外部斷言的算法，以減少用戶手工工作。該算法疊代的運行成果1的算法，使用每次疊代中產生的SAT公式，求解並剔除解碼器不存在的外部斷言。有限狀態假設保證了該算法的停機性。研究成果發表於International Conference on Computer Aided Design(ICCAD11)。 3、提出了全新算法以發掘多個同時存在的解碼器及其對應斷言。該算法疊代的構造函式依賴問題的SAT公式，以檢查當現有已發掘的解碼器集合具有相同的輸出時，是否能夠導致所有潛在解碼器的混合SAT公式具有不同的輸出。若是，則表明仍然存在尚未被發掘的解碼器，而混合SAT公式在外部配置信號集合的解上的投影，即為新的解碼器的遷移關係。該算法疊代運行直至函式依賴問題的SAT公式不可滿足為止。研究成果發表於IEEE Transaction on CAD of Integrated Circuits and Systems(TCAD),2012年第8期。 4、提出基於Craig插值的特徵化算法，以加快生成解碼器的速度。該算法構造遷移關係的不可滿足SAT公式，並從SAT求解器產生的resolution序列中產生解碼器的布爾函式。該算法也發表於IEEE Transaction on CAD of Integrated Circuits and Systems(TCAD),2012年第8期。 5、由於本小組的開創性工作，使得對偶綜合引起了國際學術界的關注和跟進研究。自2011年以來，在EDA領域的頂級會議ICCAD[4]和DAC[6]，以及頂級期刊IEEE Transaction on CAD of Integrated Circuits and Systems[5]上共發表了3篇來自其他研究小組的論文。這些工作給出了意想不到的發現，是對我們研究工作的巨大推進和有益補沖。
