1、核心翻譯步驟示例

本節我們以第2節提到的Lustre語言的主要特性為線索來解釋L2C在翻譯過程中的關鍵節點是如何處理的, 并以圖 1的實例來解釋Lustre程序是如何被一步步地翻譯到Clight語言的.

1.1 數據流并發性

Lustre程序具有數據流并發性, 而Clight程序卻是串行執行的.因此, 翻譯過程中的一大難題就是要將Lustre語句串行化.現在一般采用的因果分析和排序大多采用測試或翻譯確認的方法, 未進行形式化驗證.對于L2C構建經過形式化證明的可信編譯器的目標, 對排序做嚴格證明是必要的.我們首先定義Lustre*中的因果關系.支持國產處理器仿真的全數字實時仿真平臺SkyEye與可信編譯器L2C的核心翻譯步驟

(1) 如果一個等式A的左值出現在等式B的右值中, 則說等式B依賴于等式A.

(2) 如果一個節點A的左值出現在等式B的時鐘中, 則說等式B依賴于等式B.

然后, 我們定義拓撲排序的性質, 并且定義拓撲排序等價性定理, 即任意兩個滿足拓撲排序性質的程序在串行執行語義中是等價的, 以此來保證串行化方案的正確性.最后利用Coq實現拓撲排序算法, 將并行的LustreS串行化, 并以此算法完成之前定義的拓撲排序性質和語義等價性證明.

實際翻譯效果以圖 1中的第7行~第8行為例, 按照第1條因果關系的定義,?圖 1中第8行的左值出現在了第7行的右值中, 所以第7行語句依賴于第8行.圖 4顯示了拓撲排序后LustreS程序中與圖 1第7行~第8行對應的代碼片段, 在排序后,?圖 1的第7行被翻譯為圖 4中的第4行,?圖 1中的第8行被對應到圖 4中的第2行, 可見排序后的語句滿足因果關系的定義.

1.2 高階算子

Lustre提供了10多個高階算子 (涵蓋了LustreV6支持的所有高階算子), 包括map, red等.圖 1第10行使用了map算子, 本節以map為例來介紹高階算子消去.Lustre中map算子的形式為map《op; size》(a1,?a2, …,?an), 其中,?a1~an是n個輸入數組, size為數組的大小; 而op為一個操作, 可以是運算符或一個節點, 擁有n個輸入參數.map算子運算的結果為一個數組, 記為res, 其中, res[i]=op (a1[i],?a2[i], …,?an[i]).圖 1中的p值展示了圖 1第10行map算子運算的結果, 可見高階算子簡化了對數組的循環操作.

由于目標語言Clight不支持高階運算, 所以在翻譯過程中, 需要消去Lustre*中的高階算子.基于高階算子對數組處理的特點, 我們最終在LustreS到LustreR1階段將所支持的各個高階算子按其語義特性展開為Clight支持的語法結構, 主體為for循環結構.

圖 5展示了圖 1中第10行的map運算在LustreS這一層的中間表示, 可見, 在LustreS這一層L2C不會對map高階算子做翻譯.

經過LustreRGen過程, L2C會將map高階表達式轉換成for循環, 如圖 6所示.

通過設計翻譯算法將LustreS中的高階復雜運算分解成LustreR1中多個基礎運算的循環, 我們消除了Lustre*程序中的所有高階算子.

1.3 時態和時鐘算子

Lustre支持如LustreV6的一些可以操作流數據的時態算子, 如fby, 以及操作變量時鐘的時鐘算子, 如when算子.在Lustre程序中, 每個變量均有自己的時鐘, 默認情況下為一個全局基本時鐘, 該時鐘在每個時鐘周期都為True.如圖 2中擁有全局基本時鐘的x3, 在每個時鐘周期都有值.而Lustre提供的when算子則可以用來改變某個變量的時鐘, 如圖 2中的y1,?b為True的周期有值且與x3當前周期值相同, 但b為False的周期的值則是未定義.再如Lustre提供的fby算子, 可以用來訪問流數據的歷史值, 它不改變時鐘, 返回值相當于向右shift流數據的值, 如圖 2中的s, 它的值在y1上整體向右shift了一位, 并且在shift產生的空缺值中補上了fby函數指定的默認值5.支持國產處理器仿真的全數字實時仿真平臺SkyEye與可信編譯器L2C的核心翻譯步驟

