Efficient techniques for verifying combinational circuits

Rapid advances in VLSI technology have led to increased complexity in current hardware designs. Therefore, checking for the correctness of operation has become an extremely difficult task. However, early detection of errors in designs is imperative in order to avoid higher production costs which are associated with the rectification of errors late in the design cycle or after the fabrication has been completed. Recently, formal verification techniques have gained a lot of importance as methods to mathematically prove the correctness of hardware systems. This research aims at developing a comprehensive framework for the efficient verification of combinational circuits. Towards achieving this goal, we have developed a novel technique called functional learning that can be used to analyze the relations among different gates in a logic circuit. We have developed three efficient combinational verification methodologies. The first technique is based on functional learning and uses a functional learning based Automatic Test Pattern Generation (ATPG) tool to verify two given circuits. Functional learning and Reduced Ordered Binary Decision Diagrams (ROBDDs) are combined in the second technique to build a powerful combinational verifier. The third technique uses a hash table to find functional equivalences among internal gates in two circuits. The equivalence checking is done using ROBDDs. Finally, building upon our experience in developing these three verification techniques and our knowledge of various core verification methodologies like ATPG and ROBDDs, we propose a comprehensive framework which combines various core techniques, novel re-synthesis-for-verification strategies and circuit and ROBDD partitioning. Special attention has been devoted to making the framework modular and amenable to easy extension by the addition of new techniques. We envision our framework forming the core of powerful verifiers for combinational circuits and feel that many of these techniques can be extended to the field of sequential circuit verification as well.