Simplifying Boolean constraint solving for random simulation-vector generation

ABSTRACT

We present an algorithm for simplifying the solution of conjunctive Boolean constraints of state and input variables, in the context of constrained random vector generation using BDDs. The basis of our approach is extraction of "hold-constraints" from constraint system. Hold-constraints are deterministic and trivially resolvable; in addition, they can be used to simplify the original constraints as well as refine the conjunctive partition. Experiments demonstrate significant reduction in the time and space needed for constructing the conjunction BDDs, and the time spent in vector generation during simulation.

REFERENCES

• 1: A. Aharon , B. Dorfman , E. Gofman , M. Leibowitz , V. Schwartzburd , A. Bar-David, Verification of the IBM RISC System/6000 by a dynamic biased pseudo-random test program generator, IBM Systems Journal, v.30 n.4, p.527-538, 1991
• 2: Valeria Bertacco , Maurizio Damiani, The disjunctive decomposition of logic functions, Proceedings of the 1997 IEEE/ACM international conference on Computer-aided design, p.78-82, November 09-13, 1997, San Jose, California, United States
• 3: D. Bochmann , F. Dresig , B. Steinbach, A new decomposition method for multilevel circuit design, Proceedings of the conference on European design automation, February 25-28, 1991, Amsterdam, The Netherlands
• 4: O. Coudert and J. C. Madre. A Unified Framework for the Formal Verification of Sequential Circuits. In Proc. Intl. Conf. on Computer-Aided Design, pages 126--129, November 1990.
• 5: Srinivas Devadas , Abhijit Ghosh , Kurt Keutzer, An observability-based code coverage metric for functional simulation, Proceedings of the 1996 IEEE/ACM international conference on Computer-aided design, p.418-425, November 10-14, 1996, San Jose, California, United States
• 6: Daniel Geist , Giora Biran , Tamara Arons , Michael Slavkin , Yvgeny Nustov , Monica Farkas , Karen Holtz , Andy Long , Dave King , Steve Barret, A methodology for the verification of a “system on chip”, Proceedings of the 36th ACM/IEEE conference on Design automation, p.574-579, June 21-25, 1999, New Orleans, Louisiana, United States [doi>10.1145/309847.310001]
• 7: J. Freeman, R. Duerden, C. Taylor, and M. Miller. The 68060 microprocessor functional design and verification methodology. In On-Chip Systems Design Conference, pages 10.1--10.14, 1995.
• 8: Kenneth L. McMillan, A Conjunctively Decomposed Boolean Representation for Symbolic Model Checking, Proceedings of the 8th International Conference on Computer Aided Verification, p.13-25, August 03, 1996
• 9: Alan Mishchenko , Bernd Steinbach , Marek Perkowski, An algorithm for bi-decomposition of logic functions, Proceedings of the 38th conference on Design automation, p.103-108, June 2001, Las Vegas, Nevada, United States [doi>10.1145/378239.378353]
• 10: Thomas R. Shiple , Ramin Hojati , Alberto L. Sangiovanni-Vincentelli , Robert K. Brayton, Heuristic minimization of BDDs using don't cares, Proceedings of the 31st annual conference on Design automation, p.225-231, June 06-10, 1994, San Diego, California, United States [doi>10.1145/196244.196360]
• 11: Bwolen Yang , Reid G. Simmons , Randal E. Bryant , David R. O'Hallaron, Optimizing Symbolic Model Checking for Constraint-Rich Models, Proceedings of the 11th International Conference on Computer Aided Verification, p.328-340, July 06-10, 1999
• 12: Jun Yuan , Kurt Shultz , Carl Pixley , Hillel Miller , Adnan Aziz, Modeling design constraints and biasing in simulation using BDDs, Proceedings of the 1999 IEEE/ACM international conference on Computer-aided design, p.584-590, November 07-11, 1999, San Jose, California, United States

INDEX TERMS

Primary Classification:
  I. Computing Methodologies
  I.1 SYMBOLIC AND ALGEBRAIC MANIPULATION
      I.1.2 Algorithms
          Subjects: Analysis of algorithms

Additional Classification:
  B. Hardware
  B.7 INTEGRATED CIRCUITS
      B.7.1 Types and Design Styles
          Subjects: Algorithms implemented in hardware

  G. Mathematics of Computing
  G.4 MATHEMATICAL SOFTWARE
      Subjects: Parallel and vector implementations

General Terms:
Algorithms, Theory