Article

Free access

HSIS: a BDD-based environment for formal verification

Authors:

A. Aziz,

T. Kam,

A. L. Sangiovanni-VincentelliAuthors Info & Claims

DAC '94: Proceedings of the 31st annual Design Automation Conference

Pages 454 - 459

https://doi.org/10.1145/196244.196467

Published: 06 June 1994 Publication History

PDF eReader

References

[1]

A. Aziz, S. Tasiran, and R. K. Brayton. BDD Variable Ordering for Interacting Finite State Machines. In Design Automation Conference, 1994.

Digital Library

Google Scholar

[2]

F. Balarin and G. York. Verilog HDL Modeling Styles for Formal Verification. In IFIP Conference on Hardware Description Languages and their Applications, pages 439-452. OCRI Publications, April 1993.

Digital Library

Google Scholar

[3]

R. S. Boyer and J. S. Moore. A ComputationaILogic Handbook. Academic Press, New York, 1988.

Digital Library

Google Scholar

[4]

R. K. Brayton, M. Chiodo, R. Hojati, T. Kam, K. Kodandapani, R. R Kurshan, S. Malik, A. L. Sangiovanni-Vincentelli, E. M. Sentovich, T. Shiple, K. J. Singh, and H.-Y. Wang. BLIF-MV: An Interchange Format for Design Verification and Synthesis. Technical Report UCB/ERL M91/97, Electronics Research Lab, Univ. of California, Berkeley, CA 94720, November 1991.

Google Scholar

[5]

J. R. Burch, E. M. Clarke, K. L. McMillan, and D. L. Dill. Symbolic Model Checking: 1020 States and Beyond. Information and Computation, 98(2): 142-170, 1992.

Digital Library

Google Scholar

[6]

S. T. Cheng. Compiling Verilog into Automata. Technical report, UC Berkeley, 1994.

Google Scholar

[7]

E.M. Clarke, E. A. Emerson, and A. R Sistla. Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications. ACM Transactions on P1vgramming Languages and Systems, 8(2):244-263,1986.

Digital Library

Google Scholar

[8]

O. Coudert and J. C. Madre. A Unified Framework for the Formal Verification of Sequential Circuits. In P~vc. Intl. Conf. on Computer-AidedDesign, pages 126-129, November 1990.

Crossref

Google Scholar

[9]

D. L. Dill, A. J. Drexler, A. J. Hu, and C. H. Yang. Protocol Verification as a Hardware Design Aid. In P~vc. Intl. Conf. on Computer Design, pages 522-525, October 1992.

Digital Library

Google Scholar

[10]

E. A. Emerson and C. L. Lei. Modalities for Model Checking: Branching Time Strikes Back. In P1vc. ACM Symposium on Principles of P1vgramming Languages, pages 84-96,1985.

Digital Library

Google Scholar

[11]

M. Gordon. HOL: A Proof Generating System for Higher-orderLogic. In G. Birwistle and R A. Subrahmanyam, editors, VLSI Specification, Verification and Synthesis, pages 73-127. Academic Press, Boston, 1988.

Crossref

Google Scholar

[12]

Z. Har'E1 and R. R Kurshan. Software for Analytical Development of Communication Protocols. AT& T Technical Journal, pages 45-59, January 1990.

Google Scholar

[13]

R. Hojati, R. K. Brayton, and R. R Kurshan. BDD-Based Debugging of Design Using Language Containment and Fair CTL. In C. Courcoubetis, editor, P~vc. of the Conf. on Computer-Aided Verification, volume 697, pages 41-58. Springer-Verlag, June 1993.

Digital Library

Google Scholar

[14]

R. Hojati, S. Krishnan, and R. K. Brayton. Heuristic Algorithms for Early Quantification and Partial Product Minimization. Technical Report M94/11, UC Berkeley, 1994.

Digital Library

Google Scholar

[15]

R. Hojati, T. R. Shiple, R. K. Brayton, and R. R Kurshan. A Unified Environment for Language Containment and Fair CTL Model Checking. In P~vc. of the Design Automation Conf., pages 475-481, Dallas, Texas, June 1993.

Digital Library

Google Scholar

[16]

R. Hojati, V. Singhal, and R. K. Brayton. Edge-Streett/Edge-Rabin Automata Environment for Formal Verification Using Language Containment. Technical Report M94/12, UC Berkeley, 1994.

Digital Library

Google Scholar

[17]

R. Hojati, H. Touati, R. R Kurshan, and R. K. Brayton. Efficient w-Regular Language Containment. In P1vc. of the Fourth Workshop on Computer-Aided Verification, pages 371-382, Montrdal, Qudbec, Canada, 1992.

Digital Library

Google Scholar

[18]

R. R Kurshan. Reducibility in Analysis of Coordination. In Discrete Event Systems: Models and Applications, volume 103 of LNCIS, pages 19-39. Springer-Verlag, 1987.

Google Scholar

[19]

R. R Kurshan. Automata-Theoretic Verification of Coordinating P1vcesses. Princeton University Press, 1993. To appear.

Google Scholar

[20]

K. L. McMillan and J. Schwalbe. Formal Verification of the Encore Gigamax Cache Consistency Protocols. In International Symposium on Shared Memory Multiplvcessors, April 1991.

Google Scholar

[21]

Kenneth L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.

Digital Library

Google Scholar

[22]

R. Milner. Communication and Concurrency. Prentice Hall, New York, 1989.

Digital Library

Google Scholar

[23]

E. M. Sentovich, K. J. Singh, L. Lavagno, C. Moon, R. Murgai, A. Saldanha, H. Savoj, R R. Stephan, R. K. Brayton, and A. L. Sangiovanni-Vincentelli. SIS: A System for Sequential Circuit Synthesis. Technical Report UCB/ERL M92/41, Electronics Research Lab, Univ. of California, Berkeley, CA 94720, May 1992.

