More Web Proxy on the site http://driver.im/

article

Limits of Using Signatures for Permutation Independent Boolean Comparison

Authors:

Sharad MalikAuthors Info & Claims

Formal Methods in System Design, Volume 21, Issue 2

Pages 167 - 191

https://doi.org/10.1023/A:1016091418702

Published: 01 September 2002 Publication History

Abstract

This paper addresses problems that arise while checking the equivalence of two Boolean functions under arbitrary input permutations. The permutation problem has several applications in the synthesis and verification of combinational logic: it arises in the technology mapping stage of logic synthesis and in logic verification. A popular method to solve it is to compute a signature for each variable that helps to establish a correspondence between the variables. Several researchers have suggested a wide range of signatures that have been used for this purpose. However, for each choice of signature, there remain variables that cannot be uniquely identified. Our research has shown that, for a given example, this set of problematic variables tends to be the same–regardless of the choice of signatures. The paper investigates this problem.

References

[1]

1. K.S. Brace, R.L. Rudell, and R.E. Bryant, "Efficient implementation of a BDD package," in Proceedings of the 27th ACM/IEEE Design Automation Conference, June 1990, pp. 40-45.

Digital Library

[2]

2. R.E. Bryant, "Graph-based algorithms for Boolean function manipulation," IEEE Transactions on Computers, Vol. C-35, pp. 677-691, 1986.

Digital Library

[3]

3. J.B. Burch and D.E. Long, "Efficient Boolean function matching," in Proceedings of the Int'l Conference on Computer-Aided Design, November 1992, pp. 408-411.

Digital Library

[4]

4. D.I. Cheng and M. Marek Sadowska, "Verifying equivalence of functions with unknown input correspondence," in Proceedings of EDAC, February 1993, pp. 81-85.

[5]

5. E.M. Clarke, K.L. McMillan, X. Zhao, M. Fujita, and J. Yang, "Spectral transforms for large Boolean functions with applications to technology mapping," in Proceedings of the 30th ACM/IEEE Design Automation Conference, 1993, pp. 54-60.

Digital Library

[6]

6. G. Hotz, Schaltungstheorie, De Gruyter Lehrbuch, Walter De Gruyter, 1974.

[7]

7. Y.-T. Lai, S. Sastry, and M. Pedram, "Boolean matching using binary decision diagrams with applications to logic synthesis and verification," in Proceedings of the ICCD'92, October 1992, pp. 452-458.

Digital Library

[8]

8. J. Mohnke, "A signature-based approach to formal logic verification," Ph.D. thesis, http://sundoc. bibliothek.uni-halle.de/diss-online/99/99H050/, 1999.

[9]

9. J. Mohnke and S. Malik, "Permutation and phase independent Boolean comparison," INTEGRATION--The VLSI Journal, Vol. 16, pp. 109-129, 1993.

Digital Library

[10]

10. D. Möller, J. Mohnke, and M. Weber, "Detection of symmetry of Boolean functions represented by ROBDDs," in Proceedings of ICCAD, November 1993, pp. 680-684.

Digital Library

[11]

11. I. Pomeranz and S.M. Reddy, "On diagnosis and correction of design errors," in Proceedings of ICCAD, November 1993, pp. 500-507.

Digital Library

[12]

12. I. Pomeranz and S.M. Reddy, "On determining symmetries in inputs of logic circuits," IEEE Transactions on CAD of Integrated Circuits and Systems, Vol. 13, No. 11, pp. 1428-1434, 1994.

Digital Library

[13]

13. U. Schlichtmann, F. Brglez, and P. Schneider, "Efficient Boolean matching based on unique variable ordering," in Proceedings of the IWLS, May 1993.

[14]

14. K.H. Wang, T.T. Hwang, and C. Chen, '"Restructering binary decision diagrams based on functional equivalence," in Proceedings of EDAC, February 1993, pp. 261-265.

[15]

15. I. Wegener, The Complexity of Boolean Functions, Wiley-Teubner Series in Computer Science, John Wiley and B.G. Teubner, Stuttgart, 1987.

Digital Library

Cited By

