Automated Synthesis of Combinational Logic Using Theorem-Proving Techniques
- 1 July 1985
- journal article
- Published by Institute of Electrical and Electronics Engineers (IEEE) in IEEE Transactions on Computers
- Vol. C-34 (7) , 610-632
- https://doi.org/10.1109/tc.1985.1676600
Abstract
Recent findings indicate that logic design still constitutes 50 percent of the total design effort, and yet few automated tools are being used in industry. The use of an automated theorem-proving system in the logic design process presents an intriguing addition to traditional design automation tools. This paper deals with the automated synthesis of combinational logic. The method consists of a theorem-proving implementation of a systematic, uniform procedure for the synthesis of an arbitrary switching function. Any multiple-valued (including binary) function can be synthesized in a top-down fashion using the functional blocks of the designer's choice. The method is general enough to allow for the choice of an arbitrary logic system and radix. Additional constraints of modularity, technology dependence, fault tolerance, and others may be imposed upon the design. It may also be possible to accommodate into this approach formal design verification, design for testability, functional level modeling, and formal analysis of race and hazard conditions.Keywords
This publication has 26 references indexed in Scilit:
- Automated Synthesis of Combinational Logic Using Theorem-Proving TechniquesIEEE Transactions on Computers, 1985
- LSI logic testing — An overviewIEEE Transactions on Computers, 1981
- Fault Tolerance of a General Purpose Computer Implemented by Very Large Scale IntegrationIEEE Transactions on Computers, 1980
- Logic Design of Multivalued I2L Logic CircuitsIEEE Transactions on Computers, 1979
- The evolution of digital electronics towards VLSIIEEE Transactions on Electron Devices, 1979
- Synthesis of Multiple-Valued Logic Networks Based on Tree-Type Universal Logic ModuleIEEE Transactions on Computers, 1977
- Methods for Automated Theorem Proving in Nonclassical LogicsIEEE Transactions on Computers, 1976
- Problems and Experiments for and with Automated Theorem-Proving ProgramsIEEE Transactions on Computers, 1976
- A Minimization Technique for Multiple-Valued Logic SystemsIEEE Transactions on Computers, 1968
- Introduction to a General Theory of Elementary PropositionsAmerican Journal of Mathematics, 1921