Verification of Combinational Circuits Using Conjunctively Decomposed Implications

This paper presents an efficient formal logic verification algorithm for combinational circuits. Our method utilizes the general implication among internal signals conjunctively decomposed in compact BDD forms, which leads to more efficient and robust verification. Furthermore, unlike other methods using BDD, our method is less susceptible to structural difference between the two circuits compared to each other. A cutset is chosen between inputs and outputs of the joint composition of two compared circuits. Then the general implication is computed from logic relations between inputs and internal signals on the cutset. The implication is conjunctively decomposed as in [McM96] or approximately in compact forms and subsequently applied to the equivalence output checking relation represented by internal signals on the cutset. We show algorithms of the implication decomposition and utilization. Experimental results show its potential advantage -- multipliers can be verified with BDD in the ..