Combinational Equivalence Checking for Threshold Logic Circuits

Threshold logic is gaining prominence as an alternative to Boolean logic. The main reason for this trend is the availability of devices that implement these circuits efficiently (current mode, differential mode circuits) as well as the promise they hold for the future nano devices (RTDs, SETs, QCAs and other nano devices). Threshold networks can provide a seamless transition from CMOS to post-CMOS technologies. This has generated renewed interest in the design automation community to design efficient CAD tools for threshold logic. Recently a lot of work has been done to synthesize threshold logic circuits. So far there has been no efficient method to verify the synthesized circuits. Therefore, there is a need to develop tools for the synthesis, verification and optimization of threshold logic networks. Researchers at Arizona State University have developed the first efficient procedure to determine the logic function of a threshold gate. It is the first work that identifies the problem of equivalence checking for threshold logic circuits. This work formulates the problem and provides a polynomial complexity procedure that can be used with the rest of the verification infrastructure currently used by the industry (Boolean Equation Diagrams, etc.) The procedure is provably correct and has polynomial total complexity. It generates a maximally factored form representation of the logic function, which is very compact. This results in the significant speed-up (1.25x to 16x) when equivalence checking is done using Boolean Equation Diagrams (BED). Moreover the maximally factored form generated is that of a minimal SOP (which is the complete sum for a unate function). This results in much smaller representation using BEDs. Potential Applications Future Nano-Scale Devices Resonant Tunneling Diodes Single Electron Transistor Quantum Cellular Automata Benefits and Advantages Can implement complex functions Fewer gates less area Fewer levels less delay Achieves up to 189X improvement in runtime (on average 23X) Generates a (provably) maximally factored form Gives up to two orders speed-up when compared to alternative method Could verify circuits that conventional approaches could not Download Original PDF