1 嵌入式軟體調試與驗證技術概述

1.1 調試和驗證過程的重要性

近年來，嵌入式系統（ES Embedded systems）因其靈活的操作和可能性而被廣泛應用於電子系統行業。嵌入式系統由硬體、軟體和其他模塊（如機械）組成，旨在作為更大系統的一部分執行特定任務。網路物理系統（CPS Cyber-Physical System）和物聯網（IoT Internet of Things）等重要的新概念也考慮到了嵌入式系統的不同方面。在CPS中，考慮到時間、能量和大小等物理量，計算和物理過程被整合在一起。在物聯網中，物理對象被無縫集成到信息網路中。綜上所述，車輛內部控制、自動駕駛儀、電信產品、電器、移動設備、機器人控制和醫療設備都是嵌入式系統的一些實際例子。

在過去幾年中，嵌入式電子產品中使用的軟體數量不斷增加，而且這種趨勢在未來仍將繼續。全球已開發的微處理器中幾乎有90%都已應用於嵌入式系統產品，因為嵌入式軟體（ESW）是功能創新的主要推動力，例如，在汽車領域，它可以減少氣體排放或提高安全性和舒適性。

嵌入式軟體還經常用於安全關鍵型應用（如汽車），在這些應用中，故障是不可接受的，這一點從因軟體錯誤而導致的災難和不便清單中可見一斑。驗證和調試過程的主要挑戰是如何處理系統的複雜性。

嵌入式軟體在現代SoC中以不同的視角進行應用，從分佈在多個處理器內核中的應用軟體（如應用程式、中間件、操作系統、驅動程式、固件），到依賴於硬體的軟體（即裸機），最後涵蓋通信軟體棧。

電子系統級（ESL）設計和驗證通常是自下而上和自上而下方法的結合。它通過硬體和軟體的並行設計，利用硬體和軟體的協同作用來實現系統級目標。因此，軟體開發需要與 SoC 設計、集成和驗證提前開始（並行）。在硅前階段，是清除系統環境中關鍵錯誤的時候。在這一階段，SW越來越多地成為一個需要解決的問題，因為如果錯誤過於嚴重，它可能會阻礙製造。生產完成後，可繼續在晶元上開發SW，併進行硅後驗證。

軟體開發、調試和驗證過程導致SoC項目成本高達整個開發成本的80%。設計複雜度越來越高，因此產生了設計生產力差距和驗證差距。目前，技術能力每36個月翻一番。在過去幾年中，通過在矽片中填充多核和記憶體組件，併在軟體中提供額外功能，硬體設計生產率得到了提高。隨著嵌入式軟體數量的增加，可以註意到軟體差距的存在，目前的主要挑戰是如何將數百萬門的軟體線與數百萬門的軟體線相匹配。目前，軟體部分每10個月翻一番，而依賴硬體的軟體的生產率每5年才翻一番。隨著設計複雜度的增加，對系統壽命和上市時間的要求也在不斷縮短。如果能最大限度地減少驗證和調試時間，開發周期就能縮短。如果由於設計錯誤而需要重新設計設備和/或增加新的項目開發周期，產品的最終成本可能會增加數十萬美元。此外，人們還普遍認為，在設備投放市場之前，必須糾正功能錯誤。硬體和軟體知識產權 (IP) 模塊的供應公司就是對正確性要求很高的企業，因為他們需要確保自己的IP核在插入目標項目時能正確工作。

本章介紹調試/驗證平臺和方法，並概述本書的範圍和組織結構。

1.2 調試和驗證平臺

調試和驗證平臺可以定義為電腦系統硬體的標準，決定了可以執行哪些類型的調試和驗證過程。基本上，我們可以將平臺分為兩類： 硅前平臺和硅後平臺。在硅前平臺中，設計調試和驗證是通過虛擬環境和複雜的模擬與形式驗證工具進行的。與之不同的是，在硅後平臺中，使用邏輯分析儀和基於斷言的工具在目標板上運行真實器件。

1.2.1 操作系統模擬

