Article

Free access

Representation and symbolic manipulation of linearly inductive Boolean functions

Authors:

Aarti Gupta,

Allan L. FisherAuthors Info & Claims

ICCAD '93: Proceedings of the 1993 IEEE/ACM international conference on Computer-aided design

Pages 192 - 199

Published: 07 November 1993 Publication History

PDF eReader

References

[1]

C.L. Berman. Ordered Binary Decision Diagrams and circuit structure. In Proc. IEEE Int. Conf. on Comp. Design, pages 392-395. IEEE Comp. Soc. Press, 1989.

Crossref

Google Scholar

[2]

S. Bose and A. L. Fisher. Automatic verification of synchronous circuits using symbolic simulation and temporal logic, in L. M. J. Claesen, editor, Proc. IFIP Int. Workshop on Applied Formal Methods for Correct VLSI Design, volume II, pages 151-158. North-Holland, 1990.

Google Scholar

[3]

K. S. Brace, R. L. Rudell, and R. E. Bryant. Efficient implementation of a BDD package, in Proc. 27th ACM/IEEE Design Automation Conf., pages 40-45. IEEE Comp. Soc. Press, June 1990.

Digital Library

Google Scholar

[4]

R. E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Trans. on Comp., C-35(8):677-691, August 1986.

Digital Library

Google Scholar

[5]

R. E. Bryant. Symbolic Boolean manipulation with Ordered Binary Decision Diagrams. Technical Report CMU-CS-92- 160, School of Comp. Sci., Carnegie Mellon Univ., July 1992. Also to be published in ACM Computing Surveys.

Digital Library

Google Scholar

[6]

J. Burch, E. M. Clarke, K. McMillan, and D. L. Dill. Se- ~ential circuit verification using symbolic model checking. Proc. 27th ACM/IEEE Design Automation Conf., pages 46-51. IEEE Comp. Soc. Press, June 1990.

Digital Library

Google Scholar

[7]

A. J. Camilleri, M. J. C. Gordon, and T. F. Melham. Hardware verification using higher-order logic. In D. Borrione, editor, From HDL Descriptions to Guaranteed Correct Circuit Designs, pages 43-67. North-Holland, 1987.

Google Scholar

[8]

