透過模組化合約驗證基於COTS的電路圖｜國立清華大學博碩士論文庫

簡易檢索 / 詳目顯示

回結果列表

研究生：	賴冠勳 Lai, Kuan-Hsun
論文名稱：	透過模組化合約驗證基於COTS的電路圖 Validation of COTS-based Schematics at the Electrical Level by Modular Contracts
指導教授：	周百祥 Chou, Pai H.
口試委員:	韓永楷 Hon, Wing-Kai 謝孫源 Hsieh, Sun-Yuan 李皇辰 Lee, Huang-Chen
學位類別：	碩士 Master
系所名稱：	電機資訊學院 - 資訊工程學系 Computer Science
論文出版年：	2024
畢業學年度：	112
語文別：	英文
論文頁數：	64
中文關鍵詞：	嵌入式系統、電子設計自動化、基於元件設計、組態求解
外文關鍵詞：	Embedded system, Electronic Design Automation, Component-Based Architecture Design, Configuration Resolution
相關次數：	點閱：62 下載：0
分享至:	分享至facebook 分享至twitter

查詢本校圖書館目錄查詢臺灣博碩士論文知識加值系統勘誤回報

儘管商用現成 (COTS) 組件簡化了嵌入式系統的設計，但確保各種組件的兼容性和正確集成仍然充滿挑戰。現有的電子設計自動化 (EDA) 工具主要關注原理圖捕獲和佈局，而忽略了驗證互連組件兼容性的複雜任務。本論文提出了一種基於契約的介面驗證技術，用於基於 COTS 的嵌入式系統在電氣層級的驗證。它利用組件庫，根據從數據表和參考設計中提取的跨域知識對 COTS 組件進行建模。然後，它查詢各個組件的相關術語，包括假設和保證，並試圖建立一個契約，其中每個節點的假設可以由同一鏈接上的所有其他節點保證。我們的方法的一個新穎之處在於我們將每個變量與一個標籤集相關聯，以識別其角色。這使得我們的方法具有模塊化，因為它使算法能夠自動提取與契約相關的所有參數，而無需依賴於其他契約方法所假設的命名約定或手動製作。

如果可以建立契約，則證明最終的系統設計符合指定的要求並且可以在給定的假設下可靠地運行。如果沒有，那麼我們的工具可以識別契約失敗的原因。這可能是向人類設計師或由生成式 AI 創建的設計提供反饋的最重要功能。

我們通過一系列案例研究證明了我們提出的技術的有效性。我們展示了這項技術檢測和標記組件連接不一致、電壓兼容性問題和電源不足場景的能力。通過自動化這些檢查，我們的工具顯著減少了人為錯誤的可能性並提高了設計過程的效率。所提出的工具是 Sysmaker 的一部分，Sysmaker 是一個用於基於 COTS 的嵌入式系統的設計框架。通過將我們的契約方法推廣到其他抽象級別，我們期望 Sysmaker 最終能夠帶來更穩健可靠的嵌入式系統。

The design of embedded systems, while streamlined by commercial off-the-shelf (COTS) components, is fraught with challenges in ensuring the compatibility and correct integration of diverse components. Existing electronic design automation (EDA) tools primarily focus on schematic capture and layout, neglecting the intricate task of verifying the compatibility of interconnected components. This thesis proposes a contract-based interface verification technique at the electrical level for COTS-based embedded systems. It leverages a component library that models COTS components based on cross-domain knowledge extracted from datasheets and reference designs. It then queries the individual components for the relevant terms, including assumptions and guarantees, and attempts to establish a contract where the assumptions at each node can be guaranteed by all other nodes on the same link. One novelty with our approach is that we associate each variable with a tagset to identify its role. This makes our approach modular in the sense that it enables an algorithm to automatically extract all parameters relevant to a contract, without relying on naming conventions or manual crafting that other contract approaches assume.

If a contract can be established, then it is a proof that the final system design adheres to the specified requirements and can function reliably under the given assumptions. If not, then our tool can identify the reason where the contract fails to hold. This is perhaps the most important capability for providing feedback to either the human designer or to a design created by generative AI.

The effectiveness of our proposed technique is demonstrated through a series of case studies. We showcase its ability to detect and flag inconsistencies in component connections, voltage compatibility issues, and insufficient power supply scenarios. By automating these checks, our tool significantly reduces the potential for human error and enhances the efficiency of the design process. The proposed tool is a part of Sysmaker, a design framework for COTS-based embedded systems. By generalizing our contract appraoch to other levels of abstraction, we expect Sysmaker to ultimately lead to more robust and reliable embedded systems.

Contents i
Acknowledgments vii
Introduction 1
1 Motivation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1
1.1 Board-Level design . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1
1.2 Virtual Integration . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3
1.3 Sysmaker . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4
1.4 Consistency Checking . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4
2 Contributions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5
3 Thesis Outline . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5
Related Work 6
1 Board-level Design Tools . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6
1.1 Schematic Capture and Layout Tools . . . . . . . . . . . . . . . . . . . . . . 6
1.2 Inference-based Method . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7
1.3 Deduction-based Method . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
1.4 Turning Coders into Makers: The Promise of Embedded Design Generation . 11
2 Contract-based Approach . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
2.1 SysML . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
2.2 CoDeL . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
Methodology 14
1 Sysmaker . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14
2 Preliminaries . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14
2.1 Block Graph . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
2.2 Component Library . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
2.3 Implementation Block . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
3 Design Flow . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16
3.1 Specification Authoring . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16
3.2 Candidate Selection . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
3.3 Consistency Checking . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
3.4 Resource Allocation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
3.5 Simulation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
Technical Approach 19
1 Problem Formulation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19
2 Relation to the feature model . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
3 Validation Algorithm . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
3.1 Port-Slot Allocation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
3.2 Initial Compatibility Assessment . . . . . . . . . . . . . . . . . . . . . . . . 33
3.3 Detailed Integration Planning . . . . . . . . . . . . . . . . . . . . . . . . . 36
3.4 Final Validation Protocol . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
Implementations 39
1 System Architecture . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
2 Component and Arbiter Library . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
3 Visualization tool . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
4 Solver . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
Case Study 44
1 Component modeling . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
2 System Assembly . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
2.1 Case 1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
2.2 Case 2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
2.3 Case 3 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
3 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
Conclusions and Future Work 53
1 Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
2 Future Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
Appendix 58
                                

