Article

Free access

A formal design verification system based on an automated reasoning system

Authors:

Anthony S. Wojcik,

Joseph Kljaich,

Nagendra SrinivasAuthors Info & Claims

DAC '84: Proceedings of the 21st Design Automation Conference

Pages 641 - 647

Published: 25 June 1984 Publication History

Abstract

In recent years, interest has grown in the possibility of developing a formal design verification approach as an alternative to standard simulation techniques for verification. Several researchers have used, or suggested the use of, artificial intelligence techniques in such a formal system.

The purpose of this paper is to briefly describe the ongoing work on the development of a viable formal design verification system based on an automated reasoning system. This system, called LMA (Logic Machine Architecture), has been developed at Argonne National Laboratory. This paper describes the basic ideas underlying this formal system for verification and discusses several of the current research projects.

References

[1]

Wagner, T. J., "Verification of Hardware Designs Through Symbolic Manipulation", Proceedings of the Symposium on Design Automation and Microprocessors, Palo Alto, CA., pp. 50-53, February 1977.

Digital Library

[2]

Wagner, T. J., "Hardware Verification", Ph.D. Dissertation, Computer Science Department, Stanford University, Report No. STAN-CS-77-632, September 1977.

Digital Library

[3]

Darringer, J. A., "The Application of Program Verification Techniques to Hardware Verification", Proceedings of the 16th Design Automation Conference, San Diego, CA., pp. 375-381, June 1979

Digital Library

[4]

Akers, S. B., "A Procedure for Functional Design Verification", General Electric Company, Electronics Laboratory Report, Syracuse, New York, December 1979.

[5]

Smith, G. L., et al, "Boolean Comparison of Hardware and Flowcharts", IBM Journal of Research and Development, Vol. 26, No. 1, pp. 106-116, January 1982.

Digital Library

[6]

Pitchumani,V., "Methods of Verification of Digital Logic" Ph.D. Dissertation, Department of Electrical Engineering, Syracuse University, February 1981.

[7]

Pitchumani, V. and Stabler, E.P., "A Formal Method for Computer Design Verification", Proceedings of the 19th Design Automation Conference, Las Vegas, Nevada, June, 1982, pp. 809-814.

Digital Library

[8]

Maruyama, F., Uchara, T., Kawato, N. and Saito, T., "A Verification Technique for Hardware Designs", Proceedings of the 19th Design Automation Conference, Las Vegas, Nevada, June 1982, pp. 832-841.

Digital Library

[9]

Haynes, L., "Logic Design Verification Using Static Analysis", Ph.D. Dissertation, Coordinated Science Laboratory Report University of Illinois at Urbana-Champaign, May 1983.

[10]

Umrigar, Z. and Pitchumani, V., "Formal Verification of a Real-Time Hardware Design", Proceedings of the 20th Design Automation Conference, Miami Beach, FL, pp. 221-227, June 1983.

Digital Library

[11]

Wojcik, A. S., "Formal Design Verification of Digital Systems", Proceedings of the 20th Design Automation Conference, Miami Beach, FL, pp. 228-234, June 1983.

Digital Library

[12]

Barrow, H. G., "Proving the Correctness of Digital Hardware Designs", Proceedings of the National Conference on Artificial Intelligence, AAAI-83, August 1983.

[13]

McCharen, J. D., Overbeek, R.A. and Wos, L., "Problems and Experiments for and with Automated Theorem-Proving Programs", IEEE Transactions on Computers, Vol. C-25, pp. 773-782, August 1976.

[14]

Smith, B. T., "Reference Manual for the Environmental Theorem Prover", Argonne National Laboratory, Applied Mathematics Division Internal Report, April 1982.

[15]

Kabat, W. C. and Wojcik, A. S., "Automated Synthesis of Combinational Logic Using Theorem Proving Techniques", Proceedings of the 12th International Symposium on Multiple-Valued Logic, Paris, Frances, pp. 178-199, May 1982.

[16]

Wojciechowski, W. S. and Wojcik, A. S., "Automated Design of Multiple-Valued Logic Circuits by Automatic Theorem Proving Techniques", IEEE Transactions on Computers, September 1983.

Digital Library

[17]

Lusk, E. L. and Overbeek, R. A., "An LMA-Based Theorem Prover", Argonne National Laboratory Mathematics and Computer Science Division Report, 82-75, December 1982.

[18]