O. Coudert, C. Berthet, and J. C. Madre. Verification of synchronous sequential machines using symbolic execution. In Proc. Int. Workshop on Automatic Ve-r(lication Methods for Finite State Systems, volume 407 of LNCS, pages 365-373. Springer-Verlag, 1990.

Digital Library

Google Scholar

[9]

A. J. de Geus. High level design: A design vision for the 90's. In Proc. IEEE Int. Conf. on Comp. Design, page 8. IEEE Comp. Soc. Press, 1992.

Digital Library

Google Scholar

[10]

A. Gupta and A. L. Fisher. Representation and manipulation of inductive Boolean functions. Technical Report CMU-CS- 92-129, School of Comp. Sci., Carnegie Mellon Univ., April 1992.

Crossref

Google Scholar

[11]

A. Gupta and A. L. Fisher. Parametric circuit representation using inductive Boolean functions. In Proceedings of the Conference on Computer-Aided Verification, June 1993.

Digital Library

Google Scholar

[12]

W. A. Hunt, Jr. The mechanical verification of a microprocessor design. In D. Borrione, editor, From HDL Descriptions to Guaranteed Correct Circuit Designs, pages 89-129. North-Holland, 1987.

Google Scholar

[13]

R. P. Kurshan and K. L. McMillan. A structural induction theorem for processes. In Proc. 8th Ann. ACM Syrup. on Principles of Dist. Computing, pages 239-247. ACM Press, 1989.

Digital Library

Google Scholar

[14]

R. Lisanke, editor. FSM Benchmark Suite. Microelectronics Center of North Carolina, Research Triangle Park, North Carolina, 1987.

Google Scholar

[15]

K.L. McMillan. Symbolic Model Checking, An approach to the state explosion problem. PhD thesis, SchooIof Comp. Sci., Carnegie Mellon Univ., May 1992.

Digital Library

Google Scholar

[16]

J.-K. Rho and E Somenzi. Inductive verification of iterative systems. In Proc. 29th ACM/IEEE Design Automation Conf., pages 628-633. IEEE Comp. Soc. Press, June 1992.

Digital Library

Google Scholar

[17]

D. Verkest, P. Johannes, L. Claesen, and H. De Man. Correctness proofs of parameterized hardware modules in the Cathedral-II synthesis environment, in Proc. European Design Automation Conf. IEEE Comp. Soc. Press, 1990.

Digital Library

Google Scholar

[18]

P. Wolper and V. Lovinfosse. Verifying properties of large sets of processes with network invariants. In Proc. Int. Workshop on Automatic Verification Methods for Finite State Systems. volume 407 of LNCS. pages 68-80. Springer-Verlag. 1990.

Digital Library

Google Scholar

Cited By

View all

Boichut YCouvreur JNguyen D(2011)Functional term rewriting systems towards symbolic model-checkingInternational Journal of Critical Computer-Based Systems10.1504/IJCCBS.2011.0423342:3/4(378-408)Online publication date: 1-Sep-2011
https://dl.acm.org/doi/10.1504/IJCCBS.2011.042334
Couvreur JThierry-Mieg Y(2005)Hierarchical decision diagrams to exploit model structureProceedings of the 25th IFIP WG 6.1 international conference on Formal Techniques for Networked and Distributed Systems10.1007/11562436_32(443-457)Online publication date: 2-Oct-2005
https://dl.acm.org/doi/10.1007/11562436_32

Recommendations

On the Symmetric Negabent Boolean Functions
INDOCRYPT '09: Proceedings of the 10th International Conference on Cryptology in India: Progress in Cryptology

We study the negabent Boolean functions which are symmetric. The Boolean function which has equal absolute spectral values under the nega-Hadamard transform is called a negabent function. For a bent function, the absolute spectral values are the same ...
Boolean functions with two distinct Walsh coefficients

Are there other Boolean functions having two distinct Walsh coefficients except affine Boolean functions and maximal nonlinear (i.e. bent) Boolean functions__ __ This paper proves that all Boolean functions with exactly two distinct Walsh coefficients ...
Characterizing negabent boolean functions over finite fields
SETA'12: Proceedings of the 7th international conference on Sequences and Their Applications

We consider negabent Boolean functions that have Trace representation. To the best of our knowledge, this is the first ever work on negabent functions with such representation. We completely characterize negabent quadratic monomial functions. We also ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

ICCAD '93: Proceedings of the 1993 IEEE/ACM international conference on Computer-aided design

November 1993

781 pages

ISBN:0818644907

Chairmen:
Michael Lightner
Univ. of Colorado, Boulder
,
Jochen A. G. Jess
Eindhoven Univ. of Tech., Eindhoven, The Netherlands

Publisher

IEEE Computer Society Press

Washington, DC, United States

Publication History

Published: 07 November 1993

Check for updates

Qualifiers

Article

Conference

ICCAD '93

Sponsor:

SIGDA
IEEE-CS

ICCAD '93: International Conference on Computer Aided Design

November 7 - 11, 1993

California, Santa Clara, USA

Acceptance Rates

Overall Acceptance Rate 457 of 1,762 submissions, 26%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
205
Total Downloads

Downloads (Last 12 months)62
Downloads (Last 6 weeks)5

Reflects downloads up to 19 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Boichut YCouvreur JNguyen D(2011)Functional term rewriting systems towards symbolic model-checkingInternational Journal of Critical Computer-Based Systems10.1504/IJCCBS.2011.0423342:3/4(378-408)Online publication date: 1-Sep-2011
https://dl.acm.org/doi/10.1504/IJCCBS.2011.042334
Couvreur JThierry-Mieg Y(2005)Hierarchical decision diagrams to exploit model structureProceedings of the 25th IFIP WG 6.1 international conference on Formal Techniques for Networked and Distributed Systems10.1007/11562436_32(443-457)Online publication date: 2-Oct-2005
https://dl.acm.org/doi/10.1007/11562436_32

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Cited By

Recommendations

On the Symmetric Negabent Boolean Functions

Boolean functions with two distinct Walsh coefficients

Characterizing negabent boolean functions over finite fields