智能設備（如智能手機）的操作系統允許開發人員創建數以千計的附加程式，這些程式具有多種實用功能，如存儲用戶的個人數據。為了開發這些應用程式（即應用程式），每個平臺都有其優勢、劣勢和挑戰。
Gronli等人從軟體架構、應用程式開發、平臺能力和限制以及開發人員支持等幾個不同方面對主要的移動操作系統平臺進行了比較。比較的操作系統平臺包括：(1) 谷歌基於Linux的操作系統 Android；(2)微軟的 Windows Phone操作系統；(3) 蘋果的iOS平臺：(4) Mozilla新推出的基於網路的火狐操作系統。所有被評估的平臺都提供了從良好到卓越的互動式調試選項。

1.2.2 虛擬平臺

虛擬原型（VP Virtual prototyping）（又稱虛擬平臺）是一個系統的軟體模型，可用於早期軟體開發和 SoC/系統架構分析。虛擬原型包括處理器和外設模型，可以以實時或接近實時的速度運行，可能支持整個軟體堆棧直至應用級的硅前開發。虛擬原型驗證解決方案可能附帶幫助開發模型的工具，通常還提供模擬和調試環境。早期的虛擬原型驗證解決方案需要專有模型，而現在許多解決方案都使用基於開放系統級建模（OSCI）、事務級建模（TLM transaction-level modeling）標準和 IEEE-1666 SystemC 標準的 SystemC 模型。

除早期軟體開發外，虛擬原型還可用於軟體分發、系統開發套件和客戶演示。例如，在後RTL軟體開發中，虛擬原型可用作半導體公司向系統公司軟體開發人員分發的硅參考板的低成本替代品。與參考板相比，虛擬原型可提供更好的調試能力和迭代時間，因此可加快硅後系統集成過程。

1.2.3 RTL 模擬

依賴於硬體的軟體需要模擬器或目標平臺進行測試。寄存器傳輸級（RTL Register Transfer Level）模擬是驗證數字集成電路設計正確性最廣泛使用的方法。它們更適合測試具有硬體依賴性的軟體（如彙編代碼）和需要時序精度的軟體。然而，當模擬具有複雜內部行為的大型集成電路設計（如運行嵌入式軟體的 CPU 內核）時RTL模擬可能會非常耗時。由於RTL到佈局仍是最普遍的集成電路設計方法，因此必須加快RTL模擬過程。最近，圖形處理單元上的通用計算（GPGPU）正在成為加速計算密集型工作負載的一種有前途的模式。

1.2.4 加速/模擬

傳統調試工具跟不上系統級晶元 (SoC) /ASIC 設計規模和複雜性的快速增長。隨著RTL/柵極設計規模的增大，傳統模擬器的運行速度明顯減慢，從而延誤了硬體/軟體（系統）集成，延長了整個驗證周期。
當過長的模擬時間成為動態驗證的瓶頸時，通常會使用硬體模擬和模擬加速。硬體模擬器提供的調試環境具有邏輯模擬器的許多功能，在某些情況下甚至超過了邏輯模擬器的調試功能，如設置斷點和記憶體設計內容或符號的可見性。要在硬體模擬中使用基於斷言的驗證（ABV Assertion-based Verification）方法，必須在硬體中支持斷言。傳統的模擬器基於可重構邏輯和FPGA。為了提高靈活性並簡化調試過程（調試過程需要斷言處理能力），目前新一代的模擬器和模擬加速器通常基於處理元件陣列，如 Cadence Palladium 。另一種方法是在晶元內部集成調試和通信模塊，如用於調試的片上線上模擬（ICE in-circuit emulation）架構。然而，由於模擬器成本高昂，對許多開發人員來說都是昂貴的。

1.2.5 FPGA 原型開發

近年來，現成的商用 FPGA（COTS Commercial-Off-The-Shelf）可提供處理能力，滿足儀器解析度和測量速度不斷提高的要求，而且功耗低。此外，部分動態重新配置允許在運行過程中改變或調整有效載荷處理。
FPGA技術通常用於新數字設計的原型，然後再進入製造階段。雖然這些物理原型的運行速度比邏輯模擬器快很多個數量級，但其根本局限在於調試時缺乏片上可見性。有公司在原型中安裝了基於跟蹤緩衝器的儀器，允許設計人員在實時運行期間捕獲預定的信號數據視窗，進行離線分析。然而，設計人員無需在每次修改視窗時重新編譯整個電路，而是建議僅使用備用 FPGA路由多路復用器構建一個覆蓋網路，將所有電路信號連接到跟蹤儀器。因此，在調試過程中，設計人員只需重新配置該網路，而無需尋找新的佈局佈線方案。

