Search algorithms for satisfiability problems in combinational switching circuits.
dc.contributor.author | Marques da Silva, Joao Paulo | en_US |
dc.contributor.advisor | Sakallah, Karem A. | en_US |
dc.date.accessioned | 2014-02-24T16:22:57Z | |
dc.date.available | 2014-02-24T16:22:57Z | |
dc.date.issued | 1995 | en_US |
dc.identifier.other | (UMI)AAI9542904 | en_US |
dc.identifier.uri | http://gateway.proquest.com/openurl?url_ver=Z39.88-2004&rft_val_fmt=info:ofi/fmt:kev:mtx:dissertation&res_dat=xri:pqm&rft_dat=xri:pqdiss:9542904 | en_US |
dc.identifier.uri | https://hdl.handle.net/2027.42/104664 | |
dc.description.abstract | A number of tasks in computer-aided analysis of combinational circuits, including test pattern generation, timing analysis, delay fault testing and logic verification, can be viewed as particular formulations of the satisfiability problem (SAT). The first purpose of this dissertation is to describe a configurable search-based algorithm for SAT that can be used for implementing different circuit analysis tools. Several methods for reducing the amount of search are detailed and integrated into a general algorithmic framework for solving SAT. Special emphasis is given to the description of methods for diagnosing the causes of conflicts that may be identified while searching for a solution to each instance of SAT. These methods allow the implementation of non-chronological backtracking, conflict identification based on equivalence relations and logic value assertions derived from conflicts. Path sensitization in combinational circuits is often used to solve test pattern generation, timing analysis and delay fault testing problems. While path sensitization can be cast as an instance of SAT, such an approach can conceal desirable structural properties of the problem and may lead to exponential size representations. Another purpose of this dissertation is to introduce a new model for path sensitization that permits modeling test pattern generation and timing analysis with linear size representations. In addition, this formulation for path sensitization permits the adaptation of all the pruning methods developed for the general SAT problem. The proposed SAT algorithms and path sensitization model form an initial kernel for the development of tools for the analysis of combinational circuits. Their practical applicability is supported by experimental results obtained with test pattern generation and timing analysis tools. | en_US |
dc.format.extent | 291 p. | en_US |
dc.subject | Engineering, Electronics and Electrical | en_US |
dc.subject | Computer Science | en_US |
dc.title | Search algorithms for satisfiability problems in combinational switching circuits. | en_US |
dc.type | Thesis | en_US |
dc.description.thesisdegreename | PhD | en_US |
dc.description.thesisdegreediscipline | Electrical Engineering | en_US |
dc.description.thesisdegreegrantor | University of Michigan, Horace H. Rackham School of Graduate Studies | en_US |
dc.description.bitstreamurl | http://deepblue.lib.umich.edu/bitstream/2027.42/104664/1/9542904.pdf | |
dc.description.filedescription | Description of 9542904.pdf : Restricted to UM users only. | en_US |
dc.owningcollname | Dissertations and Theses (Ph.D. and Master's) |
Files in this item
Remediation of Harmful Language
The University of Michigan Library aims to describe library materials in a way that respects the people and communities who create, use, and are represented in our collections. Report harmful or offensive language in catalog records, finding aids, or elsewhere in our collections anonymously through our metadata feedback form. More information at Remediation of Harmful Language.
Accessibility
If you are unable to use this file in its current format, please select the Contact Us link and we can modify it to make it more accessible to you.