Algorithms and data structures for logic synthesis and verification using Boolean satisfiability

Loading...

View/Download File

Backes_umn_0130E_13529.pdf (1.35 MB)

Persistent link to this item

https://hdl.handle.net/11299/148684

Statistics

View Statistics

Journal Title

Journal ISSN

Volume Title

Title

Algorithms and data structures for logic synthesis and verification using Boolean satisfiability

Authors

Backes, John D.

Published Date

2013-03

Publisher

Type

Thesis or Dissertation

Abstract

Boolean satisfiability (SAT) was the first problem to be proven to be NP-Complete. The proof, provided by Stephen Cook in 1971, demonstrated that inputs accepted by a non-deterministic Turing machine can be described by satisfying assignments of a Boolean formula. The reduction to SAT feels natural for a wealth of decision problems; this has motivated an immense amount of research into heuristics for solving SAT instances quickly. Over the past decade the performance of SAT solvers has improved tremendously, and as a consequence, real-world problems that were once thought to be intractable are now feasible in many cases. In this thesis we discuss how some problems in logic synthesis and verification can be solved with Boolean satisfiability. The dissertation begins by discussing Cyclic Combinational Circuits. Cyclic Combinational Circuits are logic circuits that contain feedback, but exhibit no state behavior. Many functions can be implemented with fewer gates using a cyclic topology rather than an acyclic topology. A pivotal step in synthesizing these circuits is proving whether or not the resulting structure is actually combinational, and if not, how to modify the circuit to behave properly. This analysis can be elegantly cast as an instance of SAT. Furthermore, this thesis demonstrates how modern SATBased synthesis techniques can be used to generate cyclic structures, rather than just analyze them. These SAT-Based synthesis techniques rely on augmenting proofs of unsatisfiability to generate circuit structures. These structures, called Craig Interpolants, and the proofs they are generated from are the focus of the second portion of this dissertation. Techniques are proposed for reducing the size of these interpolants,and then the use of proofs of unsatisfiability as an underlying data structure for synthesis is advocated. Finally, the last portion of this thesis discusses some improvements to a new model checking algorithm known as Property Directed Reachability (PDR). This algorithm iteratively solves SAT instances representing discrete time frames of a sequential circuit in order to demonstrate that a state invariant exists.

Keywords

Automated theorem proving

Boolean satisfiability

Cyclic circuits

Formal verification

Model checking

SAT solving

Description

University of Minnesota Ph.D. dissertation. March 2013. Major:Electrical Engineering. Advisor: Marc D. Riedel. 1 computer file (PDF); xi, 145 pages.

Related to

Replaces

License

Collections

Dissertations

Series/Report Number

Funding information

Isbn identifier

Doi identifier

Previously Published Citation

Suggested citation

Backes, John D.. (2013). Algorithms and data structures for logic synthesis and verification using Boolean satisfiability. Retrieved from the University Digital Conservancy, https://hdl.handle.net/11299/148684.

Content distributed via the University Digital Conservancy may be subject to additional license and use restrictions applied by the depositor. By using these files, users agree to the Terms of Use. Materials in the UDC may contain content that is disturbing and/or harmful. For more information, please see our statement on harmful content in digital repositories.