| Summary: | Relations among various nodes in the circuit, as captured by static and inductive invariants,
have shown to have a positive impact on a wide range of EDA applications. Techniques such
as boolean constraint propagation for static learning and assume-then-verify approach to
reason about inductive invariants have been possible due to efficient SAT solvers. Although
a significant amount of research effort has been dedicated to the development of effective
invariant learning techniques over the years, the computation time for deriving powerful
multi-node invariants is still a bottleneck for large circuits. Fast computation of static
and inductive invariants is the primary focus of this thesis. We present a novel technique
to reduce the cost of static learning by intelligently identifying redundant computations
that may not yield new invariants, thereby achieving significant speedup. The process of
inductive invariant reasoning relies on the assume-then-verify framework, which requires
multiple iterations to complete, making it infeasible for cases with a large set of multi-node
invariants. We present filtering techniques that can be applied to a diverse set of multi-node
invariants to achieve a significant boost in performance of the invariant checker. Mining and
reasoning about all possible potential multi-node invariants is simply infeasible. To alleviate
this problem, strategies that narrow down the focus on specific types of powerful multi-node
invariants are also presented. Experimental results reflect the promise of these techniques.
As a measure of quality, the invariants are utilized for untestable fault identification and to
constrain ATPG for path delay fault testing, with positive results. === Master of Science
|
|---|
