[發(fā)明專利]一種基于SVA形式化驗(yàn)證的FPGA軟件仿真測(cè)試環(huán)境建立方法

有效

• 申請(qǐng)?zhí)枺?/td>: 202210845602.1
• 申請(qǐng)日: 2022-07-19
• 公開(kāi)（公告）號(hào): CN115098400B
• 公開(kāi)（公告）日: 2022-12-06
• 發(fā)明（設(shè)計(jì)）人: 路云峰;賈楊;周建云;王世海;劉斌
• 申請(qǐng)（專利權(quán)）人: 北京航空航天大學(xué)
• 主分類號(hào): G06F11/36
• 分類號(hào): G06F11/36;G06F21/57
• 代理公司: 北京慕達(dá)星云知識(shí)產(chǎn)權(quán)代理事務(wù)所(特殊普通合伙) 11465
• 代理人: 符繼超

1.一種基于SVA形式化驗(yàn)證的FPGA軟件仿真測(cè)試環(huán)境建立方法，其特征在于，包括以下步驟：

S1、依據(jù)被測(cè)對(duì)象FPGA軟件的測(cè)試需求，結(jié)合SVA并發(fā)斷言模板和DUT信號(hào)分析工具，產(chǎn)生適用于對(duì)被測(cè)對(duì)象開(kāi)展形式化驗(yàn)證的Bind模板；

S2、將所述Bind模板文件導(dǎo)入Bind庫(kù)中；所述Bind庫(kù)依據(jù)模板標(biāo)識(shí)按照測(cè)試類型對(duì)Bind模板進(jìn)行分組；

S3、在所述Bind庫(kù)中選取要執(zhí)行的Bind，生成實(shí)例化模板并將實(shí)例化模板插入并發(fā)斷言監(jiān)控的代碼文件module之外；

S4、調(diào)用形式化驗(yàn)證工具讀入源代碼并調(diào)用Bind庫(kù)，實(shí)現(xiàn)基于SVA的形式化驗(yàn)證。

2.根據(jù)權(quán)利要求1所述的一種基于SVA形式化驗(yàn)證的FPGA軟件仿真測(cè)試環(huán)境建立方法，其特征在于，所述S1步驟還包括：

根據(jù)測(cè)試需求，將Bind模板的測(cè)試類型分為功能測(cè)試、性能測(cè)試、邊界測(cè)試、時(shí)序測(cè)試、接口測(cè)試以及安全性測(cè)試；

對(duì)不同類型的Bind模板插入不同類型的Bind標(biāo)識(shí)，并通過(guò)DUT信號(hào)分析工具掃描出Verilog/VHDL源碼文件中的管腳、寄存器或線網(wǎng)信號(hào)，選取需要使用并發(fā)斷言監(jiān)控的信號(hào)，以input類型端口定義在Bind模板中。

3.根據(jù)權(quán)利要求2所述的一種基于SVA形式化驗(yàn)證的FPGA軟件仿真測(cè)

試環(huán)境建立方法，其特征在于，所述S2步驟中所述Bind庫(kù)還預(yù)留斷言違例組和回歸測(cè)試組；每一個(gè)Bind組包含若干Bind文件和Bind組日志文件，Bind文件通過(guò)實(shí)例化與被測(cè)對(duì)象連接，封裝在其中的并發(fā)斷言在形式化驗(yàn)證工具中生效并執(zhí)行驗(yàn)證工作；其中，Bind組日志文件記錄本組信息，包含Bind文件數(shù)量、Bind標(biāo)識(shí)以及各Bind中的并發(fā)斷言數(shù)量。

4.根據(jù)權(quán)利要求3所述的一種基于SVA形式化驗(yàn)證的FPGA軟件仿真測(cè)試環(huán)境建立方法，其特征在于，該方法還包括：

S5、將被測(cè)對(duì)象和Bind庫(kù)聯(lián)合執(zhí)行形式化驗(yàn)證之后，產(chǎn)生形式化驗(yàn)證結(jié)

果；若發(fā)現(xiàn)違例斷言，則將違例斷言所在的Bind文件移到Bind庫(kù)下斷言違例組；當(dāng)執(zhí)行回歸測(cè)試后，則存放于Bind庫(kù)下的回歸測(cè)試組。

5.根據(jù)權(quán)利要求1所述的一種基于SVA形式化驗(yàn)證的FPGA軟件仿真測(cè)

試環(huán)境建立方法，其特征在于，所述S1步驟中并發(fā)斷言模板構(gòu)建方式如下：

1）從并發(fā)斷言屬性模板庫(kù)中選擇合適的屬性框架模板；所述屬性框架模板類型包括：時(shí)序型、條件型、約束型、脈寬型和自定義屬性；

2）基于屬性框架模板，設(shè)置其敏感信號(hào)、觸發(fā)時(shí)鐘以及參數(shù)指標(biāo)；

3）設(shè)置完成后封裝于Bind模板中。

6.根據(jù)權(quán)利要求1所述的一種基于SVA形式化驗(yàn)證的FPGA軟件仿真測(cè)試環(huán)境建立方法，其特征在于，所述S1步驟中DUT信號(hào)分析工具需要具備如下功能：

1）讀取Verilog、VHDL以及SystemVerilog文件；

2）自動(dòng)識(shí)別RTL代碼中的輸入輸出端口、寄存器變量、線網(wǎng)變量；

3）將識(shí)別到的端口、信號(hào)以及變量輸出成文本。

7.根據(jù)權(quán)利要求1所述的一種基于SVA形式化驗(yàn)證的FPGA軟件仿真測(cè)試環(huán)境建立方法，其特征在于，所述步驟S4中形式化驗(yàn)證工具，具備如下功能：

1）兼容IEEE SystemVerilog標(biāo)準(zhǔn)；

2）支持硬件描述語(yǔ)言Verilog、VHDL編譯；

3）支持基于給定的屬性，靜態(tài)地分析設(shè)計(jì)的行為；

4）支持探索電路所有可能的輸入序列；

5）發(fā)現(xiàn)電路行為與屬性不一致時(shí)，產(chǎn)生錯(cuò)誤分析報(bào)告，并生成違例案例。