1.2.6 原型開發板

傳統上，矽片後調試通常既痛苦又緩慢。矽片的可觀測性有限，而且成本高昂。模擬和模擬速度慢，而且很難解決邊角情況、併發和周期依賴行為。在模擬中，希望受限隨機發生器能命中導致故障場景（觸發錯誤）的輸入組合。此外，當複雜的硅後錯誤浮出水面時，上市時間也是一個主要問題，而找到問題的根本原因並加以修複需要時間。

硅後自省技術已成為解決日益嚴重的正確性、可靠性和良品率問題的有力工具。以前使用硅後自省技術的工作包括線上錯誤檢測、多處理器高速緩存一致性驗證和線上缺陷檢測。訪問控制擴展（ACE Access-Control Extensions）可以訪問和控制微處理器的內部狀態。利用ACE技術，特殊固件可在執行過程中定期探測微處理器，以定位運行時故障，修複設計錯誤。

1.2.7 為軟體開發和調試選擇合適的平臺

正如前文所述，沒有 "放之四海而皆準 "的方法。每個平臺都有其優勢和劣勢。

1.3 調試方法

調試可能是嵌入式系統開發人員最耗時的工作。對有效調試工具和基礎設施的任何投資都會加速產品的發佈。基本上，調試過程可以以互動式或後處理的形式進行。

表 1.1 軟體包類別與調試方法和平臺的關係

表 1.2 嵌入式軟體調試

1.3.1 互動式調試

剋服可觀察性問題的一種常用調試方法是互動式（或運行/停止）技術。這種技術的優勢在於，我們可以檢查SoC的全部狀態，而不會受到器件引腳速度的限制。此外，它只需要在SoC中增加少量調試邏輯。互動式調試的主要缺點是該技術具有侵入性，因為在觀察其狀態之前必須停止SoC。

最原始的調試方式是在標準輸出上列印信息（如 C 語言的 printf）和使用調試應用程式（如gdb）。如果在硬體引擎上測試嵌入式軟體，則應使用JTAG 2介面獲取調試信息。工業調試解決方案包括Synopsys System-Level Catalyst, 側重於虛擬平臺和FPGA原型調試；SVEN和OMAR側重於軟體和硬體技術，增加了硅和軟體調試設施。

1.3.2 後處理調試

後處理調試以批處理模式運行模擬，將數據記錄到波形資料庫，然後在模擬完成後分析結果。當DUT由基於類的驗證環境（如開放驗證方法（OVM Open Verification Methodology）或通用驗證方法（UVM Universal Verification Methodology））驅動時，後一種使用模式會給後處理結果帶來挑戰。

Incisive Debug Analyzer（IDA提供了互動式調試流程的功能以及在後處理模式下調試的優勢，允許所有調試數據文件運行一次模擬。

參考資料

• 軟體測試精品書籍文檔下載持續更新 https://github.com/china-testing/python-testing-examples 請點贊，謝謝！
• 本文涉及的python測試開發庫 謝謝點贊！ https://github.com/china-testing/python_cn_resouce
• python精品書籍下載 https://github.com/china-testing/python_cn_resouce/blob/main/python_good_books.md
• Linux精品書籍下載 https://www.cnblogs.com/testing-/p/17438558.html

1.4 驗證方法

1.4.1 驗證規劃

驗證規劃是一種定義如何測量變數、場景和功能的方法。此外，它還記錄瞭如何衡量驗證結果，例如模擬覆蓋率、定向測試和形式分析。它還提供了一個框架，用於達成共識和定義設計的驗證閉合。驗證規劃工具的一個例子是 Enterprise Planner，它可以創建、編輯和維護驗證計劃，既可以從頭開始，也可以通過鏈接和跟蹤功能規範來實現。

