全數字實時仿真平臺

SkyEye，中文全稱天目全數字實時仿真軟件，應用軟件仿真技術，逼真地模擬出被測軟件的物理環境。用圖形化方式構建虛擬目標系統，有效降低了硬件工程師和軟件工程師之間的溝通成本，軟件工程師可以不依賴硬件工程師，根據需求對虛擬硬件的配置進行改動，并可以在虛擬硬件模型上運行與真實硬件相同的二進制文件，可以大大縮短產品研發周期，提高軟件測試效率。完全自主可控的支持數十種國產芯片仿真的全數字實時仿真平臺SkyEye

SkyEye功能

更靈活快速的虛擬目標系統搭建–通過可視化圖形界面拖拽虛擬硬件組件快速搭建

仿真狀態可控性、確定性和重復性–在虛擬系統上運行的二進制文件與實際目標上運行的二進制文件相同，仿真過程可以通過運行、暫停控制、可以隨時重復執行，每次運行結果是確定的，可以使用軟件復現問題

提供GDB源碼調試和匯編級調試工具，使開發者更高效的分析和定位問題

提供代碼覆蓋率和生成報告功能，進行源碼和目標碼的覆蓋率分析

提供故障注入功能，可以進行內存和IO的故障注入進行測試

提供協同仿真工具，支持與其他異構模型協同仿真

提供外設建模工具和二次開發API接口，方便用戶進行二次開發

提供Python API接口，可以進行自動化測試腳本構建所需測試環境

界面提供自動化測試功能，可以選擇所需測試用例自動運行并給出測試結果

同步數據流語義

在從Lustre到C的轉換過程中, 經歷了同步數據流語義逐步向串行命令式語義的過渡.在現階段, Vélus的動態語義的形式化定義是從SN-Lustre中間表示開始的, 在Obc, 中間表示被變換至一種基于對象的串行命令式語義; 相應地, L2C的動態語義形式化定義是從LustreS中間表示開始的, 在LustreC, 中間表示徹底變換為一種類C的串行命令式語義.這些中間層語言所處位置, 如圖 1和圖 2所示.

可以看出, Vélus的同步數據流語義消去僅在一個階段完成, 而L2C則經歷了多個階段逐步消去.由于L2C的源語言特征相比Vélus要復雜很多, 實踐過程決定了跨多層的語義過渡是必然的選擇.

Vélus在定義SN-Lustre語義時已完成排序(scheduling), 因此無需考慮同步數據流語言的數據流并發特性.L2C是在LustreS層進行排序(toposort), 在LustreS層有串行語義定義(節點內部的所有等式相互之間存在全序關系), 同時也定義有超粗粒度的并發語義(以等式為粒度, 等式操作是不可分割的原子操作, 等式之間存在由數據依賴所確定的偏序關系).

Vélus和L2C的同步數據流語義都選擇了基于操作語義來定義(雖然也存在看似很不錯的基于指稱語義的基礎工作).在Lustre語言的原始論文中, 作者給出了Lustre語言的基本操作語義規則.Vélus和L2C的操作語義定義首先要與學界公認的這些工作相符, 同時也應考慮實現的因素(交互式定理證明的方便性).比如, 采用Coinductive來定義流看似是非常自然的(因為要處理的是infinite對象), 然而無論是Vélus還是L2C均放棄選擇這種方法, L2C團隊當初遇到的問題主要是因為采用Coq實現整體任務需求的技術難度無法預測.

在Vélus和L2C的同步數據流語義中, 對于流數據對象的基本理解是一致的, 均將其看作是從自然數到取值論域的函數.比如, 可以將一個流s在第n個周期的值記為s(n).然而, 在具體實現上, L2C采取了一些不同的措施.特別是針對同步數據流語義中最具代表性的fby算子.

在定義fby算子的語義時, Vélus使用了一個輔助算子hold, 會將所處理的流數據對象在上一個激活周期的取值保持到其后續的無效周期, 這樣, 若當前周期是激活周期, 則fby運算的結果就相當于當前周期hold運算的結果.這一思想在L2C項目開展的初期用來實現一種時鐘歸一化(clock unifying)算法, 其中定義了類似于hold的算子, 并用來刻畫fby算子的語義.然而, 在后來的工作中, L2C擯棄了這種做法.主要原因是, 這種方法僅適合于定義二元fby算子, 而難以推廣到實際應用中很有用的三元fby算子.L2C對二元和三元fby算子的語義定義采用了一致的框架, 定義一個大小為n的循環緩沖區, 并設法限定僅在激活周期可訪問緩沖區, 這里, n即為三元fby算子的第3個參數(對于二元fby算子, n=1).

定義同步數據流語義的另一個重要方面, 就是語義環境中要保留子環境的狀態, 這些子環境對應于當前環境下調用其他節點而形成的實例環境.保存這些子環境的原因是因為存在時態變量(見第4.2節), 需要保存歷史狀態, 這就導致了在調用的節點實例返回時不能像傳統的函數調用那樣釋放掉變量的存儲空間.因而, 我們必須要定義并維護一個樹狀的語義環境, 這對語義定義以及相應的證明來說, 難度增加了許多, 但這是我們必須要應對的.L2C在定義語義時對是否是時態變量進行了區分, 以方便對應到Clight的語義環境中.Vélus在文獻中對這種樹狀語義環境也有許多描述, 但僅從論文無法了解其進一步的實現詳情.