[Aut24] Autodesk Inc. Autodesk Fusion 360. https://www.autodesk.com/products/fusion-360/overview, 2024. Version used: 2024.
[BBB+16] Jonathan Bachrach, David Biancolin, Austin Buchan, Duncan W. Haldane, and Richard Lin. JITPCB. In 2016 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), pages 2230–2236, 2016.
[Des24] Embedded Systems Design. KiCad electrical rules check (ERC). https://embedded-systems-design.github.io/kicad-electrical-rules-check, 2024. Accessed:2024-07-13.
[dMB08] Leonardo de Moura and Nikolaj Bjørner. Z3: An efficient SMT solver. In C. R. Ramakr-ishnan and Jakob Rehof, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 337–340, Berlin, Heidelberg, 2008. Springer Berlin Heidelberg.
[FCY+22] Morteza Fayazi, Zachary Colter, Zineb Benameur-El Youbi, Javad Bagherzadeh, TutuAjayi, and Ronald Dreslinski. FASCINET: A fully automated single-board computer gen-erator using neural networks. IEEE Transactions on Computer-Aided Design of IntegratedCircuits and Systems, 41(12):5435–5448, 2022.
[GMK15] Marco Gario, Andrea Micheli, and Bruno Kessler. PySMT : a solver-agnostic library for fast prototyping of SMT-based algorithms. In Proceedings of the 2015 International Conference on SMT Solving, 2015.
[Inc24] Autodesk Inc. Autodesk eagle: PCB design and electrical schematic software. https://www.autodesk.com/products/eagle/overview, 2024. Accessed: 2024-07-13.
[KiC24] KiCad. KiCad: A cross platform and open source electronics design automation suite. https://kicad.org/, 2024. Accessed: 2024-07-13.
[LHK+19] Jo-Yu Lo, Da-Yuan Huang, Tzu-Sheng Kuo, Chen-Kuo Sun, Jun Gong, Teddy Seyed, Xing-Dong Yang, and Bing-Yu Chen. AutoFritz: Autocomplete for prototyping virtual breadboard circuits. In Proceedings of the 2019 CHI Conference on Human Factors in Computing Systems, CHI ’19, page 1–13, New York, NY, USA, 2019. Association for Computing Machinery.
[Lin23] Hao-Yu Lin. Ontology-based modeling for efficient component selection in design automation of embedded systems. Master’s thesis, National Tsing Hua University, 2023.
[LLC24] Altium LLC. Altium designer: PCB design software. https://www.altium.com/altium-designer, 2024. Accessed: 2024-07-13.
[LRC+20] Richard Lin, Rohit Ramesh, Connie Chi, Nikhil Jain, Ryan Nuqui, Prabal Dutta, and Björn Hartmann. Polymorphic blocks: Unifying high-level specification and low-level control for circuit board design. In Proceedings of the 33rd Annual ACM Symposium on User Interface Software and Technology, UIST ’20, page 529–540, New York, NY, USA, 2020. Association for Computing Machinery.
[OMG12] OMG. OMG Systems Modeling Language (OMG SysML), Version 1.3. http://www.omg.org/spec/SysML/1.3, 2012. sysml.
[PG15] Steffen Peter and Tony Givargis. Component-based synthesis of embedded systems using satisfiability modulo theories. ACM Trans. Des. Autom. Electron. Syst., 20(4), sep 2015.
[RLI+17] Rohit Ramesh, Richard Lin, Antonio Iannopollo, Alberto Sangiovanni-Vincentelli, Björn Hartmann, and Prabal Dutta. Turning coders into makers: the promise of embedded design generation. In Proceedings of the 1st Annual ACM Symposium on Computational Fabrication, SCF ’17, New York, NY, USA, 2017. Association for Computing Machinery.
[Tex13] Texas Instruments. CC2541 SimpleLink™ Bluetooth® low energy and proprietary wireless MCU datasheet, June 2013. Available at https://www.ti.com/lit/ds/symlink/cc2541.pdf, Rev. D.
[TGT+17] Robert Todd, Laurence Grodd, Jimmy Tomblin, Katherine Fetty, and Daniel Liddell. Design rule checking. In Electronic Design Automation for IC Implementation, Circuit Design, and Process Technology, pages 525–540. CRC Press, 2017.
[Tho23] Stephen Thornton. Karl Popper. In Edward N. Zalta and Uri Nodelman, editors, The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University, Winter 2023 edition, 2023.
[Wal] Cory Walker. EDASolver. https://edasolver.com/.
[ZFS05] Xuan F. Zha, Steven J. Fenves, and Ram D. Sriram. A Feature-Based Approach to Em-bedded System Hardware and Software Co-Design. In ASME 2005 International Design Engineering Technical Conferences and Computers and Information in Engineering, volume Volume 3: 25th Computers and Information in Engineering Conference, Parts A and B of International Design Engineering Technical Conferences and Computers and Information in Engineering Conference, pages 609–620, 09 2005.

簡易檢索 / 詳目顯示

相關論文