The problem of extracting RTL modules from a gate level netlist has many interesting applications in digital design (V.K. Madiseti, 1999; P. Schaumont et al., 1999; K. Singh and P. Subrahmunyam, 1995), because it provides a conceptual description of the circuit. We approach this transformation by solving two subproblems: the identification of potential modules (candidate subcircuits) and testing them for functional equivalence to known high-level modules (subcircuit identification). We present a technique for unique and comprehensive enumeration of subgraphs of an arbitrary graph, as well as a method of recognizing subgraph isomorphisms. Combined, these results provide a solution to the problem of candidate subcircuit enumeration. These techniques provide both theoretical and practical contributions within design automation and graph theory.

Recovering functional information from existing hardware is a difficult problem in design automation. However, it is an important focus for designers attempting to redesign for expanded functionality or superior performance. Often, the only reliable information available about a piece of digital hardware is the hardware itself. Documentation, even if it is available, may be outdated or incorrect. Existing procedures are able to recover the transistor-level netlist, or a gate-level netlist from an existing implementation. The next step in this process is the gate-level to module-level transformation, the focus of this paper. We have designed a technique to enumerate all of the potential modules within a gate-level netlist so that their functional equivalence to known modules may be evaluated.

Motivated by the problem of reengineering legacy digital circuits for which design information is missing or incomplete, this paper presents a new technique for representing the relationships among the internal components of a combinational circuit. This technique proves to be a powerful tool for redesign, capable of representing internal Boolean relationships in a fully or partially specified multiple-output combinational circuit with a single data structure.

The paper describes work that represents the culmination of a comprehensive hardware/software modeling and analysis project concerning the Charles Stark Draper Laboratory Fault-Tolerant Processor (FTP). The FTP performs a safety related function at the Integral Fast Reactor (IFR, previously known as the Experimental Breeder Reactor-II) operated by Argonne National Laboratory for the Department of Energy. Previously, we demonstrated the tolerance to hardware failures of data exchange instructions on the FTP (G.H. Chisholm et al., 1987; A.J. Kljaich et al., 1989; A.S. Wojcik et al., 1984; A.S. Wojcik, 1983). We describe a methodology for assuring that the software executing on the FTP is also tolerant to hardware failures. This methodology is based on an abstraction of the program data and control flows in terms of the specification of an abstract application program that operates on the FTP. We then prove the fault tolerance of the abstract application program to hardware and sensor failures. Based on a more detailed specification and analysis of the code that is used in the application software, we demonstrate that this code satisfies the sufficient conditions developed for the abstract application program to claim system fault tolerance.

The problem of finding meaningful subcircuits in a logic layout appears in many contexts in computer-aided design. Existing techniques rely upon finding exact matchings of subcircuit structure within the layout. These syntactic techniques fail to identify functionally equivalent subcircuits which are differently implemented optimized, or otherwise obfuscated. We present a mechanism for identifying functionally equivalent subcircuits which is capable of overcoming many of these limitations. Such semantic matching is particularly useful in the field of design recovery.

The use of redundancy to attain a fault-tolerant system design is described. Specifically, a general theory of redundancy is proposed that allows the design of fault-tolerant structures at the system-level, gate-level, or both. The theory accounts for classic approaches to redundant design such as TMR, NMR, and quadded and interwoven logics. It is shown that, by using mathematical block theory, it is possible to describe complex interconnections of redundant elements in a simple, straightforward fashion. Comparisons are made with other approaches to redundant design.>

A formal verification system based on the use of automated reasoning techniques is described to validate fault tolerance. An extended Petri net representation, called a flow net, is described together with the theorem-proving implementation of a rule-based system for manipulating system descriptions. Examples taken from the literature are used to illustrate the representation and the capabilities of the formal verification system under development.>

A decomposition approach to the modular design of multiple-valued logic functions is discussed. Systematic procedures to utilize a fixed set of building blocks from which an arbitrary function can be designed are illustrated. The building blocks are composed of T gates (multiplexers). The first step is the partitioning of all logic functions into classes. Representative building blocks for each class are then developed. Finally, optimization techniques are described that reduce the number of building blocks required in the design. This approach is, in principle, applicable to functions in any radix and will always yield a design for the target function. Examples are presented to illustrate the approach for ternary functions.>

A novel rule-based circuit representation is proposed to describe the connectivities of CMOS circuits at the transistor level. The unique feature of the rule-based representation is its ability to automate CMOS circuit design and verification. A precise symbolic description of the functionality of a transistor-level circuit can be derived based on a set of production rules in linear time. Automated synthesis and verification of CMOS logic circuits are demonstrated.

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.

This paper describes a method for the automatic synthesis of multiple-valued combinational logic circuits using automatic theorem proving techniques. Logic design of multiple-valued circuits is considerably more complex than binary design because of the associated combinatorial explosion. Two general approaches which can be taken in axiomatizing the environment of combinational logic design in multiple-valued logic have been investigated. These axiomatizations, formulated in the language of first order logic, are used to state the problem of combinational logic design as a theorem proving problem. This formulation together with a representation of the function being designed can be used as input to an automatic theorem proving program. The circuit design can then be obtained from the proof generated by the theorem prover.

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.

The use of three-valued signals in the design of asynchronous speed-independent modules is considered. The three-valued Post algebra is used as the mathematical basis for multivalued logic design. Asynchronous operation in a three-valued system is defined. Basis data/control signal detectors and control primitives are developed. It is shown that the design of the nonbinary modules only requires the use of standard binary design techniques and the detectors and logic primitives that are developed. A general monitoring and control structure that allows the interconnection of both combinational and sequential modules is described.

The fundamentals of Post algebras are presented and Post and Boolean functions are examined. A functional representation is developed that facilitates the comparison of Post and Boolean algebras. Based on this representation, relationships between finite, higher-order (that is, more than 2-valued) Boolean algebras and functions in these algebras and finite, higher-order Post algebras and their corresponding functions are develop.

The use of N-valued logics in the design of base N adder circuits is considered. Two types of N-valued logics are examined, Post N-valued logics and binary-coded N-valued logics. Specific implementations of these nonbinary logics are discussed. General formulas for the sum and carry functions of an adder are established in order to calculate the cost of base N adder stages using the Post logics. Relative costs of the base N adders using both types of N-valued logics are discussed in terms of a cost function. It is shown that for the model used, the binary-coded logics yield adders that have, in general, lower relative cost than comparabloe adders based on the Post logics, and that base 2 adders have a lower relative cost than the base N adders.