另外, L2C因支持高階迭代算子以及更多的數組和結構體算子, 使語義定義的難度增大許多, 但相關細節不屬本文所要討論的范圍.L2C的多階段翻譯架構(如圖 2所示)正是為了適應各種各樣的語義復雜度以及與Clight語義之間的巨大差異, 同樣, 圖 2所示的許多翻譯步驟也不在本文所討論的議題之內.

翻譯正確性驗證

在形式化定義動態語義階段, Vélus和L2C的各階段翻譯正確性的驗證目標與CompCert所建議的階段翻譯正確性目標從形式上是一致的, 都是要證明一種從高層到低層單向的語義模擬等價關系.這種模擬等價關系之所以可以是單向的, 是由于每一層語言均具有確定的語義(deterministic semantics).

對于同步數據流語義來說, 這種單向的語義模擬等價關系可大致描述為:任意數據流程序G的每個節點f, 若可以將輸入流xs映射到輸出流ys, 則對于翻譯后得到的程序G’中與f對應的節點或函數f '以及這一層次中相應于G’的初始化函數reset, 如果G’在其第1個激活周期先執行reset后執行f ', 而在其他后續激活周期中都重復執行f ', 那么同樣可以將xs映射到輸出流ys.注意:這一命題中的G、f、xs和ys都是任意的.

雖然各階段要證明的單向語義模擬等價關系形式上看都是相似的, 但具體到不同階段, 其含義卻都有所不同.首先, 各個階段的語法和語義互不相同; 其次, 每個階段可能有或沒有語法層面的reset函數, 如果有的話, 不同階段的reset函數也可能有所不同; 以及還有其他各種不同, 這里不再贅述.

一般來說, 從Lustre源程序到Clight程序的各階段翻譯過程中, 同步數據流語言的語法及語義特征逐漸被消去, C語言語法及語義特征逐漸增加.在定義上述單向語義模擬等價關系時, 所消失的語義特征描述通常會由新增加的語法特征來彌補.比如前面提到的reset特征, 在較高的語言層次, 語法層面并沒有對應的函數, 所以是在語義定義中體現其行為, 而在靠后的語言層次(比如圖 2所示的LustreE2層)已有語法層面的reset函數, 就不會也不可能通過語義定義來體現reset行為.

因Vélus和L2C的編譯框架之間差異較大(如圖 1和圖 2所示), 可以想象到二者在翻譯正確性驗證方面存在較大的差異.這種差異體現在各個方面.這里僅列舉一例.如果考慮第4.1節~第4.3節提到的核心翻譯步驟, 在Vélus中僅由Translation一個階段完成(如圖 1所示), 而在L2C中則是分散到從LustreR1到LustreD的許多階段實現的(如圖 2所示).一般來說, 一個翻譯階段所負責的工作越多, 其正確性證明的難度也越大, 重用性也越差.然而, 另一方面, 翻譯階段也不能太多, 否則會導致語言層次增加太多, 反而加重維護的負擔.因此, 應根據源語言的規模合理設計翻譯階段的數量.

Vélus中SN-Lustre之前的階段未定義動態語義, 這些階段所保持的特性主要是靜態方面的.多數這些階段, 甚至從SN-Lustre到Obc的過程(Translation), 基本上是繼承前人(Bertails、Biernacki和Auger等人)的工作.Bourke等人的論文對這些靜態語義相關階段的介紹很少, 同時, Vélus未開源, 所以具體繼承情況的詳情未能很好地得到了解, 從Biernacki和Auger等人的論文僅可了解到其中的一些.

Vélus的語法分析器是Bourke等人重新寫的, 它基于Jourdan等人提出的對LR(1)自動機進行確認并對確認程序進行驗證的方法, 因此可以認為是一個經過形式化驗證的語法分析器.L2C中, 最近剛完成與此平行的工作, 并以編譯選項的方式集成到了開源L2C編譯器中.

對于Vélus中的類型、時鐘檢查(elaboration)以及接下來的規范化過程(normalization), 僅了解Bertails、Biernacki和Auger等人在Coq中實現了這些過程以及進行了驗證, 但他們的論文中未提到是如何進行驗證的.L2C中與此對應的過程(LustreWGen、LustreVGen和LustreSGen)的驗證在目前的開源版本中尚未發布, 相關工作仍在完善和整理之中.這些翻譯過程在Vélus和L2C編譯框架中所處位置, 如圖 1和圖 2所示, 下同.

Vélus對于排序過程(Scheduling)的驗證是基于翻譯確認的方法 具體實現在相關論文中未加介紹.L2C中的排序過程(Toposort)是經過嚴格形式化驗證的, 證明了經過排序后的LustreS程序的串行語義行為, 與排序前LustreS程序的等式粒度并發語義所刻畫的行為是兼容的.從實現角度來看, 對排序過程的形式化驗證要比翻譯確認的工作量大很多, 所以從通常的觀點來看, 是否有必要這樣做是值得商榷的.但L2C的這項工作, 對于在項目開展初期積累團隊成員在使用Coq進行編程和驗證的經驗以及檢查LustreS操作語義定義的合理性等方面起著重要的作用.

總結

以上是生活随笔為你收集整理的全数字实时仿真平台SkyEye和同步数据流语义与翻译正确性验证的全部內容，希望文章能夠幫你解決所遇到的問題。

如果覺得生活随笔網站內容還不錯，歡迎將生活随笔推薦給好友。