Advertisement

Maximal Input Reduction of Sequential Netlists via Synergistic Reparameterization and Localization Strategies

  • Jason Baumgartner
  • Hari Mony
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3725)

Abstract

Automatic formal verification techniques generally require exponential resources with respect to the number of primary inputs of a netlist. In this paper, we present several fully-automated techniques to enable maximal input reductions of sequential netlists. First, we present a novel min-cut based localization refinement scheme for yielding a safely overapproximated netlist with minimal input count. Second, we present a novel form of reparameterization: as a trace-equivalence preserving structural abstraction, which provably renders a netlist with input count at most a constant factor of register count. In contrast to prior research in reparameterization to offset input growth during symbolic simulation, we are the first to explore this technique as a structural transformation for sequential netlists, enabling its benefits to general verification flows. In particular, we detail the synergy between these input-reducing abstractions, and with other transformations such as retiming which – as with traditional localization approaches – risks substantially increasing input count as a byproduct of its register reductions. Experiments confirm that the complementary reduction strategy enabled by our techniques is necessary for iteratively reducing large problems while keeping both proof-fatal design size metrics – register count and input count – within reasonable limits, ultimately enabling an efficient automated solution.

Keywords

Model Check Primary Input Register Count Register Reduction Input Reduction 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. 1.
    Jain, P., Gopalakrishnan, G.: Efficient symbolic simulation-based verification using the parametric form of Boolean expressions. IEEE Transactions on CAD (April 1994)Google Scholar
  2. 2.
    Aagaard, M.D., Jones, R.B., Seger, C.-J.H.: Formal verification using parametric representations of Boolean constraints. In: Design Automation Conference (June 1999)Google Scholar
  3. 3.
    Bertacco, V., Olukotun, K.: Efficient state representation for symbolic simulation. In: Design Automation Conference (June 2002)Google Scholar
  4. 4.
    Moon, I.-H., Kwak, H.H., Kukula, J., Shiple, T., Pixley, C.: Simplifying circuits for formal verification using parametric representation. In: Aagaard, M.D., O’Leary, J.W. (eds.) FMCAD 2002. LNCS, vol. 2517. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  5. 5.
    Chauhan, P., Clarke, E.M., Kroening, D.: A SAT-based algorithm for reparameterization in symbolic simulation. In: Design Automation Conference (June 2004)Google Scholar
  6. 6.
    Mador-Haim, S., Fix, L.: Input elimination and abstraction in model checking. In: Gopalakrishnan, G.C., Windley, P. (eds.) FMCAD 1998. LNCS, vol. 1522, pp. 304–320. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  7. 7.
    Jin, H., Kuehlmann, A., Somenzi, F.: Fine-grain conjunction scheduling for symbolic reachability analysis. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, p. 312. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  8. 8.
    Chauhan, P., Clarke, E., Kukula, J., Sapra, S., Veith, H., Wang, D.: Automated abstraction refinement for model checking large state spaces using SAT based conflict analysis. In: Aagaard, M.D., O’Leary, J.W. (eds.) FMCAD 2002. LNCS, vol. 2517. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  9. 9.
    Kuehlmann, A., Baumgartner, J.: Transformation-based verification using generalized retiming. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, p. 104. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  10. 10.
    Wang, D., Ho, P.-H., Long, J., Kukula, J.H., Zhu, Y., Ma, H.-K.T., Damiano, R.F.: Formal property verification by abstraction refinement with formal, simulation and hybrid engines. In: Design Automation Conference (June 2001)Google Scholar
  11. 11.
    Wang, D.: SAT based Abstraction Refinement for Hardware Verification. PhD thesis, Carnegie Mellon University (May 2003)Google Scholar
  12. 12.
    van Eijk, C.A.J.: Sequential equivalence checking without state space traversal. In: Design, Automation, and Test in Europe (March 1998)Google Scholar
  13. 13.
    Kuehlmann, A., Paruthi, V., Krohm, F., Ganai, M.: Robust Boolean reasoning for equivalence checking and functional property verification. IEEE Transactions on CAD (December 2002)Google Scholar
  14. 14.
    Mony, H., Baumgartner, J., Paruthi, V., Kanzelman, R.: Exploiting suspected redundancy without proving it. In: Design Automation Conference (June 2005)Google Scholar
  15. 15.
    Grumberg, O., Long, D.E.: Model checking and modular verification. ACM Transactions on Programming Languages and System 16(3) (1994)Google Scholar
  16. 16.
    Ford, L.R., Fulkerson, D.R.: Maximal flow through a network. Canadian Journal of Mathematics 8 (1956)Google Scholar
  17. 17.
    Fisler, K., Vardi, M.: Bisimulation and model checking. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 338–342. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  18. 18.
    Kukula, J.H., Shiple, T.R.: Building circuits from relations. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  19. 19.
    Awedh, M., Somenzi, F.: Increasing the robustness of bounded model checking by computing lower bounds on the reachable states. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 230–244. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  20. 20.
    Clarke, E., Gupta, A., Kukula, J., Strichman, O.: SAT based abstraction-refinement using ILP and machine learning techniques. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, p. 265. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  21. 21.
    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
  22. 22.
    Gupta, A., Ganai, M., Yang, Z., Ashar, P.: Iterative abstraction using SAT-based BMC with proof analysis. In: Int’l. Conference on Computer-Aided Design (November 2003)Google Scholar
  23. 23.
    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
  24. 24.
    Leiserson, C., Saxe, J.: Retiming synchronous circuitry. Algorithmica 6 (1991)Google Scholar
  25. 25.
    Baumgartner, J., Heyman, T., Singhal, V., Aziz, A.: An abstraction algorithm for the verification of level-sensitive latch-based netlists. Formal Methods in System Design (23) (2003)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Jason Baumgartner
    • 1
  • Hari Mony
    • 1
  1. 1.IBM Systems & Technology GroupAustin

Personalised recommendations