Don''t-Care Computation via Adjustable Interpolation
Date Issued
2009
Date
2009
Author(s)
Chen, I-Hsin
Abstract
In recent years, there have been a variety of applications of interpolation in logic synthesis and verification, such as functional dependency, bi-decomposition, and Ashenhurst decomposition. The goal of this research is to compute don’t-cares for a given node in a multi-level network by using interpolation. Traditionally, an interpolant can be derived from a refutation proof given by a SAT solver, and its onset can be adjusted via rewriting the structure of the refutation proof. However, in most cases, the interpolant derived by the refutation proof generated by a SAT solver can not be adjusted too much. As a result, the application of interpolation is limited. In this thesis, we propose SAT-based don’t-care computation algorithms via interpolation. In addition, a set of techniques has been developed for a SAT solver to adjust the solution space of the interpolant. The methods include setting the initial variable activities and altering the Boolean initial values. The circuit structure has also been utilized to simplify the problem to accelerate SAT solving. Experiments show that the algorithms can get more don’t-cares while applying the interpolation sizing method to the algorithms.
Subjects
Craig interpolation
logic network
SAT solving
adjustable interpolant
Type
thesis
File(s)![Thumbnail Image]()
Loading...
Name
ntu-98-R95943159-1.pdf
Size
23.32 KB
Format
Adobe PDF
Checksum
(MD5):07d1d61c13f39c874a299b2ce4b5933d