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.

The availability of 4-valued I2L circuits presents a new perspective for digital systems designers. This correspondence explores several aspects of digital system design using 4-valued logic elements. An approach to designing the ith stage of an ALU employing these elements is presented. The realization of rudimentary ALU operations is shown using the T-gate as a universal building block System design based on both Post and Boolean 4-valued logics is discussed.