[發明專利]一種基于SVA形式化驗證的FPGA軟件仿真測試環境建立方法

有效

• 申請號: 202210845602.1
• 申請日: 2022-07-19
• 公開（公告）號: CN115098400B
• 公開（公告）日: 2022-12-06
• 發明（設計）人: 路云峰;賈楊;周建云;王世海;劉斌
• 申請（專利權）人: 北京航空航天大學
• 主分類號: G06F11/36
• 分類號: G06F11/36;G06F21/57
• 代理公司: 北京慕達星云知識產權代理事務所(特殊普通合伙) 11465
• 代理人: 符繼超

本發明公開了一種基于SVA形式化驗證的FPGA軟件仿真測試環境建立方法，該方法包括：依據被測對象FPGA軟件的測試需求，結合SVA并發斷言模板和DUT信號分析工具，產生適用于對被測對象開展形式化驗證的Bind模板；導入Bind庫中；在所述Bind庫中選取要執行的Bind，生成實例化模板并將實例化模板插入并發斷言監控的代碼文件module之外；調用形式化驗證工具讀入源代碼并調用Bind庫，實現基于SVA的形式化驗證。該方法將斷言與設計代碼實現分離，不會對斷言編寫及驗證產生限制，在采用形式化驗證提升驗證效率的同時，增強代碼與并發斷言的可管理性，既滿足驗證目標，又使得驗證問題可追溯。

技術領域

本發明屬于可編程邏輯器件軟件仿真測試技術領域，特別涉及一種基于SVA形式化驗證的FPGA軟件仿真測試環境建立方法。

背景技術

近年來，可編程邏輯器件軟件在航空、航天、船舶、武器裝備等產品中的應用與日俱增，可編程邏輯器件軟件產品的功能復雜度越來越高，可編程邏輯器件軟件驗證工作時間超過可編程邏輯器件軟件開發周期一半。可編程邏輯器件軟件產品升級周期也日益縮短，傳統的基于testbench模擬電路輸入的測試方式需要編寫大量測試代碼，用于模擬電路運行狀態，這種方式需要消耗大量的人力成本和時間成本，且難以達到百分百測試覆蓋。因此，近年來形式化驗證在可編程邏輯器件軟件測試領域逐漸得到重視。同時傳統的基于斷言的驗證方法需要在被測邏輯的代碼文件中植入大量斷言語句，驗證過程將產生大量冗余代碼。斷言也并沒有進行分類保存，不利于斷言管理。當驗證工作結束，刪除冗余代碼后，又不利于問題追溯和技術沉淀。

因此，針對傳統基于斷言的驗證方法中存在大量冗余代碼、且不利于管理的問題，本領域技術人員亟需解決。

發明內容

本發明的主要目的在于提供一種基于SVA形式化驗證的FPGA軟件仿真測試環境建立方法，該方法可解決傳統基于斷言的驗證方法中存在大量冗余代碼、且不利于管理的問題，可實現可編程邏輯器件軟件驗證時將被測邏輯代碼與SystemVerilog并發斷言分離到不同文件，進而實現基于SVA的形式化驗證仿真。

為實現上述目的，本發明采取的技術方案為：

本發明實施例提供一種基于SVA形式化驗證的FPGA軟件仿真測試環境建立方法，包括以下步驟：

S1、依據被測對象FPGA軟件的測試需求，結合SVA并發斷言模板和DUT信號分析工具，產生適用于對被測對象開展形式化驗證的Bind模板；

S2、將所述Bind模板文件導入Bind庫中；所述Bind庫依據模板標識按照測試類型對Bind模板進行分組；

S3、在所述Bind庫中選取要執行的Bind，生成實例化模板并將實例化模板插入并發斷言監控的代碼文件module之外；

S4、調用形式化驗證工具讀入源代碼并調用Bind庫，實現基于SVA的形式化驗證。

進一步地，所述S1步驟還包括：

根據測試需求，將Bind模板的測試類型分為功能測試、性能測試、邊界測試、時序測試、接口測試以及安全性測試；

對不同類型的Bind模板插入不同類型的Bind標識，并通過DUT信號分析工具掃描出Verilog/VHDL源碼文件中的管腳、寄存器或線網信號，選取需要使用并發斷言監控的信號，以input類型端口定義在Bind模板中。

進一步地，所述S2步驟中所述Bind庫還預留斷言違例組和回歸測試組；每一個Bind組包含若干Bind文件和Bind組日志文件，Bind文件通過實例化與被測對象連接，封裝在其中的并發斷言在形式化驗證工具中生效并執行驗證工作；其中，Bind組日志文件記錄本組信息，包含Bind文件數量、Bind標識以及各Bind中的并發斷言數量。

進一步地，該方法還包括：