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

Application of DAG-Aware MIG Rewriting Technique in Logic Synthesis and Verification

王立為(Li-Wei Wang)

指導教授 ： 黃鐘揚

國立臺灣大學/電機資訊學院/電子工程學研究所/碩士(2016年)

https://doi.org/10.6342/NTU201601708

摘要

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

關鍵字

眾數反向圖 ； 邏輯合成 ； 資料路徑驗證

並列摘要

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.

並列關鍵字

Majority-Inverter Graph ； Logic Synthesis ； Datapath Verification

參考文獻

[6] Alan Mishchenko, Satrajit Chatterjee, and Robert Brayton, “Dag-aware aig rewriting a fresh look at combinational logic synthesis,” in Proceedings of the 43rd annual Design Automation Conference. ACM, 2006, pp. 532–535.

[8] Daniel Brand, “Verification of large synthesized designs,” in The Best of ICCAD, pp. 65–72. Springer, 2003.

[11] Randal E Bryant, “Graph-based algorithms for boolean function manipulation,” IEEE Transactions on computers, vol. 100, no. 8, pp. 677–691, 1986.

[14] Grigori S Tseitin, “On the complexity of derivation in propositional calculus,” in Automation of reasoning, pp. 466–483. Springer, 1983.

[15] Demosthenes Anastasakis, Lisa McIlwain, and Slawomir Pilarski, “Efficient equivalence checking with partitions and hierarchical cut-points,” in Proceedings of the 41st annual Design Automation Conference. ACM, 2004, pp. 539–542.