Speichereffizienter Aufbau von binären Entscheidungsdiagrammen [Memory-Efficient Construction of Binary Decision Diagrams]

It is necessary to develop more efficient data structures and associated verification algorithms to ensure correct behavior of increasingly complex hardware systems. A suitable data structure is a Binary Decision Diagram (BDD) because it can represent Boolean functions compactly and enables efficient algorithms to manipulate them. However, BDDs have challenges to overcome: practicability depends on their minimization and the reduction of large memory requirements for some complex functions.

This book presents approaches in which Boolean normal forms are ordered based on rules of Boolean algebra with the goal of minimizing the number of intermediate computations to build BDDs thereby reducing memory usage and required runtime. The approaches are integrated into a software package in order to evaluate their performance against state-of-the-art strategies.

Download here