執行於含錯處理器程式之修復編譯器

A QBF-Based Recompiler for Code Generation on Erroneous Processors and Beyond

蔡秉翰(Ping-Han Tsai)

指導教授 ： 江介宏

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

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

摘要

隨著現今電路設計的複雜性不斷提升，電路驗證成為一門越來越具挑戰性的工作。即便經過正規驗證，在晶片上發現製造階段所出現的錯誤也並非罕見。對於處理器類的設計，那些製造階段的錯誤是有機會用軟體指令補丁合成法來修正的。雖然之前的研究證明了這方法的可行性，但所生成的指令卻必須使用過多的遲滯指令，導致含錯處理器的效率被大幅降低。所以在這篇論文中我們提出了一個以量化布林函式為基礎的方法將原先要執行的組合語言再編譯為適用於含錯處理器的指令且避免了多餘的遲滯指令。實驗結果也證明了我們提出的方法的有效性。

關鍵字

修復編譯器 ； MIPS架構 ； 量化布林函數求解 ； Skolem函數 ； 控制器錯誤

並列摘要

With the increasing complexity of designs, verification becomes more and more challenging. Even with formal verification techniques deployed, post-silicon bugs are not uncommon to be found in manufactured chips. For processor designs, post-silicon bugs may possibly be avoided by exploiting software workaround. Although prior work has shown the feasibility, excessive stall operations have to be inserted in the generated assembly code and thus drastically slowing down software execution on a buggy processor. Given a program to be executed on a target buggy processor, in this thesis we propose a QBF-based method to recompile the program into assembly code executable on the buggy processor without triggering bugs while avoiding redundant stall operations. Experimental results show the effectiveness of our proposed method.

並列關鍵字

recompiler ； MIPS ； QBF solving ； Skolem function ； control-bug

參考文獻

[5] V. Balabanov and J.-H. R. Jiang. Unified QBF Certification and its Applications. Formal Methods in System Design, 41(1): 45-65, Aug. 2012

[6] G.S. Tseitin. On The Complexity of Derivation in Propositional Calculus. Studies in Constructive Mathematics and Mathematical Logic, pages 466-483, 1983

[7] L. Hellerman. A Catalog of Three-variable Or-inverter and And-inverter Logical Circuits. IEEE Transaction on Electronic Computers., pages 198-223 (Vol. EC-12), Jun. 1963

[8] D. A. Patterson and J. L. Hennessy. Computer Organization and Design: The Hardware/Software Interface, 2008.

[9] T.-P. Liu, S.-R. Lin, and J.-H. R. Jiang. Software Workarounds for Hardware Errors: An Approach to Compiler Patch Synthesis. IEEE Transaction on Computer-Aided Design of Integrated Circuits and Systems, 32(12):1992-2003, Dec. 2013.