Bdd partitioning for formal verification and synthesis of digital systems
Amit Narayan, Alberto Luigi Sangiovanni-Vincentelli · 1998
Reduced Ordered Binary Decision Diagrams (ROBDDs) are extensively used in various VLSI-CAD algorithms as a representation for Boolean functions. However, the complexity of the problems that can be solved using these algorithms is usually limited by the fact that the ROBDDs of many functions can require space which is exponential in the number of variables. This large space requirement of ROBDDs is commonly known as the problem. This dissertation addresses the ROBDD memory explosion problem in the context of digital system verification and synthesis. BDD partitioning is proposed as an effective way of dealing with this problem. The first part of the dissertation focuses on formal verification of digital systems. A new representation for Boolean functions called partitioned-ROBDDs is proposed. In this representation the Boolean space is divided into 'k' partitions and the function is represented as a separate ROBDD over each partition. It is shown that partitioned-ROBDDs are canonical and efficiently manipulable. In addition, for many functions they are exponentially more compact than ROBDDs. Moreover, different partitions can be processed independently and only one partition needs to be present in the memory at any given time which further increases the space efficiency. In addition to the theoretical discussion of the properties of partitioned-ROBDDs, their utility in formal verification of combinational and sequential circuits is demonstrated by means of experiments. Since ROBDDs and partitioned-ROBDDs are canonical representations of Boolean functions, they can be directly used to check the equivalence of two combinational circuits. A mixed bottom-up/top-down procedure for memory efficient construction of ROBDDs is proposed. This procedure aims at reducing the intermediate memory requirement by first introducing suitable decomposition points and then finding a good order of composition to obtain the ROBDD representation of the outputs of a Boolean netlist. Automatic techniques to construct partitioned-ROBDDs representing the outputs of combinational circuits and the set of reachable states of sequential circuits are also presented. In both cases, partitioned-ROBDDs show a substantial reduction in total memory utilization over ROBDDs. In the case of combinational verification, partitioned-ROBDDs are able to verify many circuits for which ROBDDs fail. These include some complex industrial circuits which could be verified for the first time using these techniques. Similarly, in the case of sequential circuits, for a given memory limit, partitioned-ROBDDs can complete traversal for many circuits for which ROBDDs fail. For circuits where both partitioned-ROBDDs as well as monolithic ROBDDs cannot complete traversal, partitioned-ROBDDs can reach a significantly larger set of states. The second part of the dissertation focuses on logic synthesis. A new application of ROBDDs, in the synthesis of pass-transistor circuits, is proposed and the ROBDD memory explosion problem is studied in this context. It is shown that Pass-transistor logic (PTL) can be a promising alternative to static CMOS for deep sub-micron designs. A comprehensive synthesis flow for PTL designs is outlined which utilizes the fact that ROBDDs can be directly mapped into PTL circuits. Decomposed-ROBDDs are proposed as a suitable logic level representation for multi-stage PTL circuits. Although not canonical, decomposed-ROBDDs do not suffer from the memory explosion problem associated with monolithic ROBDDs. A set of algorithms to synthesize PTL circuits optimized for area, delay and power using this representation are proposed.