BDDNOW: A Parallel BDD Package. BDDs (binary decision diagrams) are ubiquitous in formal verification tools, and the time and memory used by the BDD package is frequently the constraint that prevents application of formal verification. Accordingly, several researchers have investigated using parallel processing for BDDs. In this paper, we present a parallel BDD package with several novel features. The parallelization scheme strives for minimal communication overhead, so we are able to demonstrate speed-up even running on networked commodity PC workstations. Average memory utilization per node is comparable to that of efficient sequential packages. In addition, the package supports dynamic variable reordering, and simultaneous computation of multiple BDD operations. Finally, the package is designed for portability - providing a subset of the CUDD API for the application programmer, and running on the widely available PVM package.
Keywords for this software
References in zbMATH (referenced in 7 articles )
Showing results 1 to 7 of 7.
- Abujarad, F.; Kulkarni, S.S.: Automated constraint-based addition of nonmasking and stabilizing fault-tolerance (2011)
- Chung, Ming-Ying; Ciardo, Gianfranco: Speculative image computation for distributed symbolic reachability analysis (2011)
- Ezekiel, Jonathan; Lüttgen, Gerald: Measuring and evaluating parallel state-space exploration algorithms. (2008)
- Chung, Ming-Ying; Ciardo, Gianfranco: A pattern recognition approach for speculative firing prediction in distributed saturation state-space generation. (2006)
- Grumberg, Orna; Heyman, Tamir; Schuster, Assaf: A work-efficient distributed algorithm for reachability analysis (2006)
- Grumberg, Orna; Heyman, Tamir; Ifergan, Nili; Schuster, Assaf: Achieving speedups in distributed symbolic reachability analysis through asynchronous computation (2005)
- Ciardo, Gianfranco; Lüttgen, Gerald; Siminiceanu, Radu: Efficient symbolic state-space construction for asynchronous systems (2000)