Constraints in one-to-many concretization for abstraction refinement

ABSTRACT

In one-to-many concretization for model checking based on abstraction refinement, constraints on input vectors that are pseudo-randomly generated are often essential to the success of the procedure. These constraints have to do with both primary inputs and invisible state variables. We discuss algorithms that address both types and we show their effectiveness through experiments.

REFERENCES

• 1: P. Bjesse and J. Kukula. Using counter example guided abstraction refinement to find complex bugs. In Proceedings of the Conference on Design, Automation and Test in Europe, pages 156--161, Feb. 2004.
• 2: R. K. Brayton et al. VIS: A system for verification and synthesis. In T. Henzinger and R. Alur, editors, Eighth Conference on Computer Aided Verification (CAV'96), pages 428--432. Springer-Verlag, Rutgers University, 1996. LNCS 1102.
• 3: F. M. de Paula and A. Hu. An effective guidance strategy for abstraction-guided simulation. In Proceedings of the Design Automation Conference, pages 63--68, San Diego, CA, June 2007.
• 4: D. Kroening and G. Weissenbacher. Counterexamples with loops for predicate abstraction. In Computer-Aided Verification, pages 152--165, Aug. 2006.
• 5: R. P. Kurshan. Computer-Aided Verification of Coordinating Processes. Princeton University Press, Princeton, NJ, 1994.
• 6: R. Milner. An algebraic definition of simulation between programs. Proc. 2nd Int. Joint Conf. on Artificial Intelligence, pages 481--489, 1971.
• 7: K. Nanshi and F. Somenzi. Guiding simulation with increasingly refined abstract traces. In Proceedings of the Design Automation Conference, pages 737--742, San Francisco, CA, July 2006.
• 8: K. Nanshi and F. Somenzi. Improved visibility in one-to-many trace concretization. In Design Automation and Test in Europe, pages 819--824, Munich, Germany, Mar. 2008.
• 9: URL: http://www.opencores.org.
• 10: S. Shyam and V. Bertacco. Distance-guided hybrid verification with GUIDO. In Proceedings of the Conference on Design, Automation and Test in Europe, pages 1211--1216, Munich, Germany, 2006.
• 11: URL: http://vlsi.colorado.edu/~vis.
• 12: C. Wang, A. Gupta, and F. Ivancic. Induction in CEGAR for detecting counterexamples. In Formal Methods in Computer Aided Design, pages 77--84, Nov. 2007.
• 13: C. Wang, B. Li, H. Jin, G. D. Hachtel, and F. Somenzi. Improving Ariadne's bundle by following multiple threads in abstraction refinement. In Proceedings of the International Conference on Computer-Aided Design, pages 408--415, Nov. 2003.
• 14: W. Wu and M. S. Hsiao. Efficient design validation based on cultural algorithms. In Proceedings of the Conference on Design, Automation and Test in Europe, pages 402--407, Mar. 2008.

INDEX TERMS

Primary Classification:
  B. Hardware
  B.6 LOGIC DESIGN
      B.6.3 Design Aids
          Subjects: Verification

General Terms:
Algorithms, Verification

Keywords:
abstraction refinement, model checking, simulation