Optimizing sequential verification by retiming transformations

ABSTRACT

Sequential verification methods based on reachability analysis are still limited by the size of the BDDs involved in computations. Extending their applicability to larger and real circuits is still a key issue. Within this framework, we explore a new way to improve symbolic traversal performance, working on the representation of state sets. We exploit retiming to reduce the number of latches of a FSM, and to relocate them in order to obtain a simplified state set representation. We consider retiming as a temporary state space transformation to increase the efficiency of sequential verification. We discuss it as a state space transformation and we formally analyze the conditions under which such a transformation is equivalence preserving for a given property under verification. We lower image computation cost, and we reduce the size of BDDs representing intermediate results and state sets. Experimental results show considerable memory and time improvements on some benchmark and home made circuits.

REFERENCES

• 1: Dominik Stoffel , Wolfgang Kunz, Record & play: a structural fixed point iteration for sequential circuit verification, Proceedings of the 1997 IEEE/ACM international conference on Computer-aided design, p.394-399, November 09-13, 1997, San Jose, California, United States
• 2: G. P. Bischoff, Formal implementation verification of the bus interface unit for the Alpha 21264 microprocessor, Proceedings of the 1997 International Conference on Computer Design (ICCD '97), p.16, October 12-15, 1997
• 3: Rajeev K. Ranjan , Vigyan Singhal , Fabio Somenzi , Robert K. Brayton, Using combinational verification for sequential circuits, Proceedings of the conference on Design, automation and test in Europe, p.32-es, January 1999, Munich, Germany [doi>10.1145/307418.307476]
• 4: Jason Baumgartner , Tamir Heyman , Vigyan Singhal , Adnan Aziz, Model Checking the IBM Gigahertz Processor: An Abstraction Algorithm for High-Performance Netlists, Proceedings of the 11th International Conference on Computer Aided Verification, p.72-83, July 06-10, 1999
• 5: Aarti Gupta , Pranav Ashar , Sharad Malik, Exploiting Retiming in a Guided Simulation Based Validation Methodology, Proceedings of the 10th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, p.350-353, September 27-29, 1999
• 6: C. Legl, P. Vanbekbergen, and A. Wang. Retiming of Edge-Triggered Circuits with Multiple Clocks and Load Enables. In IWLS'99: IEEE International Workshop on Logic Synthesis, May 1999.
• 7: K. Ravi. Improvements to Reachability Analysis. Unpublished manuscript, October 1997.
• 8: Gianpiero Cabodi , Paolo Camurati , Stefano Quer, Improved reachability analysis of large finite state machines, Proceedings of the 1996 IEEE/ACM international conference on Computer-aided design, p.354-360, November 10-14, 1996, San Jose, California, United States
• 9: Kavita Ravi , Fabio Somenzi, Hints to accelerate Symbolic Traversal, Proceedings of the 10th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, p.250-264, September 27-29, 1999

INDEX TERMS

Primary Classification:
  J. Computer Applications

Additional Classification:
  B. Hardware
  B.7 INTEGRATED CIRCUITS

  C. Computer Systems Organization

General Terms:
Design, Experimentation, Measurement, Performance, Theory, Verification