A Framework for Constrained Functional Verification

ABSTRACT

We describe a framework for constrained simulation-vector generationin an industry setting. The framework consists of two keycomponents: the constraint compiler and the vector generator. Theconstraint compiler employs various techniques, including prioritization,partitioning, extraction, and decomposition, to minimize theinternal representation of the constraints, and thus the complexityof constraint solving. The vector generator then uses the compileddata together with input biasing to generate random simulation vectors.Constraints and input biases are treated in a unified manner inthe vector generator. Although there are many alternative ways ofgenerating vectors from constraints, the framework uniquely suits apractical constrained verification environment because of its abilityto handle complicated constraints and its seamless treatment of constraintsand biases. We illustrate the effectiveness of the frameworkwith real examples from commercial designs.

REFERENCES

• 1: Catriel Beeri , Ronald Fagin , David Maier , Mihalis Yannakakis, On the Desirability of Acyclic Database Schemes, Journal of the ACM (JACM), v.30 n.3, p.479-513, July 1983 [doi>10.1145/2402.322389]
• 2: [2] T. Bengtsson, A. Martinelli, and E. Dubrova. A Fast Heuristic Algorithm for Disjoint Decomposition of Boolean Functions. Proc. Intl. Workshop on Logic Synthesis , pages 51-55, 2002.
• 3: 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
• 4: 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
• 5: [5] 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.
• 6: E. V. Dubrova , J. C. Muzio , B. von Stengel, Finding composition trees for multiple-valued functions, Proceedings of the 27th International Symposium on Multiple-Valued Logic (ISMVL '97), p.19, May 28-30, 1997
• 7: Georg Gottlob , Nicola Leone , Francesco Scarcello, A Comparison of Structural CSP Decomposition Methods, Proceedings of the Sixteenth International Joint Conference on Artificial Intelligence, p.394-399, July 31-August 06, 1999
• 8: Marc Gyssens , Peter G. Jeavons , David A. Cohen, Decomposing constraint satisfaction problems using database techniques, Artificial Intelligence, v.66 n.1, p.57-89, March 1994 [doi>10.1016/0004-3702(94)90003-5]
• 9: James H. Kukula , Thomas R. Shiple, Building Circuits from Relations, Proceedings of the 12th International Conference on Computer Aided Verification, p.113-123, July 15-19, 2000
• 10: [10] C. Pixley. Integrating Model Checking Into the Semiconductor Design Flow. Computer Design's Electronic Systems journal, pages 67-74, March 1999.
• 11: [11] S. Regimbal, J-F. Lemire, Y. Savaria, G. Bois, E-M. Aboulhamid, and A. Baron. Applying aspect-oriented programming to hardware verification with e. Proceedings of HDLCON, 2002.
• 12: [12] N. Robertson and P. D. Seymour. Graph minors. ii. algorithmic aspects of tree-width. Journal of Algorithms, pages 7:309-322, 1986.
• 13: Kanna Shimizu , David L. Dill, Deriving a simulation input generator and a coverage metric from a formal specification, Proceedings of the 39th conference on Design automation, June 10-14, 2002, New Orleans, Louisiana, USA [doi>10.1145/513918.514118]
• 14: Robert E. Tarjan , Mihalis Yannakakis, Simple linear-time algorithms to test chordality of graphs, test acyclicity of hypergraphs, and selectively reduce acyclic hypergraphs, SIAM Journal on Computing, v.13 n.3, p.566-579, August 1984 [doi>10.1137/0213035]
• 15: Jun Yuan , Ken Albin , Adnan Aziz , Carl Pixley, Simplifying Boolean constraint solving for random simulation-vector generation, Proceedings of the 2002 IEEE/ACM international conference on Computer-aided design, p.123-127, November 10-14, 2002, San Jose, California [doi>10.1145/774572.774590]
• 16: Jun Yuan , Ken Albin , Adnan Aziz , Carl Pixley, Constraint synthesis for environment modeling in functional verification, Proceedings of the 40th conference on Design automation, June 02-06, 2003, Anaheim, CA, USA [doi>10.1145/775832.775909]
• 17: 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:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.4 Processors
          Subjects: Compilers

Additional Classification:
  B. Hardware
  B.7 INTEGRATED CIRCUITS
      B.7.2 Design Aids
          Subjects: Verification; Simulation

General Terms:
Algorithms, Performance, Verification