Abraham, Jacob A.562081522008-08-282017-05-112008-08-282017-05-112003http://hdl.handle.net/2152/715textThe task of checking whether a circuit implementation satisfies an abstract specification, prior to manufacturing the circuit, is extremely important. This is because of the reliance on the abstract specification being predictive of silicon behavior. It is also important to know the exact conditions under which the prediction is guaranteed to be valid. This dissertation delves into the fundamental bottlenecks and issues in model extraction and the inherent difficulties in verifying equivalence of transistor circuit implementations with respect to higher-level specifications. A novel implementation verification methodology that is based on symbolic simulation is presented. In addition, the dissertation presents the general theory of automatic constraint generation that is required for a sound verification strategy and proposes an enhanced implementation verification methodology to eliminate gate/switch-level full-chip simulations. The practical aspects of developing a tool to dovetail into this methodology is also presented.electronicengCopyright is held by the author. Presentation of this material on the Libraries' web site by University Libraries, The University of Texas at Austin was made possible under a limited license grant from the author who has retained all copyrights in the works.Microprocessors--Design and constructionThesis3119627