邏輯等效驗證在超大型積體電路設計的流程中，扮演十分重要的角色。近年來有論文指出驗證所花費的時間在整個電路設計中約佔百分之六十至百分之八十的比例。因此，一個有效率的演算法是必須的。因此，利用機率方法來驗證邏輯等效被提出。過去的方法是將要驗證的電路轉換成機率表示式，再比較此表示式是否相等即可。近來，將機率表示式中的符號替換成實數可以得出此電路輸出端的機率，並且證明此替換之方式，其驗證之結果不會產生失真。但是當電路的輸入端的數目過大時，這種替換變數的方式將需要極大的計算量及記憶體使用量。因此，我們提出了一個方式，是利用電路中的內部等價閘，來減少變數取代的使用量。而實驗的數據也指出我們的方法在實際的電路是可行的。

Logic equivalence checking plays an important role in VLSI design flow. Recently, the effort of logic equivalence checking occupies 60%~80% effort of the whole design flow. Hence, an efficient algorithm for logic equivalence checking is needed and probabilistic verification is proposed. Probability expressions of circuits are built and compared. Recently, replacing primary inputs into real numbers is used. In [8], a perfect input assignment for probabilistic verification is proposed and this approach does not cause aliasing. But this input assignment approach needs plenty of calculation and memory usage while the input number is huge. Hence, we propose an advanced approach to reduce the usage of input assignments. We check internal equivalent gates of circuits and replace them with a single assignment. Experimental results show that our approach is workable in practical circuits.

[1] V. D. Agrawal and S. Seth, “Mutually Disjoint Signals and Probability Calculation in Digital Circuits,” in Proc. the Great Lakes Symposium on VLSI, pp. 307-312, 1998.
[2] R. E. Bryant, “Graph-based Algorithm for Boolean Function Manipulation,” IEEE Transaction on Computer-Aided Design, C-35:667-691, August 1986.
[3] M. Blum, A. Chandra, and M. Wegman, “Equivalence of Free Boolean Graphs Can be Decided Probabilistically in Polynomial Time,” Information Processing Letters, 10:80-82, March 1980.
[4] S. C. Chang, L. P. P. P Van Ginneken, and M. Marek-Sadowska, “Fast Boolean Optimization by Rewiring,” in Proc. IEEE Int. Conf. Computer-Aided Design, pp. 262-269, 1996.
[5] J. Jain, J. Bitner, D. S. Fussel, and J. A. Abraham, “Probabilistic Design Verification,” in Proc. IEEE Int. Computer-Aided Design, pp. 468-471, 1991.
[6] S. K. Kumar and M. A. Breuer, “Probabilistic Aspects of Boolean Switching Functions via a New Transform,” Journal of the Association for Computing Machinery, Vol 28, No 3, pp. 502-520, July 1981.
[7] H. B. Min and E. S. Park, “Graph-theoretic Algorithm for Finding Maximal Supergates in Combinational Logic Circuits,” in Proc. IEE. Circuits, Devices and Systems, Vol. 143, No. 6, December 1996.
[8] K. P. Parker and E. J. McCluskey, “Probabilistic Treatment of General Combinational Networks,” IEEE Transaction Comput., pp. 668-670, 1975.
[9] M. Teslenko, E. Dubrova, and H. Tenhunen, “Computing a Perfect Input Assignment for Probabilistic Verification,” in Proc. SPIE, VLSI Circuits and Systems II, Vol. 5837, pp. 929-936, June 2005.