Partitioned ROBDDs - a compact, canonical and efficiently manipulable representation for Boolean functions

We presenta new representationfor Boolean functions called PartitionedROBDDs. In this representation we divide the Boolean space into `k' partitions and represent a function over each partition as a separate ROBDD. We show that partitioned-ROBDDs are canonical and can be efficiently manipulated. Further, they can be exponentially more compact than monolithic ROBDDs and even Free BDDs. Moreover, at any given time, only one partition needs to be manipulated which further increases the space efficiency. In addition to showing the utility of partitioned-ROBDDs on special classes of functions, we provide automatic techniques for their construction. We show that for large circuits our techniques are more efficient in space as well as time over monolithic ROBDDs. Using these techniques,some complex industrial circuits could be verified for the first time.

• Type: Conference
• Year: 1996
• Where: ICCAD
• Authors: Amit Narayan, Jawahar Jain, Masahiro Fujita, Alberto L. Sangiovanni-Vincentelli
• Keywords: Boolean Space, Hardware, ICCAD 1996, Monolithic Robdds, Representationfor Boolean Functions