Abstract
We consider the problem of equivalence checking of circuits N 1,N 2 with a common specification (CS). We show that circuits N 1 and N 2 have a CS iff they can be partitioned into toggle equivalent subcircuits that are connected “in the same way”. Based on this result, we formulate a procedure for checking equivalence of circuits N 1 and N 2 with specifications S 1 and S 2. This procedure not only checks equivalence of N 1 and N 2 but also verifies that S 1 and S 2 are identical. The complexity of this procedure is linear in specification size and exponential in the value of a specification parameter. Previously we considered specifications parameterized by the size of the largest subcircuit (specification granularity). In this paper we give a more general parameterization based on specification “width”.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Alekhnovich, A., Razborov, A.: Satisfiability, Branch-width and Tseitin Tautologies. In: FOCS 2002, pp. 593–603 (2002)
Berman, C.L.: Circuit width, Register Allocation and Ordered Binary Decision Diagrams. IEEE Trans. CAD 10(8), 1059–1066 (1991)
Broering, E.A., Lokam, S.V.: Width-Based Algorithms for Satisfiability. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 162–171. Springer, Heidelberg (2004)
Downey, R.G., Fellows, M.R.: Parameterized complexity. Springer, Heidelberg (1999)
Goldberg, E., Novikov, Y.: How good can a resolution based SAT-solver be? In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 37–52. Springer, Heidelberg (2004)
Goldberg, E.: On equivalence checking and logic synthesis of circuits with a common specification. Cadence Berkeley Labs, Technical report, CDNL-TR-2004-1220 (August 2004), http://eigold.tripod.com/papers/tr-2004-1220.pdf
Prasad, M.R., Chong, P., Keutzer, K.: Why is Combinatorial ATPG Efficiently Solvable for Practical VLSI Circuits? Journal of Electronic Testing: Theory and Applications 17, 509–527 (2001)
Szeider, S.: On Fixed-parameter Tractable Parameterizations of SAT. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 188–202. Springer, Heidelberg (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Goldberg, E. (2005). Equivalence Checking of Circuits with Parameterized Specifications. In: Bacchus, F., Walsh, T. (eds) Theory and Applications of Satisfiability Testing. SAT 2005. Lecture Notes in Computer Science, vol 3569. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11499107_8
Download citation
DOI: https://doi.org/10.1007/11499107_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-26276-3
Online ISBN: 978-3-540-31679-4
eBook Packages: Computer ScienceComputer Science (R0)