Search State Extensibility based Learning Framework for Model Checking and Test Generation
|dc.description.abstract||The 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.
|dc.rights||I hereby certify that, if appropriate, I have obtained and attached hereto a written permission statement from the owner(s) of each third party copyrighted matter to be included in my thesis, dissertation, or project report, allowing distribution as specified below. I certify that the version I submitted is the same as that approved by my advisory committee. I hereby grant to Virginia Tech or its agents the non-exclusive license to archive and make accessible, under the conditions specified below, my thesis, dissertation, or project report in whole or in part in all forms of media, now or hereafter known. I retain all other ownership rights to the copyright of the thesis, dissertation or project report. I also retain the right to use in future works (such as articles or books) all or part of this thesis, dissertation, or project report.||en_US|
|dc.subject||Design Veriï¬ cation||en_US|
|dc.subject||Automatic Test Generation and Fault Diagnosis||en_US|
|dc.title||Search State Extensibility based Learning Framework for Model Checking and Test Generation||en_US|
|dc.contributor.department||Electrical and Computer Engineering||en_US|
|thesis.degree.grantor||Virginia Polytechnic Institute and State University||en_US|
|thesis.degree.discipline||Electrical and Computer Engineering||en_US|
Files in this item
This item appears in the following Collection(s)
Doctoral Dissertations