Gascón ASubramanyan PDutertre BTiwari AJovanović DMalik SJobstmann B(2014)Template-based circuit understandingProceedings of the 14th Conference on Formal Methods in Computer-Aided Design10.5555/2682923.2682943(83-90)Online publication date: 21-Oct-2014
https://dl.acm.org/doi/10.5555/2682923.2682943
Maurer PFettweis GNebel W(2014)A universal symmetry detection algorithmProceedings of the conference on Design, Automation & Test in Europe10.5555/2616606.2617039(1-4)Online publication date: 24-Mar-2014
https://dl.acm.org/doi/10.5555/2616606.2617039
Maurer PBrunvard EStevens KCavallaro JZhang T(2012)Extending symmetric variable-pair transitivities using state-space transformationsProceedings of the great lakes symposium on VLSI10.1145/2206781.2206859(315-320)Online publication date: 3-May-2012
https://dl.acm.org/doi/10.1145/2206781.2206859
Show More Cited By

Index Terms

Limits of Using Signatures for Permutation Independent Boolean Comparison
1. General and reference
  1. Cross-computing tools and techniques
    1. Design
2. Mathematics of computing
  1. Discrete mathematics
    1. Combinatorics
      1. Generating functions

Recommendations

Permutation and phase independent Boolean comparison
Sequential Aggregate Signatures Working over Independent Homomorphic Trapdoor One-Way Permutation Domains
Information and Communications Security
Abstract
The contribution of this paper has two folds. In the first fold, we propose a generic construction of sequential aggregate signatures from families of certificated trapdoor one-way permutations. We show that our construction is provably secure in ...
Proxy Confirmation Signatures

The undeniable signature, introduced by Chaum et al. in 1989, provides a nice property that the signer has an additional control over who will benefit from being convinced by the signature. However, a conspicuous drawback of undeniable signature is that ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Formal Methods in System Design

Formal Methods in System Design Volume 21, Issue 2

September 2002

133 pages

ISSN:0925-9856

Issue’s Table of Contents

Copyright © Copyright © 2002 Kluwer Academic Publishers.

Publisher

Kluwer Academic Publishers

United States

Publication History

Published: 01 September 2002

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

6
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 19 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Gascón ASubramanyan PDutertre BTiwari AJovanović DMalik SJobstmann B(2014)Template-based circuit understandingProceedings of the 14th Conference on Formal Methods in Computer-Aided Design10.5555/2682923.2682943(83-90)Online publication date: 21-Oct-2014
https://dl.acm.org/doi/10.5555/2682923.2682943
Maurer PFettweis GNebel W(2014)A universal symmetry detection algorithmProceedings of the conference on Design, Automation & Test in Europe10.5555/2616606.2617039(1-4)Online publication date: 24-Mar-2014
https://dl.acm.org/doi/10.5555/2616606.2617039
Maurer PBrunvard EStevens KCavallaro JZhang T(2012)Extending symmetric variable-pair transitivities using state-space transformationsProceedings of the great lakes symposium on VLSI10.1145/2206781.2206859(315-320)Online publication date: 3-May-2012
https://dl.acm.org/doi/10.1145/2206781.2206859
Maurer P(2011)Conjugate symmetryFormal Methods in System Design10.1007/s10703-011-0116-238:3(263-288)Online publication date: 1-Jun-2011
https://dl.acm.org/doi/10.1007/s10703-011-0116-2
Zhang JMishchenko ABrayton RChrzanowska-Jeske MSentovich E(2006)Symmetry detection for large Boolean functions using circuit representation, simulation, and satisfiabilityProceedings of the 43rd annual Design Automation Conference10.1145/1146909.1147044(510-515)Online publication date: 24-Jul-2006
https://dl.acm.org/doi/10.1145/1146909.1147044
Wei ZChai DNewton AKuehlmann A(2006)Fast Boolean Matching with Don't CaresProceedings of the 7th International Symposium on Quality Electronic Design10.1109/ISQED.2006.65(346-351)Online publication date: 27-Mar-2006
https://dl.acm.org/doi/10.1109/ISQED.2006.65

View Options

View options

Media

Figures

Other

Tables

View Issue’s Table of Contents