A survey of techniques for formal verification of combinational circuits
---
paper_title: Efficient Representation and Manipulation of Switching Functions Based on Ordered Kronecker Functional Decision Diagrams

paper_content:

An efficient package for construction of and operation on ordered Kronecker Functional Decision Diagrams (OKFDD) is presented. OKFDDs are a generalization of OBDDs and OFDDs and as such provide a more compact representation of the functions than either of the two decision diagrams. In this paper basic properties of OKFDDs and their efficient representation and manipulation are presented. Based on the comparison of the three decision diagrams for several benchmark functions, a 25% improve ment in size over OBDDs is observed for OKFDDs.
---
paper_title: Probabilistic verification of Boolean functions

paper_content:

We present a novel method for verifying the equivalence of two Boolean functions. Each function is hashed to an integer code by assigning random integer values to the input variables and evaluating an integer-valued transformation of the original function. The hash codes for two equivalent functions are always equal. Thus the equivalence of two functions can be verified with a very low probability of error, which arises from unlikely “collisions” between inequivalent functions. An upper bound, ∈, on the probability of error is known a priori. The bound can be decreased exponentially by making multiple runs. Results indicate significant time and space advantages for this method over techniques that represent each function as a single OBDD. Some functions known to require space (and time) exponential in the number of input variables for these techniques require only polynomial resources using our method. Experimental results indicate that probabilistic verification can provide an attractive alternative for verifying functions too large to be handled using these OBDD-based techniques.
---
paper_title: Efficient construction of binary moment diagrams for verifying arithmetic circuits

paper_content:

BDD-based approaches cannot handle some arithmetic functions such as multiplication efficiently, while Binary Moment Diagrams proposed by Bryant and Chen (1994) provide compact representations for those functions. They reported a BMD-based polynomial-time algorithm for verifying multipliers. This approach requires high-level information such as specifications to subcomponents. This paper presents a new technique called backward construction which can construct BMDs directly from circuit descriptions without any high-level information. The experiments show that the computation time for verifying for n-bit multipliers is approximately n/sup 4/. We have successfully verified 64-bit multipliers of several type in 3-6 hours with 46 Mbyte of memory on SPARCstation 10/51. This result outperforms previous BDD-based approaches for verifying multipliers.
---

Title: A Survey of Techniques for Formal Verification of Combinational Circuits

Section 1: Introduction
Description 1: Provide an overview of the need for formal verification in the design of complex digital systems, the limitations of simulation-based approaches, and the objectives of the survey.

Section 2: Methods Based on Decision Diagrams
Description 2: Describe the use of decision diagrams such as Binary Decision Diagrams (BDDs) in formal verification, including their structure, canonical properties, and techniques to address memory explosion problems.

Section 3: Node Decompositions
Description 3: Discuss various node decomposition methods like Shannon, Reed-Muller, and Kronecker decompositions, including the use of Ordered Functional Decision Diagrams (OFDDs) and Ordered Kronecker Functional Decision Diagrams (OKFDDs).

Section 4: Partitioned ROBDDs
Description 4: Explain the concept of partitioned ROBDDs for more compact and efficient Boolean function representation and their application in reducing memory requirements and enhancing verification efficiency.

Section 5: Combining Bottom-up and Top-down approaches of ROBDD construction
Description 5: Discuss hybrid methods that combine bottom-up and top-down approaches to minimize intermediate peak memory requirements during ROBDD construction.

Section 6: Probabilistic Verification
Description 6: Outline probabilistic methods for verifying circuit equivalence using random assignments and arithmetic transformations, and discuss their efficiency and error probability.

Section 7: Verification of Arithmetic Circuits
Description 7: Describe strategies for verifying arithmetic circuits beyond bit-level approaches, including the use of Hybrid Decision Diagrams (HDDs) and *BMDs for word-level representation and hierarchical verification techniques.

Section 8: Learning Techniques: Detecting Indirect Implications
Description 8: Cover learning techniques such as Recursive Learning (RL) and Functional Learning (FL) for detecting indirect implications and internal equivalences in digital circuits.

Section 9: Techniques for Exploiting Internal Equivalences
Description 9: Explore methods that leverage internal correspondences between networks, including min-cut algorithms, cross-controllability, cross-observability, and ATPG-based techniques for internal equivalence checking.

Section 10: Learning Based Verification Techniques
Description 10: Discuss recent learning-based verification tools like HANNIBAL and VERIFUL, their methodologies, limitations, and effectiveness in combinational verification.

Section 11: BDD Hash Based Techniques
Description 11: Explain BDD hash-based techniques for identifying equivalent internal gates and discuss their integration with learning algorithms and ATPG techniques to verify complex networks.