應用不可滿足子式的解碼電路綜合優化方法*

張建民，黎鐵軍，馬柯帆，肖立權

(國防科技大學 計算機學院， 湖南 長沙 410073)

?

應用不可滿足子式的解碼電路綜合優化方法*

張建民，黎鐵軍，馬柯帆，肖立權

(國防科技大學 計算機學院， 湖南 長沙 410073)

解釋布爾公式不可滿足的原因在很多領域都具有實際的應用需求，而最小不可滿足子式能夠為諸如電路的自動綜合等應用領域中的不可滿足原因提供最精確的解釋。因此，將兩種能夠高效求解最小不可滿足子式的算法——分支-限界算法與貪心遺傳算法，集成到解碼電路的自動綜合工具中。采用通信領域的標準編碼電路作為測試集，將兩種算法進行對比。實驗結果表明，在運行時間與每秒剔除的短句數方面，貪心遺傳算法優于分支-限界算法；不可滿足子式在解碼電路的自動綜合過程中發揮重要作用。

電路綜合；形式化方法；可滿足性求解；不可滿足子式

在超大規模集成(Very Large Scale Integrated， VLSI)電路芯片中，通常都會設計各種各樣的編碼和解碼電路，尤其是在與通信相關的芯片設計過程中，往往會遇到很多非常復雜的編碼與解碼電路。編碼電路通常根據某種規則將原始數據編碼或產生校驗碼，常見的包括循環冗余校驗(Cyclic Redundancy Code，CRC)或糾錯碼(Error Correction Code，ECC)，而解碼電路根據校驗碼和原始數據判定接收的數據是否正確。這些電路需要消耗設計者大量的時間來進行驗證，那么，能否只設計與驗證編碼電路，而后通過一種自動化的方法來產生正確的解碼電路，從而降低設計者的工作量？……