[發明專利]用于生成形式驗證環境的方法、電子設備及存儲介質

有效

• 申請號: 202110995708.5
• 申請日: 2021-08-27
• 公開（公告）號: CN113947050B
• 公開（公告）日: 2022-09-02
• 發明（設計）人: 高世超;陳明科
• 申請（專利權）人: 芯華章科技股份有限公司
• 主分類號: G06F30/367
• 分類號: G06F30/367
• 代理公司: 北京風雅頌專利代理有限公司 11403
• 代理人: 王剛

1.一種用于生成形式驗證環境的方法，其中，所述方法包括：

接收用于描述邏輯系統設計的功能的配置文件，其中，所述配置文件指示所述邏輯系統設計的設計類型以及與所述設計類型對應的參數；

根據所述配置文件確定與所述邏輯系統設計對應的數據庫文件；

在所述數據庫文件中獲取與所述邏輯系統設計對應的多個形式驗證環境參數；以及

根據所述形式驗證環境參數生成形式驗證環境，其中，

所述數據庫文件包括信號說明列表，并且根據所述配置文件確定與所述邏輯系統設計對應的數據庫文件進一步包括：

根據所述配置文件獲取所述邏輯系統設計的輸入信號；

在所述信號說明列表中檢測所述輸入信號的匹配信號；以及

響應于在所述信號說明列表中檢測到所述輸入信號的匹配信號，唯一綁定所述輸入信號和所述匹配信號；

在所述數據庫文件中獲取與所述邏輯系統設計對應的多個形式驗證環境參數進一步包括：根據所述配置文件按修改優先級對所述多個形式驗證環境參數進行排序，以生成配置參數修改表；

所述形式驗證環境包括行為模型和斷言語句，所述形式驗證環境參數包括所述邏輯系統設計的驗證規則，并且根據所述形式驗證環境參數生成形式驗證環境進一步包括：

根據所述配置文件確定所述邏輯系統設計的設計類型；

根據所述設計類型配置所述行為模型；以及

根據所述配置參數修改表選擇所述邏輯系統設計的驗證規則以

生成所述斷言語句；

所述形式驗證環境還包括：約束語句和反饋延遲，并且所述根據所述形式驗證環境參數生成形式驗證環境進一步包括：

根據所述配置文件確定驗證請求；

定義所述驗證請求的行為以生成所述約束語句；以及

確定所述驗證請求被響應的所述反饋延遲。

2.如權利要求1所述的方法，其中，所述設計類型包括調度程序類型、流量管理器類型、內存控制器類型或狀態機模塊類型。

3.如權利要求1所述的方法，其中，所述設計類型是所述調度程序類型中的仲裁器，并且所述根據所述設計類型配置所述行為模型進一步包括：

獲取所述仲裁器的配置參數；以及

將所述仲裁器的配置參數賦予所述行為模型。

4.如權利要求1所述的方法，其中，所述方法進一步包括：

加載與所述數據庫文件對應的數據庫模型；以及

連接待測設備的接口和所述數據庫模型的接口。

5.一種電子設備，包括存儲器、處理器及存儲在存儲器上并可在處理器上運行的計算機程序，所述處理器執行所述程序時實現如權利要求1至4任意一項所述的方法。

6.一種非暫態計算機可讀存儲介質，所述非暫態計算機可讀存儲介質存儲電子裝置的一組指令，該組指令用于使所述電子裝置執行權利要求1至4任一項所述的方法。