Article

Free access

Formal verification of word-level specifications

Authors:

Stefan Höreth,

Rolf DrechslerAuthors Info & Claims

DATE '99: Proceedings of the conference on Design, automation and test in Europe

Pages 11 - es

https://doi.org/10.1145/307418.307447

Published: 01 January 1999 Publication History

PDF eReader

References

[1]

{1} L. Arditi. ^*BMDs can delay the use of theorem proving for verifying arithmetic assembly instructions. In FMCAD, pages 34-48, 1996.

Digital Library

Google Scholar

[2]

{2} R.I. Bahar, E.A. Frohm, C.M. Gaona, G.D. Hachtel, E. Macii, A. Pardo, and F. Somenzi. Algebraic decision diagrams and their application. In Int'l Conf. on CAD, pages 188-191, 1993.

Digital Library

Google Scholar

[3]

{3} C.W. Barrett, D.L. Dill, and J.R. Levitt. A decision procedure for bit-vector arithmetic. In Design Automation Conf., June 1998.

Digital Library

Google Scholar

[4]

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

Digital Library

Google Scholar

[5]

{5} R.E. Bryant and Y.-A. Chen. Verification of arithmetic functions with binary moment diagrams. Technical report, CMU-CS-94-160, 1994.

Digital Library

Google Scholar

[6]

{6} R.E. Bryant and Y.-A. Chen. Verification of arithmetic functions with binary moment diagrams. In Design Automation Conf., pages 535-541, 1995.

Digital Library

Google Scholar

[7]

{7} Y. Chen, E. Clarke, P. Ho, Y. Hoskote, T. Kam, M. Khaira, J. O' Leary, and X. Zhao. Verification of all circuits in a floating-point unit using word-level model checking. In FMCAD, pages 389-403, 1996.

Digital Library

Google Scholar

[8]

{8} Y.-A. Chen and R.E. Bryant. ACV: an arithmetic circuit verifier. In Int'l Conf. on CAD, pages 361-365, 1996.

Digital Library

Google Scholar

[9]

{9} E. Clarke, M. Fujita, P. McGeer, K.L. McMillan, J. Yang, and X. Zhao. Multi terminal binary decision diagrams: An efficient data structure for matrix representation. In Int'l Workshop on Logic Synth., pages P6a:1-15, 1993.

Google Scholar

[10]

{10} E.M. Clarke, M. Fujita, and X. Zhao. Hybrid decision diagrams - overcoming the limitations of MTBDDs and BMDs. In Int' l Conf. on CAD, pages 159-163, 1995.

Crossref

Google Scholar

[11]

{11} E.M. Clarke and X. Zhao. Word level symbolic model checking - a new approach for verifying arithmetic circuits. Technical Report CMU-CS-95-161, 1995.

Digital Library

Google Scholar

[12]

{12} D. Cyrluk, O. Möller, and H. Rueß. An Efficient Decision Procedure for the Theory of Fixed-Sized Bitvectors , volume 1254 of LNCS. Computer Aided Verification, 1997.

Digital Library

Google Scholar

[13]

{13} R. Drechsler and B. Becker. Binary Decision Diagrams - Theory and Implementation. Kluwer Academic Publishers, 1998.

Google Scholar

[14]

{14} R. Drechsler, B. Becker, and S. Ruppertz. The K^*BMD: A verification data structure. IEEE Design & Test of Comp., pages 51-59, 1997.

Digital Library

Google Scholar

[15]

{15} R. Drechsler, A. Sarabi, M. Theobald, B. Becker, and M.A. Perkowski. Efficient representation and manipulation of switching functions based on ordered Kronecker functional decision diagrams. In Design Automation Conf., pages 415-419, 1994.

Digital Library

Google Scholar

[16]

{16} S. Höreth. Implementation of a multiple-domain decision diagram package. In CHARME, Chapman & Hall, pages 185-202, 1997.

Digital Library

Google Scholar

[17]

{17} S. Höreth. Effiziente Konstruktion und Manipulation von binären Entscheidungsgraphen. Ph.D. thesis at Technische Universität, Darmstadt, 1998.

Google Scholar

[18]

{18} S. Höreth and R. Drechsler. Dynamic minimization of word-level decision diagrams. In Design, Automation and Test Europe, pages 612-617, 1998.

Digital Library

Google Scholar

[19]

{19} G. Kamhi, O. Weissberg, and L. Fix. Automatic Datapath Extraction for Efficient Usage of HDD, volume 1254 of LNCS. Computer Aided Verification, 1997.

Digital Library

Google Scholar

[20]

{20} Y.-T. Lai and S. Sastry. Edge-valued binary decision diagrams for multi-level hierarchical verification. In Design Automation Conf., pages 608-613, 1992.

Digital Library

Google Scholar

[21]

{21} C. Scholl, B. Becker, and T.M. Weis. Word-level decision diagrams, WLCDs and division. In Int'l Conf. on CAD, 1998.

Digital Library

Google Scholar

Cited By

View all

