- 學位論文
以有序二元決策圖為基礎的布林轉換解決記憶體修復及網路可靠度問題
Solving Memory Reconfiguration and Network Reliability Problems with BDD-based Boolean Transformations
摘要
在大量製造的半導體產業中，欲生產無瑕疵記憶體單元(memory cell)的記憶體晶片的渴望從未消失。然而，當記憶體晶片的密度隨著VLSI科技的快速進展而逐漸增加之際，要生產無瑕疵的記憶體晶片變得越來越困難。對於一個有著一致結構的裝置而言，例如動態隨機儲存記憶體，使用備用行以及備用列是彌補記憶體晶片中出現瑕疵記憶體單元的一種有效方法。有這種備份配置的裝置叫做可重設的記憶體陣列(reconfigurable memory array)。搜尋一個用備份原件取代瑕疵記憶體單元的解的過程叫做記憶體修復問題或者備份配置問題。備份配置問題已經被證明是一個NP-complete問題。本論文第一部分描述一個把記憶體修復問題轉換成一系列布林(Boolean)函式運算的布林轉換技巧。一個重設解可以從這一系列函式中的其中一個函式得到。本文提到的布林轉換技巧並不侷限使用在備份配置問題中，該技巧也可以應用到其它領域的問題。 在過去，很多的演算法被提出來解決連接點為完全可靠的網路的可靠度計算問題。這類問題已被證明是NP-complete問題。然而，在真實世界中連線與連接點都可能損壞。在計算網路可靠度的時候，把不完全可靠的連接點也考慮在內會讓演算法的效率變的更差。本論文第二部分提出一個額外運算量很低的演算法來把不可靠的連接點的效果也考慮在網路可靠度的計算之中。在設計一個網路拓撲的時候，了解哪個元件的失效對網路可靠度最大是非常重要的事，因為可以使用更好的元件在最重要元件的位置或者重新設計網路拓撲。本論文也提出一個非常有效率的演算法來找出最重要的網路元件。 有效的布林函式工具對於本論文所提出的方法是非常必要的，而有序二元決策圖以及布林滿足工具(Boolean satisfiability solver)是兩個非常有效率的工具。在記憶體修復問題中的布林運算可用任何求布林解的工具進行運算，例如上述的二元決策圖以及布林滿足工具。然而，在網路可靠度運算中的可靠度函式或者系統失效(unavailability)函式則必須儲存在可以遊走(traversable)的資料結構內。此外，這些結構也必須自動可以把獨立事件乘積和編碼在結構內。這些要求使得布林滿足工具無法被使用在網路可靠度運算中。因此，有序二元決策圖是本論文中用來解布林運算的主要工具，也是探討的焦點。
並列摘要
In volume semiconductor industries, the desire to produce as many defect-free memory chips as possible never ceases. However, as the density of memory chips grows constantly along with the rapid advancement of VLSI technology, it becomes harder and harder to fabricate memory chips containing no defect. For devices having a uniform structure such as dynamic random access memories, introducing spare rows as well as spare columns is one of the effective solutions to compensate for the occurrence of faulty cells. Devices with such redundancy are known as reconfigurable memory arrays. Searching for a solution which replaces with spares all faulty cells of a reconfigurable memory array is called the memory reconfiguration problem or the spare allocation problem. The spare allocation problem has been shown to be NP-complete. The first part of this thesis describes an efficient Boolean transformation technique which transforms a memory reconfiguration problem into a set of Boolean function operations. A repair solution can then be derived from one of the Boolean functions. The idea of the Boolean transformation technique is not limited to spare allocation problems. It can also be applied to problems in other fields. In the past, many algorithms have been presented to solve network reliability evaluation problems in which vertices are considered perfectly reliable. Such problems have been shown to be a NP-hard problem. However, the vertices as well as the links of a network can fail in the real world. Taking the effect of imperfect vertices into account makes the performance of these algorithms worse. The second part of this thesis presents two low overhead strategies for taking into account the imperfect vertices in a network. In the design of a network topology, it is important to identify the most crucial component, i.e. a vertex or a link, of a network so that efforts can be made to keep it functional. A highly efficient algorithm is also presented in this part to identify the most crucial component of a network. The algorithms presented in the second part require a tool capable of encoding SDP (sum of disjoint products) forms of a Boolean expression. Efficient tools for Boolean function manipulations are essential for the Boolean encoding/transformation techniques presented in this thesis. The reduced ordered binary decision diagram and the Boolean satisfiability (SAT) are two of the efficient tools. The Boolean operations in the memory reconfiguration problem can be performed with any Boolean solvers, such as the SAT solver or the reduced ordered binary decision diagram. However, a reliability or unavailability expression in the network reliability evaluation problem needs to be stored in a traversable data structure which implicitly encodes the SDP forms of the expression. These requirements exclude the SAT solver from being used in the network reliability evaluation problem. The reduced ordered binary decision diagram is therefore the primary tool used in this thesis.