Fast Static Learning and Inductive Reasoning with Applications to ATPG Problems

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.

Name thesis:degree_name

Master of Science

Level thesis:degree_level

masters

Discipline thesis:degree_discipline

Computer Engineering

Department dc:contributor.department

Electrical and Computer Engineering

Grantor dc:publisher

Virginia Tech

Year dc:date.issued

2015

Author dc:creator

• Dsouza, Michael Dylan

Chair dc:contributor.committeechair

• Hsiao, Michael S.

Committee members dc:contributor.committeemember

• Schaumont, Patrick R.
• Wang, Chao

• Static learning
• inductive reasoning
• multi-node invariants
• logic implications
• boolean constraint propagation

Statement dc:rights

• In Copyright

Licence dc:rights.uri

• http://rightsstatements.org/vocab/InC/1.0/

Dc Identifier Other

vt_gsexam:4682

OAI identifier oai:identifier

oai:vtechworks.lib.vt.edu:10919/51591