This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
AQUILA: An Equivalence Checking System for Large Sequential Designs
May 2000 (vol. 49 no. 5)
pp. 443-464

Abstract—In this paper, we present a practical method for verifying the functional equivalence of two synchronous sequential designs. This tool is based on our earlier framework that uses Automatic Test Pattern Generation (ATPG) techniques for verification. By exploring the structural similarity between the two designs under verification, the complexity can be reduced substantially. We enhance our framework by three innovative features. First, we develop a local BDD-based technique which constructs Binary Decision Diagram (BDD) in terms of some internal signals, for identifying equivalent signal pairs. Second, we incorporate a technique called partial justification to explore not only combinational similarity, but also sequential similarity. This is particularly important when the two designs have a different number of flip-flops. Third, we extend our gate-to-gate equivalence checker for RTL-to-gate verification. Two major issues are considered in this extension: 1) how to model and utilize the external don't care information for verification; and 2) how to extract a subset of unreachable states to speed up the verification process. Compared with existing approaches based on symbolic Finite State Machine (FSM) traversal techniques, our approach is less vulnerable to the memory explosion problem and, therefore, is more suitable for a lot of real-life designs. Experimental results of verifying designs with hundreds of flip-flops will be presented to demonstrate the effectiveness of this approach.

[1] M. Abramovici, M.A. Breuer, and A.D. Friedman, Digital Systems Testing and Testable Design. IEEE Press, 1990.
[2] P. Ashar, A. Gupta, and S. Malik, “Using Complete-1-Distinguishability for FSM Equivalence Checking,” Proc. Int'l Conf. Computer-Aided Design, pp. 346-353, Nov. 1996.
[3] R.A. Bergamaschi, D. Brand, L. Stok, M. Berkelaar, and S. Prakash, “Efficient Use of Large Don't Cares in High-Level and Logic Synthesis,” Proc. Int'l Conf. Computer-Aided Design, pp. 272-278, Nov. 1995.
[4] M.P. Allen and D.J. Tildesley, Computer Simulation of Liquids, Clarendon Press, Oxford, UK, 1990.
[5] D. Brand, "Verification of Large Synthesized Designs," Proc. IEEE Int'l Conf. Computer-Aided Design (ICCAD), IEEE Computer Society Press, Los Alamitos, Calif., 1993, pp. 534-537.
[6] R.E. Bryant, "Graph-Based Algorithms for Boolean Function Manipulation," IEEE Trans. Computers, Vol. C-35, No. 8, Aug. 1986, pp. 667-690.
[7] K.T. Cheng, “Redundancy Removal for Sequential Circuits without Reset State,” IEEE Trans. Computer Aided Design of Integrated Circuits and Systems, vol. 12, no. 1, pp. 13-24, Jan. 1993.
[8] W.-T. Cheng, “The BACK Algorithm for Sequential Test Generation,” Proc. Int’l Conf. Computer Design, IEEE CS Press, 1988, pp. 66-69.
[9] B.G. Silverman,“Survey of expert critiquing systems: practical and theoretical frontiers,” Communications of the ACM, vol. 35, no. 4, pp. 06-127, Apr. 1992.
[10] H. Cho and F. Somenzi, “Sequential Logic Optimization Based on State Space Decomposition,” Proc. European Conf. Design Automation, pp. 200-204, Feb. 1993.
[11] O. Coudert, C. Berthet, and J.C. Madre, “Verification of Sequential Machines Based on Symbolic Execution,” Proc. Workshop Automatic Verification Methods for Finite State Systems, 1989.
[12] C.A. Eijk and J.A. Jess, “Detection of Equivalent State Variables in Finite State Machine Verification,” Notes Int'l Workshop Logic Synthesis, pp. 3.35-3.44, 1995.
[13] A. Ghosh, S. Devadas, and A.R. Newton, "Test Generation and Verification for Highly Sequential Circuits," IEEE Trans. Computer-Aided Design, pp. 652-667, May 1991.
[14] J.P. Hayes,Computer Architecture and Organization, Second Edition, McGraw-Hill, 1988.
[15] Y.V. Hoskote, “Formal Techniques for Verification of Synchronous Sequential Circuits,” PhD thesis, Univ. of Texas at Austin, Dec. 1995.
[16] A.Y. Zomaya, F. Ercal, and S. Olariu, Solutions to Parallel and Distributed Computing Problems: Lessons from Biological Sciences. New York: Wiley, 2001.
[17] S.-Y. Huang, K.-T. Cheng, and K.-C. Chen, “On Verifying the Correctness of Retimed Circuits,” Proc. Great-Lake Symp. VLSI, pp. 277-281, Mar. 1996.
[18] S.-Y. Huang, K.-C. Chen, and K.-T. Cheng, “Error Correction Based on Verification Techniques,” Proc. Design Automation Conf., pp. 258-261, June 1996.
[19] S.-Y. Huang, K.-T. Cheng, and K.-C. Chen, "AQUILA: An Equivalence Verifier for Large Sequential Circuits," Proc. Asia-Pacific Design Automation Conf., 1997.
[20] J. Jain, R. Mukherjee, and M. Fujita, “Advanced Verification Techniques Based on Learning,” Proc. Design Automation Conf., pp. 420-426, June 1995.
[21] A. Kuehlmann, A. Srinivasan, and D. P. LaPotin, "Verity—A Formal Verification Program for Custom CMOS Circuits," IBM J. Research and Development, Vol. 39, No. 1/2, Jan.-Mar., 1995, pp. 149-165.
[22] W. Kunz, "Hannibal: An Efficient Tool for Logic Verification Based on Recursive Learning," Proc. ICCAD, IEEE CS Press, 1993, pp. 538-541.
[23] C.E. Leiserson and J.B. Laxe, “Retiming Synchronous Circuitry,” Algorithmica, vol. 6, no. 1, 1991.
[24] R. Marlett, “EBT: A Comprehensive Test Generation Technique for Highly Sequential Circuits,” Proc. Design Automation Conf., pp. 332-339, June 1978.
[25] J. Jain, R. Mukherjee, and M. Fujita, “Advanced Verification Techniques Based on Learning,” Proc. Design Automation Conf., pp. 420-426, June 1995.
[26] A. Kuehlmann, A. Srinivasan, and D. P. LaPotin, "Verity—A Formal Verification Program for Custom CMOS Circuits," IBM J. Research and Development, Vol. 39, No. 1/2, Jan.-Mar., 1995, pp. 149-165.
[27] W. Kunz, "Hannibal: An Efficient Tool for Logic Verification Based on Recursive Learning," Proc. ICCAD, IEEE CS Press, 1993, pp. 538-541.
[28] C.E. Leiserson and J.B. Laxe, “Retiming Synchronous Circuitry,” Algorithmica, vol. 6, no. 1, 1991.
[29] R. Marlett, “EBT: A Comprehensive Test Generation Technique for Highly Sequential Circuits,” Proc. Design Automation Conf., pp. 332-339, June 1978.
[30] Y. Matsunaga, “An Efficient Equivalence Checker for Combinational Circuits,” Proc. Design Automation Conf., pp. 629-634, June 1996.
[31] C. Pixley, “A Theory and Implementation of Sequential Hardware Equivalence,” IEEE Trans. Computer-Aided Design, pp. 1,469-1,494, Dec. 1992.
[32] C. Pixley, V. Singhal, A. Aziz, and R.K. Brayton, “Multi-Level Synthesis for Safe Replaceability,” Proc. Int'l Conf. Computer-Aided Design, pp. 442-449, Nov. 1994.
[33] D.K. Pradhan, D. Paul, and M. Chatterjee, “VERILAT: Verification Using Logic Augmentation and Transformations,” Proc. Int'l Conf. Computer-Aided Design, pp. 88-95, Nov. 1996.
[34] S.M. Reddy, W. Kunz, and D.K. Pradhan, “Novel Verification Framework Combining Structural and OBDD Methods in a Synthesis Environment,” Proc. Design Automation Conf., pp. 414-419, June 1995.
[35] R. Rudell, "Dynamic Variable Ordering for Ordered Binary Decision Diagrams," Proc. ICCAD-93, pp. 42-47, 1993.
[36] N. Shenoy and R. Rudell, “Efficient Implementation of Retiming,” Proc. Int'l Conf. Computer-Aided Design, pp. 226-233, Nov. 1994.
[37] V. Singhal and C. Pixley, “The Verification Problem for Safe Replaceability,” Proc. Conf. Computer-Aided Verification, pp. 311-323, June 1994.
[38] “SIS: A System for Sequential Circuit Synthesis,” Report M92/41, Univ. of California, Berkeley, May 1992.
[39] H. Touati, H. Savoj, B. Lin, R. Brayton, and A. Sangiovanni-Vincentelli, "Implicit State Enumeration of Finite State Machines Using BDDs," Proc. Int'l Conf. Computer-Aided Design, pp. 130-133, 1990.
[40] R.K. Brayton et al., “VIS: Verification Interacting with Synthesis,” Proc. Conf. Computer-Aided Verification, pp. 408-412, 1996.

Index Terms:
Design verification, formal verification, equivalence checking, state exploration.
Citation:
Shi-Yu Huang, Kwang-Ting Cheng, Kuang-Chien Chen, Chung-Yang Huang, Forrest Brewer, "AQUILA: An Equivalence Checking System for Large Sequential Designs," IEEE Transactions on Computers, vol. 49, no. 5, pp. 443-464, May 2000, doi:10.1109/12.859539
Usage of this product signifies your acceptance of the Terms of Use.