請用此 Handle URI 來引用此文件:
http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/16097
標題: | 基於內插法與滿足性之邏輯修正 Interpolation and SAT-Based Logic Rectification |
作者: | Kai-Fu Tang 湯凱富 |
指導教授: | 黃鐘揚 |
關鍵字: | 邏輯修正,內插法,滿足性, logic rectification,interpolation,satisfiability, |
出版年 : | 2012 |
學位: | 博士 |
摘要: | In modern VLSI designs, late design changes are nearly inevitable to fix the design bugs or to cope with the specification changes. Due to the cost and time-to-market pressure, it is unlikely that designers would like to modify the register-transfer level (RTL) design and re-run the whole design flow from the beginning. Instead, they identify a patch circuit to rectify the gate-level design for the differences. This process is called logic rectification.
This dissertation focuses on two closely related rectification problems: rectification for application-specific integrated circuits (ASICs) and field-programmable gate arrays (FPGAs). Rectification for ASICs For a design with multiple functional errors, multiple patches are usually needed to correct the design. Previous works on logic rectification are limited to single-output patch. In other words, only one erroneous behaviors can be fixed in one iteration. As a result, it may lead to unnecessarily large patches or even failure in rectification. We generalize the existing rectification techniques to a great extent and propose direct and incremental logic rectifications. For direct logic rectification, we derive multiple-output patch by interpolation with cofactor reduction. The multiple-output patch considers multiple design errors simultaneously. For incremental logic rectification, single- and multiple-output partial patches are identified in an iterative manner. Our experiments incorporate both direct and incremental methods, and the algorithms perform well on large designs. Rectification for FPGAs We present rectification methods for look-up table (LUT) type FPGAs to correct an erroneous circuit implementation by in-place logic reconfiguration; that is, we only reconfigure the functions of the LUTs and do not change the routing of the erroneous circuit. Therefore, the rectification can be very efficient since the relatively much more expensive re-routing can be avoided. Our proposed algorithm is based on the Boolean satisfiability (SAT) solver and use dynamic learning techniques to accelerate the computation. To enhance the reconfiguration power, both direct and incremental methods are investigated. Experimental results demonstrate that the learning techniques are effective in pruning infeasible solutions for both academic and industrial benchmarks. |
URI: | http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/16097 |
全文授權: | 未授權 |
顯示於系所單位: | 電子工程學研究所 |
文件中的檔案:
檔案 | 大小 | 格式 | |
---|---|---|---|
ntu-101-1.pdf 目前未授權公開取用 | 6 MB | Adobe PDF |
系統中的文件,除了特別指名其著作權條款之外,均受到著作權保護,並且保留所有的權利。