Drechsler RMahzoon AWeingarten L(2022)Polynomial Formal Verification of Arithmetic CircuitsProceedings of International Conference on Computational Intelligence and Data Engineering10.1007/978-981-16-7182-1_36(457-470)Online publication date: 28-Feb-2022
https://doi.org/10.1007/978-981-16-7182-1_36
Mahzoon AGroße DDrechsler RMahzoon AGroße DDrechsler R(2022)IntroductionFormal Verification of Structurally Complex Multipliers10.1007/978-3-031-24571-8_1(1-8)Online publication date: 20-Dec-2022
https://doi.org/10.1007/978-3-031-24571-8_1
Ciesielski MKalla PAskar S(2019)Taylor Expansion DiagramsIEEE Transactions on Computers10.1109/TC.2006.15355:9(1188-1201)Online publication date: 13-Nov-2019
https://dl.acm.org/doi/10.1109/TC.2006.153
Show More Cited By

Index Terms

Formal verification of word-level specifications

Recommendations

On the execution of high level formal specifications
Formal verification of SystemC^FLspecifications using SPIN
MINO'06: Proceedings of the 5th WSEAS international conference on Microelectronics, nanoelectronics, optoelectronics

The formal language SystemC^FL is the formalization of SystemC. The language semantics of SystemC^FL was formally defined in a standard structured operational semantics (SOS) style. For verification purposes, in this paper, we present an approach to use ...
Formal verification of ASMs using MDGs

We present a framework for the formal verification of abstract state machine (ASM) designs using the multiway decision graphs (MDG) tool. ASM is a state based language for describing transition systems. MDG provides symbolic representation of transition ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

DATE '99: Proceedings of the conference on Design, automation and test in Europe

January 1999

730 pages

ISBN:1581131216

DOI:10.1145/307418

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 January 1999

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Conference

DATE99

Sponsor:

SIGDA

DATE99: Design Automation and Test in Europe Conference and Exhibition 1999

Munich, Germany

Acceptance Rates

Overall Acceptance Rate 518 of 1,794 submissions, 29%

Upcoming Conference

DATE '25

Sponsor:
sigda

Design, Automation and Test in Europe

March 31 - April 2, 2025

Lyon , France

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

11
Total Citations
View Citations
247
Total Downloads

Downloads (Last 12 months)69
Downloads (Last 6 weeks)8

Reflects downloads up to 19 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Drechsler RMahzoon AWeingarten L(2022)Polynomial Formal Verification of Arithmetic CircuitsProceedings of International Conference on Computational Intelligence and Data Engineering10.1007/978-981-16-7182-1_36(457-470)Online publication date: 28-Feb-2022
https://doi.org/10.1007/978-981-16-7182-1_36
Mahzoon AGroße DDrechsler RMahzoon AGroße DDrechsler R(2022)IntroductionFormal Verification of Structurally Complex Multipliers10.1007/978-3-031-24571-8_1(1-8)Online publication date: 20-Dec-2022
https://doi.org/10.1007/978-3-031-24571-8_1
Ciesielski MKalla PAskar S(2019)Taylor Expansion DiagramsIEEE Transactions on Computers10.1109/TC.2006.15355:9(1188-1201)Online publication date: 13-Nov-2019
https://dl.acm.org/doi/10.1109/TC.2006.153
Alizadeh BFujita M(2010)Modular datapath optimization and verification based on modular-HEDIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2010.205927129:9(1422-1435)Online publication date: 1-Sep-2010
https://dl.acm.org/doi/10.1109/TCAD.2010.2059271
Haubelt CTeich JHaubelt CTeich J(2010)Hardware-VerifikationDigitale Hardware/Software-Systeme10.1007/978-3-642-05356-6_6(235-359)Online publication date: 20-May-2010
https://doi.org/10.1007/978-3-642-05356-6_6
ALIZADEH BFUJITA M(2009)A Unified Framework for Equivalence Verification of Datapath Oriented ApplicationsIEICE Transactions on Information and Systems10.1587/transinf.E92.D.985E92-D:5(985-994)Online publication date: 2009
https://doi.org/10.1587/transinf.E92.D.985
Alizadeh BFujita M(2007)Automatic merge-point detection for sequential equivalence checking of system-level and RTL descriptionsProceedings of the 5th international conference on Automated technology for verification and analysis10.5555/1779046.1779059(129-144)Online publication date: 22-Oct-2007
https://dl.acm.org/doi/10.5555/1779046.1779059
Alizadeh BFujita M(2007)Automatic Merge-Point Detection for Sequential Equivalence Checking of System-Level and RTL DescriptionsAutomated Technology for Verification and Analysis10.1007/978-3-540-75596-8_11(129-144)Online publication date: 2007
https://doi.org/10.1007/978-3-540-75596-8_11
Ghodrat MGivargis TNicolau AConte TFaraboschi PMangione-Smith BNajjar W(2005)Equivalence checking of arithmetic expressions using fast evaluationProceedings of the 2005 international conference on Compilers, architectures and synthesis for embedded systems10.1145/1086297.1086317(147-156)Online publication date: 24-Sep-2005
https://dl.acm.org/doi/10.1145/1086297.1086317
Johannsen PDrechsler R(2002)Utilizing High-Level Information for Formal Hardware VerificationAdvanced Computer Systems10.1007/978-1-4419-8530-9_34(419-431)Online publication date: 2002
https://doi.org/10.1007/978-1-4419-8530-9_34
Show More Cited By

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

Index Terms

Recommendations

On the execution of high level formal specifications

Formal verification of SystemC^FLspecifications using SPIN

Formal verification of ASMs using MDGs