Sequential optimization in the absence of global reset

ABSTRACT

We study the problem of optimizing synchronous sequential circuits. There have been previous efforts to optimize such circuits. However, all previous attempts make implicit or explicit assumptions about the design or the environment of the design. For example, it is widespread practice to assume the existence of a hardware reset line and consequently a fixed power-up state; in the absence of the same, a common premise is that the design's environment will apply an initializing sequence. We review the concept of safe replaceability which does away with these assumptions and the delay-safe replaceability notion, which is applicable when the design's output is not used for a certain number of cycles after power-up. We then develop procedures for optimizing the combinational next-state and output logic, as well as routines for reencoding the state space and removing state bits under these replaceability criteria. Experimental results demonstrate the effectiveness of our algorithms.

REFERENCES

• 1: Berry, G. and Touati, H. J. 1993. Optimized controller synthesis using Esterel. In Workshop Notes of International Workshop on Logic Synthesis (Tahoe City, CA, May).
• 2: Berthet, C., Coudert, O., and Madre, J. C. 1990. New Ideas on symbolic manipulation of finite state machines. In Proceedings of the International Conference on Computer Design (Cambridge, MA, October) 224--227.
• 3: Robert King Brayton , Alberto L. Sangiovanni-Vincentelli , Curtis T. McMullen , Gary D. Hachtel, Logic Minimization Algorithms for VLSI Synthesis, Kluwer Academic Publishers, Norwell, MA, 1984
• 4: Brayton, R. K., Hachtel, G. D., and Sangiovanni-Vincentelli, A. L. 1990. Multilevel logic synthesis. Proc. IEEE 78, 2 (Feb.), 264--300.
• 5: Cerny, E. and Marin, M. A. 1977. An approach to unified methodology of combinational switching circuits. IEEE Trans. Comput. 27, 8.
• 6: Cheng, K.-T. 1993. Redundancy removal for sequential circuits without reset states. IEEE Trans. Comput.-Aided Des. Integ. Circ. 12, 1 (Jan.), 13--24.
• 7: Cho, H., Hachtel, G. D., Jeong, S.-W., Plessier, B., Schwarz, E., and Somenzi, F. 1990. ATPG aspects of FSM verification. In Proceedings of the International Conference on Computer-Aided Design (Santa Clara, CA, November), 134--137.
• 8: Coudert, O. and Madre, J. C. 1990. A Unified framework for the formal verification of sequential circuits. In Proceedings of the International Conference on Computer-Aided Design (Santa Clara, CA, November), 126--129.
• 9: Luis Entrena , Kwang-Ting Cheng, Sequential logic optimization by redundancy addition and removal, Proceedings of the 1993 IEEE/ACM international conference on Computer-aided design, p.310-315, November 07-11, 1993, Santa Clara, California, United States
• 10: Juris Hartmanis, Algebraic structure theory of sequential machines (Prentice-Hall international series in applied mathematics), Prentice-Hall, Inc., Upper Saddle River, NJ, 1966
• 11: Kunz, W. and Pradhan, D. 1994. Recursive learning: A precise implication procedure and its application to test verification and and optimization. IEEE Trans. Comput. Aided Des. Integ. Circ. Syst. (Sept.).
• 12: Bill Lin, Synthesis of VLSI designs with symbolic techniques, University of California at Berkeley, Berkeley, CA, 1992
• 13: Lin, B. 1993. Efficient symbolic support manipulation. In Proceedings of the International Conference on Computer Design (Cambridge, MA, October), 513--516.
• 14: Lin, B., Touati, H. J., and Newton, A. R. 1990. Don't care minimization of multi-level sequential logic networks. In Proceedings of the International Conference on Computer-Aided Design (Santa Clara, CA, November), 414--417.
• 15: A. Mehrotra , S. Qadeer , V. Singhal , R. K. Brayton , A. Aziz , A. L. Sangiovanni-Vincentelli, Sequential optimisation without state space exploration, Proceedings of the 1997 IEEE/ACM international conference on Computer-aided design, p.208-215, November 09-13, 1997, San Jose, California, United States
• 16: Carl Pixley, Introduction to a Computational Theory and Implementation of Sequential Hardware Equivalence, Proceedings of the 2nd International Workshop on Computer Aided Verification, p.54-64, June 18-21, 1990
• 17: Pixley, C. 1992. A theory and implementation of sequential hardware equivalence. IEEE Trans. Comput.-Aided Des. Integ. Circ. 11, 12 (Dec.), 1469--1494.
• 18: 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
• 19: I. Pomeranz , S. M. Reddy, Classification of Faults in Synchronous Sequential Circuits, IEEE Transactions on Computers, v.42 n.9, p.1066-1077, September 1993 [doi>10.1109/12.241596]
• 20: Irith Pomeranz , Sudhakar M. Reddy, On Removing Redundancies from Synchronous Sequential Circuits with Synchronizing Sequences, IEEE Transactions on Computers, v.45 n.1, p.20-32, January 1996 [doi>10.1109/12.481483]
• 21: Shaz Qadeer , Robert K. Brayton , Vigyan Singhal, Latch Redundancy Removal Without Global Reset, Proceedings of the 1996 International Conference on Computer Design, VLSI in Computers and Processors, p.432-439, October 07-09, 1996
• 22: Saldanha, A., Villa, T., Brayton, R. K., and Sangiovanni-Vincentelli, A. L. 1994. Satisfaction of input and output encoding constraints. IEEE Trans. Comput. Aided Des. Integ. Circ. 13, 5 (May), 589--602.
• 23: Savoj, H. and Brayton, R. K. 1991. Observability relations and observability don't cares. In Proceedings of the International Conference on Computer-Aided Design (Santa Clara, CA, November), 518--521.
• 24: Savoj, H., Brayton, R. K., and Touati, H. 1991. Extracting local don't cares for network optimization. In Proceedings of the International Conference on Computer-Aided Design (Santa Clara, CA, November), 514--517.
• 25: Ellen Sentovich , Kanwar Jit Singh , Cho W. Moon , Hamid Savoj , Robert K. Brayton , Alberto L. Sangiovanni-Vincentelli, Sequential Circuit Design Using Synthesis and Optimization, Proceedings of the 1991 IEEE International Conference on Computer Design on VLSI in Computer & Processors, p.328-333, October 11-14, 1992
• 26: Thomas R. Shiple , Ramin Hojati , Alberto L. Sangiovanni-Vincentelli , Robert K. Brayton, Heuristic minimization of BDDs using don't cares, Proceedings of the 31st annual conference on Design automation, p.225-231, June 06-10, 1994, San Diego, California, United States [doi>10.1145/196244.196360]
• 27: Shiple, T. R., Singhal, V., Brayton, R. K., and Sangiovanni-Vincentelli, A. L. 1996. Analysis of combinational cycles in sequential circuits. In Proceedings of the International Symposium on Circuits and Systems (Atlanta, May).
• 28: João P. Marques Silva , Karem A. Sakallah, GRASP—a new search algorithm for satisfiability, Proceedings of the 1996 IEEE/ACM international conference on Computer-aided design, p.220-227, November 10-14, 1996, San Jose, California, United States
• 29: Vigyan Singhal , Robert K. Brayton, Design replacements for sequential circuits, 1996
• 30: Vigyan Singhal , Carl Pixley, The Verifiacation Problem for Safe Replaceability, Proceedings of the 6th International Conference on Computer Aided Verification, p.311-323, June 21-23, 1994
• 31: Vigyan Singhal , Sharad Malik , Robert K. Brayton, The case for retiming with explicit reset circuitry, Proceedings of the 1996 IEEE/ACM international conference on Computer-aided design, p.618-625, November 10-14, 1996, San Jose, California, United States
• 32: Vigyan Singhal , Carl Pixley , Adnan Aziz , Robert K. Brayton, Exploiting power-up delay for sequential optimization, Proceedings of the conference on European design automation, p.54-59, September 18-22, 1995, Brighton, England
• 33: Singhal, V., Pixley, C., Aziz, A., and Brayton, R. 2001. A theory of safe replacements for sequential circuits. IEEE Trans. Comput. Aided Des. Integ. Circ. Syst. 20, 2 (Feb.).
• 34: Touati, H., Savoj, H., Lin, B., Brayton, R. K., and Sangiovanni-Vincentelli, A. L. 1990. Implicit state enumeration of finite state machines using BDD's. In Proceedings of the International Conference on Computer-Aided Design (Santa Clara, CA, November), 130--133.
• 35: Villa, T. University of California, Berkeley. Personal communication.

INDEX TERMS

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

General Terms:
Algorithms, Design

Keywords:
Sequential logic synthesis, no-reset latches, safe replaceability