Verifying sequential equivalence using ATPG techniques

ABSTRACT

In this paper we address the problem of verifying the equivalence of two sequential circuits. State-of-the-art sequential optimization techniques such as retiming and sequential redundancy removal can handle designs with up to hundreds or even thousands of flip-flops. However, the BDD-based approaches for verifying sequential equivalence can easily run into memory explosion for such designs. In an attempt to handle larger circuits, we modify test pattern-generation techniques for verification. The suggested approach utilizes the popular efficient backward-justification technique used in most sequential ATPG programs. We present several techniques to enhance the efficiency of this approach by (1) identifying equivalent flip-flop pairs using an induction-based algorithm, and (2) generalizing the idea of exploring the structural similarity between circuits to perform verification in stages. This ATPG-based framework is suitable for verifying circuits either with or without a reset state. In order to extend this approach to verify retimed circuits, we introduce a delay-compensation-based algorithm for preprocessing the circuits. The experimental results of verifying the correctness of circuits after sequential redundancy removal and retiming with up to several hundred flip-flops are presented.

REFERENCES

• 1: ABRAMOVICI, M., BREUER,M.A.,AND FRIEDMAN, A. D. 1990. Digital System Testing And Testable Design. IEEE Computer Society Press, Los Alamitos, CA.
• 2: BERTHET, C., COUDERT, O., AND MADRE, J. C. 1990. New ideas on symbolic manipulations of finite state machines. In Proceedings of the International Conference on Computer-Aided Design. 224-227.
• 3: Daniel Brand, Verification of large synthesized designs, Proceedings of the 1993 IEEE/ACM international conference on Computer-aided design, p.534-537, November 07-11, 1993, Santa Clara, California, United States
• 4: Daniel Brand , Reinaldo A. Bergamaschi , Leon Stok, Be careful with don't cares, Proceedings of the 1995 IEEE/ACM international conference on Computer-aided design, p.83-86, November 05-09, 1995, San Jose, California, United States
• 5: CHENG, K.-T. 1993. Redundancy removal for sequential circuits without reset states. IEEE Trans. Comput.-Aided Des. (Jan.), 652-667.
• 6: K.-T. Cheng , H.-K. T. Ma, On the over-specification problem in sequential ATPG algorithms, Proceedings of the 29th ACM/IEEE conference on Design automation, p.16-21, June 08-12, 1992, Anaheim, California, United States
• 7: CHENG, W.-T. 1988. The BACK algorithm for sequential test generation. In Proceedings of the International Conference on Computer Design (ICCD '88). 66-69.
• 8: CHO, H., JEONG,S.W.,SOMENZI, F., AND PIXLEY, C. 1993. Synchronizing sequences and symbolic traversal techniques in test generation. J. Electron. Test. 4, 1 (Feb.), 19-31.
• 9: 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
• 10: DEVADAS, S., MA, H.-K. T., AND SANGIOVANNI-VINCENTELLI, A. 1988. Logic verification, testing, and their relationship io logic synthesis. In Testing and Diagnosis of VLSI and ULSI. Kluwer Academic Publishers, Hingham, MA, 181-246.
• 11: GLAESER,U.AND VIERHAUS, H. T. 1996. Mixed-level test generation for synchronous sequential circuits using the FOGBUSTER algorithm. IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst. 15, 4 (Apr.), 410-423.
• 12: GOEL, P. 1981. An implicit enumeration algorithm to generate tests for combinational logic circuits. IEEE Trans. Comput. C-30 (Mar.), 215-222.
• 13: LEISERSON,C.E.AND SAXE, J. B. 1991. Retiming synchronous circuitry. Algorithmica 6,1, 5-35.
• 14: MALIK, S., SENTOVICH, E., BRAYTON, R., AND SANGIOVANNI-VINCENTELLI, A. 1991. Retiming and resynthesis: Optimizing sequential networks with combinational techniques. IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst. 10, 1 (Jan.), 74-84.
• 15: Aiman El-Maleh , Thomas Marchok , Janusz Rajski , Wojciech Maly, On test set preservation of retimed circuits, Proceedings of the 32nd ACM/IEEE conference on Design automation, p.176-182, June 12-16, 1995, San Francisco, California, United States [doi>10.1145/217474.217526]
• 16: Ralph A. Marlett, EBT: A comprehensive test generation technique for highly sequential circuits, Proceedings of the 15th conference on Design automation, p.335-339, June 19-21, 1978, Las Vegas, Nevada, United States
• 17: MCCLUSKEY, E. J. 1965. Introduction To The Theory Of Switching Circuits. McGraw-Hill, Inc., Hightstown, NJ.
• 18: PIXLEY, C. 1992. Theory and implementation of sequential hardware equivalence. IEEE Trans. Comput.-Aided Des. 11, 12 (Dec.), 1469-1494.
• 19: Carl Pixley , Vigyan Singhal , Adnan Aziz , Robert K. Brayton, Multi-level synthesis for safe replaceability, Proceedings of the 1994 IEEE/ACM international conference on Computer-aided design, p.442-449, November 06-10, 1994, San Jose, California, United States
• 20: Irith Pomeranz , Sudhakar M. Reddy, On Achieving Complete Testability of Synchronous Sequential Circuits with Synchronizing Sequences, Proceedings of the IEEE International Test Conference on TEST: The Next 25 Years, p.1007-1016, October 02-06, 1994
• 21: SENTOVICH, E., SINGH, K., LAVAGNO, L., MOON, C., MURGAI, R., SALDANHA, A., SAVOJ, H., STEPHAN, P., BRAYTON, R., AND SANGIOVANNI-VINCENTELLI, A. 1992. SIS: A system for sequential circuit synthesis. Tech. Rep. UCB/ERL M92/41. UC Berkeley, Berkeley, CA.
• 22: Narendra Shenoy , Richard Rudell, Efficient implementation of retiming, Proceedings of the 1994 IEEE/ACM international conference on Computer-aided design, p.226-233, November 06-10, 1994, San Jose, California, United States
• 23: Vigyan Singhal , Carl Pixley , Richard L. Rudell , Robert K. Brayton, The validity of retiming sequential circuits, Proceedings of the 32nd ACM/IEEE conference on Design automation, p.316-321, June 12-16, 1995, San Francisco, California, United States [doi>10.1145/217474.217548]
• 24: TOUATI,H.J.,SAVOJ, H., LIN, B., BRAYTON,R.K.,AND SANGIOVANNI-VINCENTELLI, A. 1990. Implicit state enumeration of finite state machines using BDDs. In Proceedings of the IEEE International Conference on Computer-Aided Design (ICCAD'90, Nov.). IEEE Computer Society Press, Los Alamitos, CA, 130-133.

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.1 Design Styles
          Subjects: Sequential circuits