Efficient Symbolic Simulation via Dynamic Scheduling, Don’t Caring, and Case Splitting

  • Viresh Paruthi
  • Christian Jacobi
  • Kai Weber
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3725)


Most computer-aided design frameworks rely upon building BDD representations from netlist descriptions. In this paper, we present efficient algorithms for building BDDs from netlists. First, we introduce a dynamic scheduling algorithm for building BDDs for gates of the netlist, using an efficient hybrid of depth- and breadth-first traversal, and constant propagation. Second, we introduce a dynamic algorithm for optimally leveraging constraints and invariants as don’t-cares during the building of BDDs for intermediate gates. Third, we present an automated and complete case splitting approach which is triggered by resource bounds. Unlike prior work in case splitting which focused upon variable cofactoring, our approach leverages the full power of our don’t-caring solution and intelligently selects arbitrary functions to apply as constraints to maximally reduce peak BDD size while minimizing the number of cases to be explored. While these techniques may be applied to enhance the building of BDDs for arbitrary applications, we focus on their application within cycle-based symbolic simulation. Experiments confirm the effectiveness of these synergistic approaches in enabling optimal BDD building with minimal resources.


  1. 1.
    Aagaard, M.D., Jones, R.B., Seger, C.-J.H.: Formal verification using parametric representations of Boolean constraints. In: DAC (1999)Google Scholar
  2. 2.
    Aloul, F.A., Markov, I.L., Sakallah, K.A.: Improving the efficiency of Circuit-to-BDD conversion by gate and input ordering. In: ICCD (2002)Google Scholar
  3. 3.
    Baumgartner, J., Kuehlmann, A., Abraham, J.: Property checking via structural analysis. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, p. 151. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  4. 4.
    Baumgartner, J., Mony, H.: Maximal input reduction of sequential netlists via synergistic reparameterization and localization strategies. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol. 3725, pp. 222–237. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  5. 5.
    Bertacco, V., Damiano, M., Quer, S.: Cycle-based symbolic simulation of gate-level synchronous circuits. In: Design Automation Conference (June 1999)Google Scholar
  6. 6.
    Bertacco, V., Olukotun, K.: Efficient state representation for symbolic simulation. In: Design Automation Conference (June 2002)Google Scholar
  7. 7.
    Bryant, R.E.: Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys 24(3) (September 1992)Google Scholar
  8. 8.
    Chauhan, P., Clarke, E., Kroening, D.: A SAT-based algorithm for reparameterization in symbolic simulation. In: Design Automation Conference (June 2004)Google Scholar
  9. 9.
    Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  10. 10.
    Coudert, O., Berthet, C., Madre, J.: Verification of synchronous sequential machines based on symbolic execution. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407. Springer, Heidelberg (1990)Google Scholar
  11. 11.
    Hong, Y., Beerel, P.A., Burch, J.R., McMillan, K.L.: Safe BDD minimization using don’t cares. In: Design Automation Conference (June 1997)Google Scholar
  12. 12.
  13. 13.
    Jacobi, C., Weber, K., Paruthi, V., Baumgartner, J.: Automatic formal verification of fused-multiply-add floating point units. In: DATE (2005)Google Scholar
  14. 14.
    Janssen, G.: Design of a pointerless bdd package. In: IWLS (2001)Google Scholar
  15. 15.
    Jin, H.-S., Awedh, M., Somenzi, F.: CirCUs: A satisfiability solver geared towards bounded model checking. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 519–522. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  16. 16.
    Kuehlmann, A., Paruthi, V., Krohm, F., Ganai, M.: Robust Boolean reasoning for equivalence checking and functional property verification. IEEE Trans. CAD 21(12) (2002)Google Scholar
  17. 17.
    Kurshan, R.P.: Computer-Aided Verification of Coordinating Processes. Princeton University Press, Princeton (1994)Google Scholar
  18. 18.
    Mony, H., Baumgartner, J., Paruthi, V., Kanzelman, R., Kuehlmann, A.: Scalable automated verification via expert-system guided transformations. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 159–173. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  19. 19.
    Murgai, R., Jain, J., Fujita, M.: Efficient scheduling techniques for ROBDD construction. In: VLSI Design, pp. 394–401 (1999)Google Scholar
  20. 20.
    Ochi, H., Yasuoka, K., Yajima, S.: Breadth-first manipulation of very large binary-decision diagrams. In: International Conference on Computer-Aided Design (1993)Google Scholar
  21. 21.
    Sanghavi, J.V., Ranjan, R.K., Brayton, R.K., Sangiovanni-Vincentelli, A.L.: High performance BDD package by exploiting memory hiercharchy. In: DAC, pp. 635–640 (1996)Google Scholar
  22. 22.
    Wilson, C., Dill, D.L., Bryant, R.E.: Symbolic simulation with approximate values. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 335–353. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  23. 23.
    Yang, B., Chen, Y.-A., Bryant, R.E., O’Hallaron, D.R.: Space- and time-efficient BDD construction via working set control. In: ASP-DAC, pp. 423–432 (1998)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Viresh Paruthi
    • 1
  • Christian Jacobi
    • 2
  • Kai Weber
    • 2
  1. 1.IBM Systems GroupAustin
  2. 2.IBM Deutschland Entwicklung GmbHBoeblingenGermany

Personalised recommendations