Variable order verification use of logic representation

Abstract

Boolean functions are fundamental to synthesis and verification of digital logic, and compact representations of Boolean functions have great practical significance. Conversion between those representations is common, especially when one is used to represent the input and another speeds up relevant algorithms. In the last 15 years, a number of applications based on efficient manipulation of Boolean functions gained industrial significance, notably in automated design and verification of logic circuits. The efficient representation and manipulation of Boolean functions is important for many algorithms in a wide variety of applications in particular, many problems in computer-aided design for digital circuits (CAD). The efficiency of the Boolean manipulation depends on the form of representation of the Boolean function. It is unavoidable and important problem to find a variable ordering which minimize the size of a BDD, since variable ordering has a great influence on the computation time and storage requirements for Boolean function manipulation number of times each variable takes part in the Logic operation to obtain the best possible the variable order. This paper describes a technique for finding the best variable ordering by analyzing the logic gate representation in the given Boolean function. Algorithm starts with initial variable ordering. The system will check each sub expression to find out the number times each variable takes part in each type of logic operations. The number of occurrences for each variable will be stored and then all the totals are arranged in descending order to identify the variable ordering for that Boolean function. If more than one input variables have the same total then a special criteria will be used to break the tie: We present graph-based evidence of the improvement obtained by using highly effective logical verification based variable ordering technique for BDDs. It is shown that the effectiveness of the Decision Diagram is mainly depending on the variable ordering selected. It is not practical to have any unique ordering for a given Boolean function and it can be selected among the number of best results, what will be more appropriate with the design. This new technique, easy to implement and automate, consistently creates high quality variable ordering for Boolean function.