Constraint synthesis for environment modeling in functional verification

ABSTRACT

Modeling design environment with constraints instead of a traditional testbench is advantageous in a hybrid verification framework that encompasses simulation and formal verification. This movement is gaining popularity in industry and sparks research in the constraint-based environment modeling and stimulus generation problem. We present an approach, called constraint synthesis, to this problem. Constraint synthesis falls in the general category of parametric Boolean equation solving but is novel in utilizing don't care information unique to hardware constraints and heuristic variable removal to simplify the solution. Experimental results have demonstrated the effectiveness of the proposed approach.

REFERENCES

• 1: O. Coudert and J. C. Madre. A Unified Framework for the Formal Verification of Sequential Circuits. In Proceedings of International Conference on Computer-Aided Design, pages 126--129, November 1990.
• 2: M. Fujita, Y. Tamiya, Y. Kukimoto, and K.-C. Chen. Application of Boolean Unification to Combinational Logic Synthesis. Proceedings of International Conference on Computer-Aided Design, pages 510--513, 1991.
• 3: Matt Kaufmann , Andrew Martin , Carl Pixley, Design Constraints in Symbolic Model Checking, Proceedings of the 10th International Conference on Computer Aided Verification, p.477-487, June 28-July 02, 1998
• 4: 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
• 5: Hee Hwan Kwak , In-Ho Moon , James H. Kukula , Thomas R. Shiple, Combinational equivalence checking through function transformation, Proceedings of the 2002 IEEE/ACM international conference on Computer-aided design, p.526-533, November 10-14, 2002, San Jose, California [doi>10.1145/774572.774650]
• 6: C-J. H. Segar M. D. Aagaard, R. B. Jones. Formal verification using parametric represenations of boolean constraints. Proceedings of the Design Automation Conference, 1996.
• 7: Ursula Martin , Tobias Nipkow, Boolean unification—the story so far, Journal of Symbolic Computation, v.7 n.3-4, p.275-293, March/April 1989 [doi>10.1016/S0747-7171(89)80013-6]
• 8: C. Pixley. Integrating Model Checking Into the Semiconductor Design Flow. Computer Design's Electronic Systems journal, pages 67--74, March 1999.
• 9: 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.
• 10: 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]
• 11: Wolfram Büttner , Helmut Simonis, Embedding Boolean expressions into logic programming, Journal of Symbolic Computation, v.4 n.2, p.191-205, Oct. 1987 [doi>10.1016/S0747-7171(87)80065-2]
• 12: 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]
• 13: 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:
  J. Computer Applications
  J.6 COMPUTER-AIDED ENGINEERING

General Terms:
Algorithms, Verification

Keywords:
constraint solving, simulation vector generation