Formal Design Verification of Digital Systems
- 1 January 1983
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- No. 0738100X,p. 228-234
- https://doi.org/10.1109/dac.1983.1585653
Abstract
In present design automation systems, the standard approach that is taken to verify the correctness of proposed logic designs is that of simulation. However, due to several difficulties that arise as simulation is applied to more complex systems, designers have searched for other techniques to at least augment this traditional approach. The purpose of this paper is to briefly describe a research project to develop a formal design verification system using the Argonne Automated Reasoning Assistant (AURA). Some results of this investigation are presented, together with a discussion of some of the problems that have been encountered and plans for future work.Keywords
This publication has 13 references indexed in Scilit:
- Automated Synthesis of Combinational Logic Using Theorem-Proving TechniquesIEEE Transactions on Computers, 1985
- Automated Design of Multiple-Valued Logic Circuits by Automatic Theorem Proving TechniquesIEEE Transactions on Computers, 1983
- A Verification Technique for Hardware DesignsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1982
- A formal method for computer design verificationPublished by Association for Computing Machinery (ACM) ,1982
- Boolean Comparison of Hardware and FlowchartsIBM Journal of Research and Development, 1982
- A Survey of the State of the Art of Design AutomationComputer, 1981
- Canonicalization and demodulationPublished by Office of Scientific and Technical Information (OSTI) ,1981
- A survey of microprogram verification and validation methodsThe Computer Journal, 1981
- Strum: Structured Microprogram Development System for Correct FirmwareIEEE Transactions on Computers, 1976
- Problems and Experiments for and with Automated Theorem-Proving ProgramsIEEE Transactions on Computers, 1976