test Browse by Author Names Browse by Titles of Works Browse by Subjects of Works Browse by Issue Dates of Works
       

Advanced Search
Home   
 
Browse   
Communities
& Collections
  
Issue Date   
Author   
Title   
Subject   
 
Sign on to:   
Receive email
updates
  
My Account
authorized users
  
Edit Profile   
 
Help   
About T-Space   

T-Space at The University of Toronto Libraries >
School of Graduate Studies - Theses >
Master >

Please use this identifier to cite or link to this item: http://hdl.handle.net/1807/18789

Title: Scaling SAT-based Automated Design Debugging with Formal Methods
Authors: Keng, Brian
Advisor: Veneris, Andreas
Department: Electrical and Computer Engineering
Keywords: Debugging
SAT
VLSI
Formal Methods
Diagnosis
Debug
Issue Date: 12-Feb-2010
Abstract: The size and complexity of modern VLSI computer chips are growing at a rapid pace. Functional debugging is increasingly becoming a bottleneck in the design flow where it can take up to 60% of the total verification time. Scaling existing automated debugging tools is necessary in order to continue along this path of rapid growth and innovation in the semiconductor industry. This thesis aims to scale automated debugging techniques with two contributions. The first contribution introduces a succinct memory model for automated design debugging that dramatically lowers the memory requirements for the debugging problem. The second contribution presents a scalable SAT-based design debugging algorithm that uses a mathematical technique called interpolation to divide the debugging problem into multiple parts across time which greatly reduces the peak memory requirements of the debugging problem. Extensive experiments on real designs demonstrate the benefit of this work.
URI: http://hdl.handle.net/1807/18789
Appears in Collections:Master
The Edward S. Rogers Sr. Department of Electrical & Computer Engineering - Master theses

Files in This Item:

File Description SizeFormat
Keng_Brian_J_200911_MASc_thesis.pdf656.47 kBAdobe PDF
View/Open

Items in T-Space are protected by copyright, with all rights reserved, unless otherwise indicated.

uoft