| CMOS technology has been recognized as a leading contender for existing VLSI systems, and is projected by industry analysts as being the dominant technology for the next decade. In this thesis, a novel approach for representing CMOS logic circuit networks at the transistor level is proposed. Unlike traditional device listing approaches which represent only circuit structures, this representation combines structural data with behavioral information, and thus illustrates a way to reduce the difficulty of information transformation between behavioral and structural representations for CMOS circuits.;Functional recognition of logic components is an important issue in circuit verification. A new method based on functional expansion and logical circuit expressions is proposed, and recognition rules are described. The success of logic component recognition can help other processes such as reverse engineering, which deals with extracting logic-level components from layouts of unknown-function circuits, and the comparison of CMOS transistor schematic networks. Functional recognition enhances the schematic comparison process in that it brings the comparison up to higher levels.;Traditional approaches which use graph matching algorithms for CMOS schematic comparison have difficulty in matching circuits with the same function but different topologies. Other approaches dealing with schematic comparison such as switch-level simulation need to exercise all possible input patterns, require a large amount of time, and thus are not practical for medium- or large-sized circuits. The approach in this thesis for CMOS schematic comparison is to represent a CMOS transistor network by a set of logical circuit expressions, so that the comparison process is not as rigid as graph matching approaches and yet is efficient enough to compare two functionally isomorphic circuits. The shift from graph connectivity to logical circuit expressions allows schematics comparison for matching functionally isomorphic structures, while most graph-based approaches can handle only topologically isomorphic circuits.;Automated CMOS design and verification using predicates is also described in this thesis. A context-free grammar and a pushdown automata are proposed so that the synthesis and verification processes for series-parallel networks can be done in linear time. ITP, an interactive theorem prover developed at Argonne National Laboratory, is used to demonstrate the capability of the approach. |
