BDD minimization using don't cares for formal verification and logic synthesis
Youpyo Hong · University of Southern California Digital Library · 2017
Computer-aided design (CAD) tools have been an essential means to cope with the enormous complexity of designing, verifying, and testing very large scale integrated (VLSI) circuits. Efficient representation and manipulation of Boolean logic functions is crucial in most CAD applications and binary decision diagrams (BDDs) have proven to be an extremely useful representation because they are canonical and typically very compact. For BDD-based tools, the size of the BDD representations often determine their run-time, the problem size that they can handle, and/or the quality of the circuits they synthesize. BDD size reduction, therefore, has been an intensive area of research. One of the approaches to reducing BDD size is to utilize the flexibility of the function to be represented from don't care conditions such as unused state codes or impossible input patterns. It is the goal of this dissertation to explore techniques and applications of BDD minimization using don't cares. This dissertation addresses two basic questions about BDD minimization using don't cares: (1) how to minimize BDDs using don't cares and (2) how/where to use DC-based BDD minimization. First, we develop new don't care-based BDD minimization heuristics which are significantly more powerful than traditional heuristics. Then we demonstrate that don't care-based BDD minimization can significantly improve the performance of symbolic reachability analysis tools. Finally, we describe how to derive don't cares and utilize the don't cares for BDD-based software synthesis.