1.4.2 驗證環境開發

動態驗證需要在驗證過程中執行嵌入式系統。它主要側重於測試、共同驗證和基於斷言的驗證。另一方面，靜態驗證在不執行嵌入式系統的情況下對其進行驗證。靜態驗證的重點是靜態分析和模型檢查方法。定理證明要求用戶熟練迭代，主要與其他靜態驗證方法結合使用。最後，混合方法側重於靜態方法和動態-靜態方法的結合。

1.4.2.1 動態驗證

動態驗證側重於測試、共同驗證和基於斷言的驗證方法。獨立於硬體的軟體的動態驗證可直接在主機上測試。而依賴硬體的軟體則需要模擬器或目標平臺。如果嵌入式軟體要求高性能（如操作系統啟動、視頻處理應用），則可使用硬體引擎（如線上模擬器、模擬加速器或快速原型）來提高性能。動態驗證的主要優勢在於整個系統都可用於驗證，以便更深入地測試系統狀態空間。

• 測試

測試是一種經驗性方法，旨在執行軟體設計，以識別任何設計錯誤。如果嵌入式軟體不能正常工作，則應進行修改以使其正常工作。腳本語言用於編寫不同的測試場景（例如，具有不同參數值或不同函數調用序列的函數）。

• 指標驅動的硬體/軟體協同驗證

度量驅動驗證是指使用驗證計劃和覆蓋率度量來組織和管理驗證項目，並優化日常活動，以實現驗證閉合。設計測試平臺的目的是將輸入驅動到硬體/軟體模塊，並監控設計的內部狀態（白盒驗證）或輸出結果（黑盒驗證）。執行回歸套件會產生一個失敗運行列表，這些失敗運行通常代表系統中有待解決的錯誤，而覆蓋率則提供了驗證完成度的衡量標準。錯誤會被反覆修複，但度量驅動驗證的獨特過程是使用覆蓋率圖表和覆蓋率漏洞分析來幫助完成驗證。通過分析覆蓋漏洞，可以深入瞭解尚未生成的系統場景，使驗證團隊能夠對驗證環境進行調整，以實現更多的功能覆蓋。

例如，覆蓋率驅動驗證已成功應用於硬體領域的e語言。最近，它又通過 Incisive Software extensions (ISX) 擴展到了嵌入式軟體領域。

• 基於斷言的驗證

基於斷言的驗證方法以時間屬性捕捉設計的預期行為，併在系統模擬過程中監控這些屬性。在對系統需求進行規範後，非正式的規範被轉化為捕捉設計意圖的時態屬性。這種需求的形式化已經提高了對新系統的理解。這種方法已成功應用於較低層次的硬體設計，特別是寄存器傳輸層（RTL），它需要時鐘機製作為時序參考和布爾層信號。因此，將這種硬體驗證技術直接應用於嵌入式軟體並不合適，因為嵌入式軟體沒有時序參考，而且包含更複雜的結構（如整數、指針等）。因此，為了將基於斷言的方法應用於嵌入式軟體，需要使用新的機制。

1.4.2.2 靜態驗證

靜態驗證在不執行程式的情況下進行分析。分析在源代碼或目標代碼上進行。嵌入式軟體的靜態驗證主要側重於抽象靜態分析、模型檢查和定理證明。

靜態分析已廣泛應用於編譯器設計的優化（例如指針分析）。 在軟體驗證中，靜態分析已用於突出顯示可能的編碼錯誤（例如linting工具）或正式靜態分析，以驗證不變屬性，例如除零、數組邊界和類型轉換。這種方法還用於分析最壞情況執行時間 (WCET worst case execution time) 和堆棧/堆記憶體消耗。

形式靜態分析基於抽象解釋理論，它近似於程式執行的語義。這種近似是通過抽象函數（例如數值抽象或形狀分析）來實現的，抽象函數負責將實際值映射到抽象值。 該模型過度近似系統的行為，使其易於分析。 另一方面，它是不完整的，並非原始系統的所有真實屬性都對抽象模型有效。 然而，如果該屬性在抽象解釋中有效，則該屬性在原始系統中也有效。

