Monitoring the Effects of Static Variable Orders on the Construction of BDDs

The increasing complexity of modern Integrated Circuits (ICs) results in more bug occurrences during their design. In this regard, formal verification techniques such as the methods based on Binary Decision Diagrams (BDDs) mathematically ensure the correctness of these ICs before fabrication. However, BDDs are very sensitive to input variable ordering. Most of the time, the construction of BDDs fails due to size explosion caused by unfavorable input variable ordering. A lot of research has been done in the past to find a good variable ordering method; however, the focus has always been on the endsize of BDDs which may not present the whole picture. In this paper, we present a framework to monitor the BDD size during construction. We argue that in addition to the endsize, the highest number of nodes, i.e. the peaksize, should also be taken into account when selecting the static variable ordering method. The proposed framework uses a variable order generator to compute an input variable order for a circuit and a BDD generator, with CUDD at its heart, to monitor important parameters in particular peaksize. With the help of the framework, we observe how popular static variable ordering heuristics affect the peaksize and endsize of BDDs using popular benchmark sets, i.e., ISCAS85, ISCAS89.