眾數反向圖改寫技術在邏輯合成與驗證之應用

Abstract

眾數反向圖是近年來提出的一種邏輯電路表示法，他將邏輯電路用眾數函數與反向函數組合而成；他的代數與布林特性讓他在邏輯優化的操作上非常有效率，比起目前最先進的方法，眾數反向圖的演算法可以得到更佳的結果。在這篇論文中，我們將無圈有向改寫技術鑲嵌進眾數反向圖，並將其應用在邏輯合成與驗證領域。在邏輯合成方面，實驗結果顯示高度優化的眾數反向圖仍可被我們的演算法再優化；在資料路徑驗證方面，我們的演算法可以提高資料路徑分析的品質，並有效的減少正規驗證所需的時間。

A Majority-Inverter Graph (MIG) is a recently introduced logic representation form which manipulates logic by using only 3-input majority function (MAJ) and inversion function (INV). Its algebraic and Boolean properties enables efficient logic optimizations. In particular, MIG algorithms obtained significantly superior synthesis results as compared to the state-of-the-art approaches based on AND-inverter graphs and commercial tools. In this thesis, we integrate the DAG-aware rewriting technique, a fast greedy algorithm for circuit compression, into MIG and apply it not only in the logic synthesis but also verification. Experimental results on logic optimization show that heavily-optimized MIGs can be further reduced by 20.4% of network size while depth preserved. Experimental results on datapath verification also show the effectiveness of our algorithm. With our MIG rewriting applied, datapath analysis quality can be improved with the ratio 3.16. Runtime for equivalence checking can also be effectively reduced.