Abstract
We describe a new method to simplify combinational circuits while preserving the set of all possible values (that is, the range) on the outputs. This method is performed iteratively and on the fly while building BDDs of the circuits. The method is composed of three steps; 1) identifying a cut in the circuit, 2) identifying a group of nets within the cut, 3) replacing the logic driving the group of nets in such a way that the range of values for the entire cut is unchanged and, hence, the range of values on circuit outputs is unchanged. Hence, we parameterize the circuit in such a way that the range is preserved and the representation is much more efficient than the original circuit. Actually, these replacements are not done in terms of logic gates but in terms of BDDs directly. This is allowed by a new generalized parametric representation algorithm to deal with both input and output variables at the same time. We applied this method to combinational equivalence checking and the experimental results show that this technique outperforms an existing related method which replaces one logic net at a time. We also proved that the previous method is a special case of ours. This technique can be applied to various other problem domains such as symbolic simulation and image computation in model checking.
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
M. Aagaard, R. B. Jones, and C.-J. H. Seger. Formal verification using parametric representations of boolean constraints. In Proceedings of the Design Automation Conference, pages 402–407, June 1999.
C. L. Berman and L. H. Trevillyan. Functional comparison of logic designs for VLSI circuits. In Proceedings of the International Conference on Computer-Aided Design, pages 456–459, Santa Clara, CA, November 1989.
D. Brand. Verification of large synthesized designs. In Proceedings of the International Conference on Computer-Aided Design, pages 534–537, Santa Clara, CA, November 1993.
R. E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, C-35(8):677–691, August 1986.
E. Cerny and M. A. Marin. A computer algorithm for the synthesis of memoryless logic circuits. IEEE Transactions on Computers, C-23(5):455–465, May 1974.
E. Cerny and C. Mauras. Tautology checking using cross-controllability and cross-observability relations. In Proceedings of the International Conference on Computer-Aided Design, pages 34–37, Santa Clara, CA, November 1990.
O. Coudert, C. Berthet, and J. C. Madre. Verification of sequential machines using Boolean functional vectors. In L. Claesen, editor, Proceedings IFIP International Workshop on Applied Formal Methods for Correct VLSI Design, pages 111–128, Leuven, Belgium, November1989.
O. Coudert and J. C. Madre. A unified framework for the formal verification of sequential circuits. In Proceedings of the International Conference on Computer-Aided Design, pages 126–129, November 1990.
P. Jain and G. Gopalakrishnan. Efficient symbolic simulation-based verifiaction using the parametric form of boolean expressions. IEEE Transactions on CAD, 13(8): 1005–1015, August 1994.
A. Kuehlmann and F. Krohm. Equivalence checking using cuts and heaps. In Proceedings of the Design Automation Conference, pages 263–268, Anaheim, CA, June 1997.
J. H. Kukula and T. R. Shiple. Building circuits from relations. In E. A. Emerson and A. P. Sistla, editors, 12th Conference on Computer Aided Verification (CAV’00), pages 131–143. Springer-Verlag, Chicago, July 2000. LNCS 1855.
H. H. Kwak, I.-H. Moon, J. Kukula, and T. Shiple. Combinational equivalence checking through function transformation. In Proceedings of the International Conference on Computer-Aided Design (To appear), San Jose, CA, November 2002.
J. P. Marques-Silva and K. A. Sakallah. GRASP: A search algorithm for propositional satisfiability. IEEE Transactions on CAD, 48(5):506–521, May 1999.
Y. Matsunaga. An efficient equivalence checker for combinational circuits. In Proceedings of the Design Automation Conference, pages 629–634, June 1996.
K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, Boston, MA, 1994.
I.-H. Moon, G. D. Hachtel, and F. Somenzi. Border-block triangular form and conjunction schedule in image computation. InW. A. Hunt, Jr. and S. D. Johnson, editors, Formal Methods in Computer Aided Design, pages 73–90. Springer-Verlag, November 2000. LNCS 1954.
I.-H. Moon, J. H. Kukula, K. Ravi, and F. Somenzi. To split or to conjoin: The question in image computation. In Proceedings of the Design Automation Conference, pages 23–28, Los Angeles, CA, June 2000.
J. Moondanos, C.-J. H. Seger, Z. Hanna, and D. Kaiss. Clever: Divide and conquer combinational logic equivalence verification with false negative elimination. In B. Berry, H. Comon, and A. Finkel, editors, 13th Conference on Computer Aided Verification (CAV’01), pages 131–143. Springer-Verlag, Paris, July 2001. LNCS 2101.
M. W. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang, and S. Malik. Chaff: Engineering an efficient SAT solver. In Proceedings of the Design Automation Conference, pages 530–535, June 2001.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Moon, IH., Kwak, H.H., Kukula, J., Shiple, T., Pixley, C. (2002). Simplifying Circuits for Formal Verification Using Parametric Representation. In: Aagaard, M.D., O’Leary, J.W. (eds) Formal Methods in Computer-Aided Design. FMCAD 2002. Lecture Notes in Computer Science, vol 2517. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36126-X_4
Download citation
DOI: https://doi.org/10.1007/3-540-36126-X_4
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00116-4
Online ISBN: 978-3-540-36126-8
eBook Packages: Springer Book Archive