L2C在LustreS到LustreR1階段會處理所有時鐘算子, 在LustreR3到LustreF1階段會處理所有的時態算子.以fby算子為例, 在LustreF1中,?圖 1中Stay節點內的第27行和第28行, fby算子會被最終翻譯成如圖 7所示的LustreF1代碼, 其中a為Stay節點的輸入參數.

L2C引入acg_init變量來標識當前周期是否為第1個周期, 如果是第1個周期, 那么將對變量m和n賦初值, 賦初值時會根據fby指定的周期數來初始化存儲m和n的數組大小, 并在數組中對每個值賦予fby指定的默認值, 然后在之后的周期依次循環遍歷數組的值, 并在每次讀取值之后在數組當前位置記錄變量在fby之前當前周期的值.以圖 2的輸入值為例, 我們將圖 7中n對應的fby相關參數acg_fby2前4個周期的變化過程展示出來, 如圖 8所示, 便于更好地理解圖 7的翻譯結果.

1.4 翻譯至Clight

經過前面幾個核心步驟后, 已經消除了Lustre中最顯著的同步數據流特征, 程序已經十分接近常規的串行命令式語言.又經過后續若干個關鍵步驟 (包含初始化函數生成ResetfunGen) 到LustreC, 已經十分接近Clight, 經由最后兩個步驟實現與CompCert完全對接 (如圖 3所示).從LustreC到Clight的翻譯過程中, 在語法上幾乎沒有太大的變化, 但在語義環境上差異較大, 證明工作繁重.圖 9展示了L2C翻譯圖 1所示Lustre程序中Main節點的最終結果, 具體翻譯驗證的難點我們將在下一節詳細描述.

1.5 流數據對象

如圖 1所示, 主節點Main的輸入和輸出都是無窮長的流數據, 簡單來說, 每個時鐘周期, Lustre*程序以輸入流數據當前時鐘周期的值傳入Main節點作為輸入, 執行得到輸出流中當前時鐘周期的值.

由于程序獲取輸入和處理輸出的方式不盡相同, 所以L2C只會翻譯Lustre*程序中的節點, 并不會給最終的Clight程序中加入C語言的入口函數Main函數.在實際使用中, 如圖 10所示, 我們會編寫C語言的main函數循環調用調用生成Main函數, 以此來處理流數據.

高性能嵌入式仿真軟件SkyEye

隨著科技的發展，系統工程的設計體量逐漸龐大起來，尤其是對于軌道交通、航空航天、核電站等安全關鍵領域中，如何在復雜度逐年變大的同時保證其安全性和可靠性，是近年來各大公司需要研究的課題。最近比較火熱的基于模型的系統工程（MBSE）技術則給大家提供了一種全新的技術方向，分享一種全數字實時仿真的安全關鍵領域解決方案，提供一種新的解決思路。支持國產處理器仿真的全數字實時仿真平臺SkyEye與可信編譯器L2C的核心翻譯步驟，提供高效的運算速度，提高研發效率和安全性。

新一代全數字仿真平臺SkyEye

基于模型的全數字研發解決方案MBSE工具軟件SkyEye是能夠滿足模擬或仿真外部硬件行為進行軟件運行和測試需求的工具。該工具運用國際流行的仿真、測試腳本語言來編寫外部硬件邏輯行為所產生外部激勵事件以構成嵌入式軟件的外部信號激勵或數據輸入，從而滿足軟件在全數字仿真運行環境下無須人的干預而閉環運行的要求。支持國產處理器仿真的全數字實時仿真平臺SkyEye與可信編譯器L2C的核心翻譯步驟

作為基于嵌入式應用的特點，嵌入式軟件全數字仿真測試支撐平臺SkyEye要為嵌入式系統提供全數字仿真測試環境或測試平臺，實現對嵌入式系統進行實時、閉環的系統測試。在該平臺上完成被測軟件的分析、運行和測試，最重要的是要實現嵌入式系統外部事件的全數字仿真平臺，使得嵌入式軟件就像在真實硬件環境下連續不中斷地運行。

---

本文標題：支持國產處理器仿真的全數字實時仿真平臺SkyEye與可信編譯器L2C的核心翻譯步驟

本文鏈接：http://www.digiproto.com

總結

以上是生活随笔為你收集整理的支持国产处理器仿真的全数字实时仿真平台SkyEye与可信编译器L2C的核心翻译步骤的全部內容，希望文章能夠幫你解決所遇到的問題。

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