• 模型檢查

模型檢查 (MC) 驗證設計模型是否滿足給定的規範。 模型檢查有兩種主要範例：顯式狀態模型檢查和符號模型檢查。
顯式狀態模型檢查使用顯式表示（例如哈希表）來存儲由狀態轉換函數給出的探索狀態。 另一方面，符號模型檢查以緊湊的形式象徵性地存儲探索的狀態。 儘管顯式模型檢查已用於軟體驗證（例如，SPIN模型檢查器），但與符號模型檢查器相比，它具有記憶體限制。 符號模型檢查基於二元決策圖（BDD）或布爾可滿足性（SAT）[31]，並且已應用於形式驗證過程中。 然而，每種方法都有其自身的優點和缺點。

形式化驗證可以處理中等規模的軟體系統，其中可供探索的狀態空間較小。 對於較大的軟體設計，使用模型檢查的形式驗證通常會遇到狀態空間爆炸問題。 因此，應用抽象技術來減輕後端模型檢查器的負擔。

常用的軟體模型檢驗方法有：

• 將C程式轉換為模型並將其輸入模型檢查器。

這種方法通過使用合適的抽象將程式的語義建模為有限狀態系統。 這些抽象模型使用基於BDD和基於SAT的模型檢查器進行驗證。

• 邊界模型檢查（BMC）

這種方法解除了嵌入式軟體中的迴圈，並將所得子句公式應用於基於 SAT 的模型檢查器。

當前模型檢查方法的主要弱點仍然是合適的抽象模型的建模和大型工業嵌入式軟體的狀態空間爆炸。

• 定理證明

定理證明是一種演繹驗證方法，它使用一組公理和一組推理規則來證明針對屬性的設計。 在過去的幾年裡，自動定理證明器（ATP）領域的研究一直是嵌入式軟體驗證的一個重要課題[27]。 然而，獨立的定理證明技術仍然需要熟練的人類指導才能構建證明。

1.4.2.3 混合驗證

驗證技術的組合是一種有趣的方法，以剋服上述孤立的動態和靜態驗證方法的缺點。
用於嵌入式軟體驗證的主要混合驗證方法側重於模型檢查和定理證明的結合，例如可滿足性模理論（SMT）和謂詞抽象方法。
SMT結合了以經典一階邏輯表達的理論（例如線性不等式理論、數組理論、列表結構理論、位向量理論），以確定公式是否可滿足。 公式中的謂詞符號可能有附加的解釋，這些解釋根據它們所屬的理論進行分類。 從這個意義上說，SMT的優點是問題不必轉換為布爾級別（如SAT求解），並且可以在字級別上處理。 例如，基於SMT的BMC已用於多線程軟體的驗證，通過從 SMT 求解器生成的不滿足性證明中抽象出狀態變數和交錯的數量來減少狀態空間。

使用定理證明器或SAT求解器進行謂詞抽象的模型檢查是基於"抽象-檢查-提煉"範式來檢查軟體的。它根據謂詞構建抽象模型，然後檢查安全屬性。如果檢查失敗，它就會完善模型並重覆整個過程。
動態驗證和靜態驗證的結合已在硬體驗證領域進行了探索。基本上，模擬用於達到"有趣"（也稱為燈塔或臨界）狀態。從這些狀態出發，模型檢查器可以在一定數量的時間步長內對局部狀態空間進行窮舉驗證。這種方法可用於硬體商業驗證工具，如。此外在硬體串列協議的驗證中，模擬和形式驗證的結合也被用於查找錯誤，而孤立的技術（即僅模擬或僅形式驗證）無法發現這些錯誤。

控制嵌入式軟體複雜性的一種方法是將形式化方法與模擬方法相結合。這種方法結合了深入系統和詳盡覆蓋嵌入式軟體系統狀態空間的優點。例如，基於斷言的驗證和基於最先進軟體模型檢查器的形式驗證相結合，並應用於使用C語言的嵌入式軟體驗證。

1.5 小結

本章介紹並討論了最先進的嵌入式軟體調試和驗證技術的主要優點和不足。