Abstract
This paper describes novel contributions to the problem of sequential equivalence checking. We address industrial setups, where the design of VLSI chips typically requires checking the equivalence of an RTL model (the specification) and a gate level optimized circuit (the implementation). Due to the size of the overall problem, compositionality is required. The circuit must be resetable, but the reset state is not yet known when equivalence checking is performed. In this paper we discuss the conditions under which decomposed proofs of equivalence are able to infer the equivalence of the full design. Our main contributions with respect to the state of the art in this field are: (1) discussing compositionality given a 3-valued initialization scheme, (2) accepting decompositions with overlapping partitions.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Grumberg, O., Clarke, E., Peled, D. (eds.): Model Checking. MIT Press, Redmond, Washington (2000)
Pixley, C.: A Theory and Implementation of Sequential Hardware Equivalence. IEEE Trans. on Computer-Aided Design 11(12), 1469–1478 (1992)
Huang, S.Y., Cheng, K.T., Chen, K.C., Brewer, F., Huang, C.Y.: AQUILA: An equivalence checking system for large sequential designs. IEEE Trans. on Computers (2000)
Huang, S.Y., Cheng, K.T., Chen, K.C.: Verifying sequential equivalence using ATPG techniques. ACM Transactions on Design Automation of Electronic Systems (2001)
Khasidashvili, Z., Hanna, Z.: SAT-based methods for sequential hardware equivalence verification without synchronization. In: Electronic Notes in Theoretical Computer Science, Elsevier, North-Holland, Amsterdam (2003)
Khasidashvili, Z., Skaba, M., Kaiss, D., Hanna, Z.: Theoretical framework for compositional sequential hardware equivalence verification in presence of design constraints. In: Proc. Int’l Conf. on Computer-Aided Design, San Jose, California, pp. 58–65 (November 2004)
Moon, I., Bjesse, P., Pixley, C.: A Compositional Approach to the Combination of Combinational and Sequential Equivalence Checking of Circuits without Known Reset States. In: Proc. Design Automation & Test in Europe Conf., Nice, France (April 2007)
Pixley, C.: A Computational Theory and Implementation of Sequential Hardware Equivalence. AMS/DIMACS Series in Discrete Mathematics and Theoretical Computer science 3, 293–320 (1991)
Mony, H., Baumbartnet, J., Paruthi, V., Kanzelman, R.: Exploiting suspected redundancy without proving it. In: Proc. IEEE DAC 2005, San Diego, CA, pp. 463–466 (June 2005)
Stoffel, D., Wedler, M., Warkentin, P., Kunz, W.: Structural FSM traversal. IEEE Transactions on Computer-Aided Design (May 2004)
Bischoff, G.P., Brace, K.S., Jain, S., Razdan, R.: Formal Implementation Verification of the Bus Interface Unit for the Alpha 21264 Microprocessor. In: Proc. Int’l Conf. on Computer Design, Austin, Texas (October 1997)
Coudert, O., Berthet, C., Madre, J.C.: Verification of Sequential Machines Based on Symbolic Execution. In: Sifakis, J. (ed.) Automatic Verification Methods for Finite State Systems. LNCS, vol. 407, pp. 365–373. Springer, Heidelberg (1990)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bischoff, G.P., Brace, K.S., Cabodi, G. (2007). A Compositional Approach for Equivalence Checking of Sequential Circuits with Unknown Reset State and Overlapping Partitions. In: Moreno Díaz, R., Pichler, F., Quesada Arencibia, A. (eds) Computer Aided Systems Theory – EUROCAST 2007. EUROCAST 2007. Lecture Notes in Computer Science, vol 4739. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-75867-9_64
Download citation
DOI: https://doi.org/10.1007/978-3-540-75867-9_64
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-75866-2
Online ISBN: 978-3-540-75867-9
eBook Packages: Computer ScienceComputer Science (R0)