Type of Document Dissertation Author Chandrasekar, Maheshwar Author's Email Address email@example.com URN etd-09142010-095057 Title Search State Extensibility based Learning Framework for Model Checking and Test Generation Degree PhD Department Electrical and Computer Engineering Advisory Committee
Advisor Name Title No Advisors Found Keywords
- Design Veriﬁcation
- Automatic Test Generation and Fault Diagnosis
- Fault Model
- Model Checking
Date of Defense 2010-09-10 Availability unrestricted AbstractThe increasing design complexity and shrinking feature size of hardware designs have created resource intensive design veriﬁcation and manufacturing test phases in the product life-cycle of a digital system. On the contrary, time-to-market constraints require faster veriﬁcation and test phases; otherwise it may result in a buggy design or a defective product. This trend in the semiconductor industry has considerably increased the complexity and importance of Design Veriﬁcation, Manufacturing Test and Silicon Diagnosis phases of a digital system production life-cycle. In this dissertation, we present a generalized learning framework, which can be customized to the common solving technique for problems in these three phases.
During Design Veriﬁcation, the conformance of the ﬁnal design to its speciﬁcations is veriﬁed. Simulation-based and Formal veriﬁcation are the two widely known techniques for design veriﬁcation. Although the former technique can increase conﬁdence in the design, only the latter can ensure the correctness of a design with respect to a given speciﬁcation. Original ly, Design Veriﬁcation techniques were based on Binary Decision Diagram (BDD) but now such techniques are based on branch-and-bound procedures to avoid space explosion. However, branch-and-bound procedures may explode in time; thus efficient heuristics and intel ligent learning techniques are essential. In this dissertation, we propose a novel extensibility relation between search states and a learning framework that aids in identifying non-trivial redundant search states during the branch-and-bound search procedure. Further, we also propose a probability based heuristic to guide our learning technique. First, we utilize this framework in a branch-and-bound based preimage computation engine. Next, we show that it can be used to perform an upper-approximation based state space traversal, which is essential to handle industrial-scale hardware designs. Final ly, we propose a simple but elegant image extraction technique that utilizes our learning framework to compute over-approximate image space. This image computation is later leveraged to create an abstraction-reﬁnement based model checking framework.
During Manufacturing Test, test patterns are applied to the fabricated system, in a test environment, to check for the existence of fabrication defects. Such patterns are usual ly generated by Automatic Test Pattern Generation (ATPG) techniques, which assume certain fault types to model arbitrary defects. The size of fault list and test set has a major impact on the economics of manufacturing test. Towards this end, we propose a fault col lapsing approach to compact the size of target fault list for ATPG techniques. Further, from the very beginning, ATPG techniques were based on branch-and-bound procedures that model the problem in a Boolean domain. However, ATPG is a problem in the multi-valued domain; thus we propose a multi-valued ATPG framework to utilize this underlying nature. We also employ our learning technique for branch-and-bound procedures in this multi-valued framework.
To improve the yield for high-volume manufacturing, silicon diagnosis identiﬁes a set of candidate defect locations in a faulty chip. Subsequently physical failure analysis - an extremely time consuming step - utilizes these candidates as an aid to locate the defects. To reduce the number of candidates returned to the physical failure analysis step, efficient diagnostic patterns are essential. Towards this objective, we propose an incremental framework that utilizes our learning technique for a branch-and-bound procedure. Further, it learns from the ATPG phase where detection-patterns are generated and utilizes this information during diagnostic-pattern generation. Finally, we present a probability based heuristic for X-filling of detection-patterns with the objective of enhancing the diagnostic resolution of such patterns. We unify these techniques into a framework for test pattern generation with good detection and diagnostic ability. Overal l, we propose a learning framework that can speed up design verification, test and diagnosis steps in the life cycle of a hardware system.
Filename Size Approximate Download Time (Hours:Minutes:Seconds)
28.8 Modem 56K Modem ISDN (64 Kb) ISDN (128 Kb) Higher-speed Access Chandrasekar_M_D_2010.pdf 1.41 Mb 00:06:31 00:03:21 00:02:56 00:01:28 00:00:07
If you have questions or technical problems, please Contact DLA.