Google Scholar

Cited By

View all

Zeng XLiang HYuan JSong XYang G(2023)Generalized Affine Equivalence Checking of Boolean Functions via Reachability AnalysisIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2023.323580242:9(2966-2979)Online publication date: Sep-2023
https://doi.org/10.1109/TCAD.2023.3235802
Rumreich LSivilotti P(2021)Formal Verification of a Java Component Using the RESOLVE FrameworkFrontiers of Combining Systems10.1007/978-3-030-86205-3_16(287-305)Online publication date: 1-Sep-2021
https://doi.org/10.1007/978-3-030-86205-3_16
Subburaj VUrban J(2018)Descartes-Agent: Verifying Formal Specifications Using the Model Checking Technique2018 Second IEEE International Conference on Robotic Computing (IRC)10.1109/IRC.2018.00081(392-398)Online publication date: Jan-2018
https://doi.org/10.1109/IRC.2018.00081
Show More Cited By

Index Terms

HSIS: a BDD-based environment for formal verification
1. Hardware

Recommendations

Efficient Verification of Sequential and Concurrent C Programs

There has been considerable progress in the domain of software verification over the last few years. This advancement has been driven, to a large extent, by the emergence of powerful yet automated abstraction techniques such as predicate abstraction. ...
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 ...
Transition predicate abstraction and fair termination
POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Predicate abstraction is the basis of many program verification tools. Until now, the only known way to overcome the inherent limitation of predicate abstraction to safety properties was to manually annotate the finite-state abstraction of a program. We ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

DAC '94: Proceedings of the 31st annual Design Automation Conference

June 1994

739 pages

ISBN:0897916530

DOI:10.1145/196244

Chairman:
Michael Lorenzetti
Mentor Graphics Corp., Wilsonville, OR

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: 06 June 1994

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Conference

DAC94

Sponsor:

EDAC
SIGDA
IEEE-CAS

DAC94: The 31st ACM/IEEE-CAS/EDAC Design Automation Conference

June 6 - 10, 1994

California, San Diego, USA

Acceptance Rates

DAC '94 Paper Acceptance Rate 100 of 260 submissions, 38%;

Overall Acceptance Rate 1,770 of 5,499 submissions, 32%

Upcoming Conference

DAC '25

Sponsor:
sigda

62nd ACM/IEEE Design Automation Conference

June 22 - 26, 2025

San Francisco , CA , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

40
Total Citations
View Citations
367
Total Downloads

Downloads (Last 12 months)34
Downloads (Last 6 weeks)10

Reflects downloads up to 23 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Zeng XLiang HYuan JSong XYang G(2023)Generalized Affine Equivalence Checking of Boolean Functions via Reachability AnalysisIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2023.323580242:9(2966-2979)Online publication date: Sep-2023
https://doi.org/10.1109/TCAD.2023.3235802
Rumreich LSivilotti P(2021)Formal Verification of a Java Component Using the RESOLVE FrameworkFrontiers of Combining Systems10.1007/978-3-030-86205-3_16(287-305)Online publication date: 1-Sep-2021
https://doi.org/10.1007/978-3-030-86205-3_16
Subburaj VUrban J(2018)Descartes-Agent: Verifying Formal Specifications Using the Model Checking Technique2018 Second IEEE International Conference on Robotic Computing (IRC)10.1109/IRC.2018.00081(392-398)Online publication date: Jan-2018
https://doi.org/10.1109/IRC.2018.00081
Pagliarini SKastensmidt F(2011)VEasyProceedings of the 2011 IEEE International Conference on Microelectronic Systems Education10.1109/MSE.2011.5937102(94-97)Online publication date: 5-Jun-2011
https://dl.acm.org/doi/10.1109/MSE.2011.5937102
Pagliarini SHaacke PKastensmidt F(2011)Evaluating coverage collection using the VEasy functional verification tool suiteProceedings of the 2011 12th Latin American Test Workshop10.1109/LATW.2011.5985893(1-6)Online publication date: 27-Mar-2011
https://dl.acm.org/doi/10.1109/LATW.2011.5985893
Chuck Monahan (2006)Symbolic Modeling and Evaluation of Data Paths32nd Design Automation Conference10.1109/DAC.1995.249979(389-394)Online publication date: Dec-2006
https://doi.org/10.1109/DAC.1995.249979
Tahar SSong XCerny EZhou ZLangevin MAit-Mohamed O(2006)Modeling and formal verification of the Fairisle ATM switch fabric using MDGsIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/43.77117818:7(956-972)Online publication date: 1-Nov-2006
https://dl.acm.org/doi/10.1109/43.771178
Kam TSubrahmanyam P(2006)Comparing layouts with HDL modelsIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/43.37237614:4(503-509)Online publication date: 1-Nov-2006
https://dl.acm.org/doi/10.1109/43.372376
Hojati RIsles AKirkpatrick DBrayton R(2005)Verification using uninterpreted functions and finite instantiationsFormal Methods in Computer-Aided Design10.1007/BFb0031810(218-232)Online publication date: 25-Jun-2005
https://doi.org/10.1007/BFb0031810
Lygeros JGodbole DSastry S(2005)A game-theoretic approach to hybrid system designHybrid Systems III10.1007/BFb0020932(1-12)Online publication date: 10-Jun-2005
https://doi.org/10.1007/BFb0020932
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Get Access

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

Efficient Verification of Sequential and Concurrent C Programs

Formal verification of ASMs using MDGs

Transition predicate abstraction and fair termination