Efficient state representation for symbolic simulation

ABSTRACT

Symbolic simulation is attracting increasing interest for the validation of digital circuits. It allows the verification engineer to explore all, or a major portion of the circuit's state space without having to design specific and time consuming test stimuli. However, the complexity and unpredictable run-time behavior of symbolic simulation have limited its scope to small-to-medium circuits.In this paper, we propose a novel approach to symbolic simulation that reduces the size of the BDDs of the state vector while maintaining an exact representation of the set of states visited. The method exploits the decomposition properties of Boolean functions. By restructuring the next-state functions in their disjoint support components, we gain a better insight in the role of each input variable. Consequently, we can simplify the next-state functions without significantly sacrificing the simulation accuracy. Our experimental results shows that this approach can be used in effectively reducing the memory requirements of symbolic simulation while surrendering only a small portion of the design's state space.

REFERENCES

• 1: Z. Barzilai, J. Carter, B. Rosen, and J. Rutledge. Hss- a high-speed simulator. IEEE Trans. on CAD/ICAS, pages 601--617, July 1987.
• 2: Craig Hansen, Hardware logic simulation by compilation, Proceedings of the 25th ACM/IEEE conference on Design automation, p.712-716, June 12-15, 1988, Atlantic City, New Jersey, United States
• 3: Randal E. Bryant, Graph-based algorithms for Boolean function manipulation, IEEE Transactions on Computers, v.35 n.8, p.677-691, Aug. 1986 [doi>10.1109/TC.1986.1676819]
• 4: In-Ho Moon , James H. Kukula , Kavita Ravi , Fabio Somenzi, To split or to conjoin: the question in image computation, Proceedings of the 37th conference on Design automation, p.23-28, June 05-09, 2000, Los Angeles, California, United States [doi>10.1145/337292.337305]
• 5: Kavita Ravi , Fabio Somenzi, High-density reachability analysis, Proceedings of the 1995 IEEE/ACM international conference on Computer-aided design, p.154-158, November 05-09, 1995, San Jose, California, United States
• 6: Gianpiero Cabodi , Paolo Camurati , Luciano Lavagno , Stefano Quer, Disjunctive partitioning and partial iterative squaring: an effective approach for symbolic traversal of large circuits, Proceedings of the 34th annual conference on Design automation, p.728-733, June 09-13, 1997, Anaheim, California, United States [doi>10.1145/266021.266355]
• 7: R. E. Bryant , D. Beatty , K. Brace , K. Cho , T. Sheffler, COSMOS: a compiled simulator for MOS circuits, Proceedings of the 24th ACM/IEEE conference on Design automation, p.9-16, June 28-July 01, 1987, Miami Beach, Florida, United States [doi>10.1145/37888.37890]
• 8: Jules P. Bergmann , Mark A. Horowitz, Improving coverage analysis and test generation for large designs, Proceedings of the 1999 IEEE/ACM international conference on Computer-aided design, p.580-583, November 07-11, 1999, San Jose, California, United States
• 9: Valeria Bertacco , Maurizio Damiani , Stefano Quer, Cycle-based symbolic simulation of gate-level synchronous circuits, Proceedings of the 36th ACM/IEEE conference on Design automation, p.391-396, June 21-25, 1999, New Orleans, Louisiana, United States [doi>10.1145/309847.309966]
• 10: Randal E. Bryant, Symbolic Boolean manipulation with ordered binary-decision diagrams, ACM Computing Surveys (CSUR), v.24 n.3, p.293-318, Sept. 1992 [doi>10.1145/136035.136043]
• 11: R. Ashenhurst. The decomposition of switching functions. In Proceedings of the International Symposium on the Theory of Switching, Part I 29, pages 74--116, 1957.
• 12: H. A. Curtis. A New Approach to the Design of Switching Circuits. Van Nostrand, Princeton, N.J., 1962.
• 13: 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
• 14: Fpga design by generalized functional decomposition. In T. Sasao, editor, Logic Synthesis and Optimization, chapter~11. Kluwer Academic, 1993.
• 15: CUDD-2.3.1. http://vlsi.Colorado.edu/~fabio.
• 16: O. Coudert , C. Berthet , J. C. Madre, Verification of synchronous sequential machines based on symbolic execution, Proceedings of the international workshop on Automatic verification methods for finite state systems, p.365-373, February 1990, Grenoble, France

INDEX TERMS

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

Additional Classification:
  B. Hardware
  B.6 LOGIC DESIGN
      B.6.3 Design Aids
          Subjects: Simulation
  B.8 Performance and Reliability

General Terms:
Design, Performance, Theory, Verification

Keywords:
BDDs, formal verification, symbolic simulation