利用必然性模型檢測技術所進行之循序電路功能修正

Functional Rectification on Sequential Circuits by Liveness Model Checking Techniques

林暐勛(Wei-Hsun Lin)

指導教授 ： 黃鐘揚

國立臺灣大學/電機資訊學院/電子工程學研究所/碩士(2012年)

https://doi.org/10.6342/NTU.2012.02665

摘要

在超大型積體電路設計階段中，功能修正已變成一個不可或缺的過程。傳統上，功能修正藉由許多組合電路的技術而達成，然而其並沒有考慮暫存器對於功能改變的彈性，因此，這些組合電路的技術並沒有辦法直接使用在有不匹配暫存器的循序電路上。在這篇論文中，我們提出了一個修正循序電路的方法，其使用了必然性模型檢測技術來檢驗舊設計電路與新規格電路的可修正性。此外，我們利用了內插邏輯技術來產生修正函數，並藉由找尋較好的基底變數，加速了整體修正過程。實驗結果顯示我們所提出的方法可以有效率地決定一個給定的信號是否可以將電路修正，並且能有效地產生夠小的修正函數。最後，我們的方法提供了組合性修正另一條路，而且可於大部分的實驗中產生較小的修正函數。

關鍵字

功能修正 ； 必然性性質 ； 模型檢測

並列摘要

Functional rectification has been an indispensable process in late VLSI design stages. Traditionally, functional rectification is achieved by various techniques on combinational circuits. It does not explore the flexibility of functional changes across the register boundary. As a result, these combinational rectification techniques cannot be applied directly to sequential circuits with unmatched registers. In this thesis, we propose a sequential rectification approach, which utilizes the liveness model checking techniques to facilitate checking of the sequential rectifiability between old implementation and golden specification. In addition, we apply the interpolation technique to construct the rectification function (i.e. the patch). By identifying better supports for the patch generation, we demonstrate that the whole procedure can be accelerated. Experimental results show that our method can efficiently determine whether a given signal is a rectification signal and find the patch circuits effectively. In the end, our method can provide an alternative way to the combinational rectification and it generates smaller in most of cases.

並列關鍵字

Functional Rectification ； Liveness Property ； Model Checking

參考文獻

[1] Andreas G. Veneris and Ibrahim N. Hajj. Design error diagnosis and correction via test vector simulation. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 18(12): 1803-1816, 2006.

[3] Bo-Han Wu, Chun-Ju Yang, Chung-Yang Huang, and Jie-Hong Roland Jiang. A robust functional ECO engine by SAT proof minimization and interpolation techniques. In Proceedings of International Conference on Computer-Aided Design, pages 729–734, 2010.

[4] Kai-Fu Tang, Chi-An Wu, Po-Kai Huang, and Chung-Yang (Ric) Huang. Interpolation-based incremental ECO synthesis for multi-error logic rectification. In Proceedings of Design Automation Conference, pages 146–151, 2011.

[5] Kai-Fu Tang, Po-Kai Huang, Chun-Nan Chou, and Chung-Yang Huang. Multi-patch generation for multi-error logic rectification by interpolation with cofactor reduction. In Proceedings of Design, Automation & Test in Europe, pages 1567–1572, 2012.

[6] Shao-Lun Huang, Wei-Hsun Lin, and Chung-Yang (Ric) Huang. Match and replace - a functional ECO engine for multi-error circuit rectification. In Proceedings of International Conference on Computer-Aided Design, pages 383–388, 2011.