Clocksin, W. F. and Mellish, C. S., Programming in PROLOG, Springer-Verlag, 1981

Digital Library

[19]

Loveland, D.W., Automated Theorem Proving: A Logical Basis, North-Holland Publishing Co., 1978.

Digital Library

[20]

Wos, L., Overbeek, R., Lusk, E. and Boyle, J., Automated Reasoning, Introduction and Applications, Prentice-Hall, Inc., 1984.

Digital Library

[21]

Peterson, J. L., Petri-Net Theory and the Modeling of Systems, Prentice-Hall, Inc., 1981.

Digital Library

[22]

Veroff, R. and Qiuntero, O., "Verification of the Logical Design of Digital Circuits Using an Automated Reasoning System", submitted to the Seventh Conference on Automated Deduction, May 1984.

Cited By

Chisholm GWojcik A(1999)An Application of Formal Analysis to Software in a Fault-Tolerant EnvironmentIEEE Transactions on Computers10.1109/12.80515548:10(1053-1064)Online publication date: 1-Oct-1999
https://dl.acm.org/doi/10.1109/12.805155
Berthet CCerny E(1988)An Algebraic Model for Asynchronous Circuits VerificationIEEE Transactions on Computers10.1109/12.222937:7(835-847)Online publication date: 1-Jul-1988
https://dl.acm.org/doi/10.1109/12.2229
Wu CWojcik ANi L(1987)A rule-based circuit representation for automated CMOS design and verificationProceedings of the 24th ACM/IEEE Design Automation Conference10.1145/37888.38012(786-792)Online publication date: 1-Oct-1987
https://dl.acm.org/doi/10.1145/37888.38012
Show More Cited By

Index Terms

A formal design verification system based on an automated reasoning system
1. Hardware
  1. Electronic design automation
    1. High-level and register-transfer level synthesis
  2. Hardware validation
    1. Functional verification
2. Theory of computation
  1. Logic
    1. Logic and verification

Recommendations

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 ...
Formal Verification for Embedded System Designs

Embedded electronics today are becoming increasingly complex, which makes their design and analysis more and more difficult. In this paper, we focus on the formal verification of embedded system designs at multiple levels of abstraction, enabled by the ...
Synchronization verification in system-level design with ILP solvers
MEMOCODE '05: Proceedings of the 2nd ACM/IEEE International Conference on Formal Methods and Models for Co-Design

Concurrency is one of the most important issues in system-level design. Interleaving among parallel processes can cause an extremely large number of different behaviors, making design and verification difficult tasks. In this work, we propose a ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

DAC '84: Proceedings of the 21st Design Automation Conference

June 1984

715 pages

ISBN:0818605421

Sponsors

SIGDA: ACM Special Interest Group on Design Automation
IEEE: Institute of Electrical and Electronics Engineers
IEEE-CS: Computer Society

Publisher

IEEE Press

Publication History

Published: 25 June 1984

Check for updates

Qualifiers

Article

Acceptance Rates

DAC '84 Paper Acceptance Rate 116 of 290 submissions, 40%;

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

4
Total Citations
View Citations
223
Total Downloads

Downloads (Last 12 months)58
Downloads (Last 6 weeks)7

Reflects downloads up to 16 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Chisholm GWojcik A(1999)An Application of Formal Analysis to Software in a Fault-Tolerant EnvironmentIEEE Transactions on Computers10.1109/12.80515548:10(1053-1064)Online publication date: 1-Oct-1999
https://dl.acm.org/doi/10.1109/12.805155
Berthet CCerny E(1988)An Algebraic Model for Asynchronous Circuits VerificationIEEE Transactions on Computers10.1109/12.222937:7(835-847)Online publication date: 1-Jul-1988
https://dl.acm.org/doi/10.1109/12.2229
Wu CWojcik ANi L(1987)A rule-based circuit representation for automated CMOS design and verificationProceedings of the 24th ACM/IEEE Design Automation Conference10.1145/37888.38012(786-792)Online publication date: 1-Oct-1987
https://dl.acm.org/doi/10.1145/37888.38012
Smith B(1985)Position paper to be presented at "Verification workshop III (verkshop III)" to be held in Watsonville, CA. Feb. 18--21, 1985ACM SIGSOFT Software Engineering Notes10.1145/1012497.101252010:4(61-62)Online publication date: 1-Aug-1985
https://dl.acm.org/doi/10.1145/1012497.1012520

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

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

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents