Abstract
Transforming Boolean relations and functions is an important horizontal technique that finds several applications in logic synthesis and formal verification. This paper develops a framework for analyzing input/output transformations of Boolean relations and functions. It also contributes efficient composition techniques based on partitioning the transformation. Experimental results on equivalence-preserving FSM state-space re-encoding demonstrate the feasibility of the approach.
Chapter PDF
References
K.S. Brace, R.L. Rudell, R. Bryant: Efficient Implementation of a BDD Package. Proc. IEEE/ACM DAC'90, June 1990, pp. 40–45
R.E. Bryant: Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, Vol. C-35, No. 8, August 1986, pp. 667–691
G. Cabodi, P. Camurati, S. Quer: Symbolic Exploration of Large Circuits with Enhanced Forward/Backward Traversals. Proc. IEEE EURO-DAC'94, Grenoble (France), September 1994, pp. 22–27 best paper award
G. Cabodi, P. Camurati, S. Quer: Computing subsets of equivalence classes for large FSMs. Proc. IEEE EURO-DAC'95, September 1995
O. Coudert, J.C. Madre, C. Berthet: Verifying temporal properties of sequential machines without building their state diagrams. AMS/DIMACS Series in Discrete Mathematics and Theoretical Computer Science, Vol. 3, 1991, pp. 75–84
G. De Micheli: Synthesis and optimization of digital circuits. McGraw-Hill, 1994
G.D. Hachtel, M. Hermida, A. Pardo, M. Poncino, F. Somenzi: Re-Encoding Sequential Circuits to Reduce Power Dissipation. Proc. IEEE ICCAD'94, November 1994, pp. 70–73
B. Lin, H.J. Touati, A. Richard Newton: Don't Care Minimization of Multi-Level Sequential Logic Networks. Proc. IEEE ICCAD'90, November 1990, pp. 414–417
C. Pixley: A computational theory and implementation of sequential hardware equivalence. AMS/DIMACS Series in Discrete Mathematics and Theoretical Computer Science, Vol. 3, 1991, pp. 293–320
S. Quer, G. Cabodi, P. Camurati, L. Lavagno, E.M. Sentovich, R.K. Brayton: Incremental FSM Re-encoding for Simplifying Verification by Symbolic Traversal. IEEE International Workshop on Logic Synthesis, May 1995
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cabodi, G., Quer, S., Camurati, P. (1995). Transforming Boolean relations by symbolic encoding. In: Camurati, P.E., Eveking, H. (eds) Correct Hardware Design and Verification Methods. CHARME 1995. Lecture Notes in Computer Science, vol 987. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60385-9_10
Download citation
DOI: https://doi.org/10.1007/3-540-60385-9_10
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60385-6
Online ISBN: 978-3-540-45516-5
eBook Packages: Springer Book Archive