[發明專利]一種基于顯示控制系統的形式化驗證方法

在審

• 申請號: 202011399429.4
• 申請日: 2020-12-05
• 公開（公告）號: CN112579439A
• 公開（公告）日: 2021-03-30
• 發明（設計）人: 馬城城;秦翔;劉暉;田珍;蘇東閣;王晨光
• 申請（專利權）人: 西安翔騰微電子科技有限公司
• 主分類號: G06F11/36
• 分類號: G06F11/36
• 代理公司: 西安匠成知識產權代理事務所(普通合伙) 61255
• 代理人: 商宇科

本發明涉及一種基于顯示控制系統的形式化驗證方法。本發明包括以下步驟：1)接口劃分：對顯示控制系統的所有接口按照輸入、處理通路、輸出三部分對接口進行劃分，生成輸入模塊接口列表、處理通路模塊接口列表、輸出模塊接口列表；2)參數配置：2.1)根據硬件提供的能力，確定合法參數的范圍，超過該范圍的為非法參數；2.2)按照各個接口的輸入參數檢查情況，選取合法參數的范圍和非法參數范圍內的相對應的典型參數；3)接口及參數組合：3.1)將步驟2.2)中所列的每個接口的典型參數逐次配置到相應接口中，生成多種參數配置情況；3.2)再依次對輸入模塊、處理通路模塊、輸出模塊內的各接口參數的多種配置進行接口間的排列組合，以覆蓋各模塊中所有功能不同參數的組合；4)有效性篩選。本發明具有準確、簡便、快捷的優點，提高了顯示控制模塊的驗證效率。

技術領域

本發明屬于計算機顯示控制領域，尤其涉及一種基于顯示控制系統的形式化驗證方法。

背景技術

顯示控制模塊是人機交互的重要橋梁之一，其功能復雜、配置多變，因此在對其進行驗證時，需要設計大量的驗證項，測試其功能的正確性。雖然顯示控制模塊經過多年發展，其驗證方法已經較為全面和簡便，但驗證項的設計及生成依舊需要花費大量的人力和時間，且出錯率較高，嚴重影響了顯示控制模塊的測試進度，目前在已公開資料中未發現有較為簡便快捷的驗證項生成方法。

發明內容

本發明為解決背景技術中存在的上述問題，而提供一種基于顯示控制系統的形式化驗證方法，該方法具有準確、簡便、快捷的優點，提高了顯示控制模塊的驗證效率。

本發明的技術解決方案是：本發明為一種基于顯示控制系統的形式化驗證方法，其特殊之處在于：該方法包括以下步驟：

1)接口劃分：對顯示控制系統的所有接口按照輸入、處理通路、輸出三部分對接口進行劃分，生成輸入模塊接口列表、處理通路模塊接口列表、輸出模塊接口列表；

2)參數配置：

2.1)根據硬件提供的能力，確定合法參數的范圍，超過該范圍的為非法參數；

2.2)按照各個接口的輸入參數檢查情況，選取合法參數的范圍和非法參數范圍內的相對應的典型參數；

3)接口及參數組合：

3.1)將步驟2.2)中所列的每個接口的典型參數逐次配置到相應接口中，生成多種參數配置情況；

3.2)再依次對輸入模塊、處理通路模塊、輸出模塊內的各接口參數的多種配置進行接口間的排列組合，以覆蓋各模塊中所有功能不同參數的組合；

4)有效性篩選。

優選的，步驟1)中輸入模塊接口列表包括顯示控制系統輸入配置相關的接口，處理通路模塊接口列表包括顯示控制系統處理通路配置相關的接口，輸出模塊接口列表包括顯示控制系統輸出配置相關的接口。

優選的，步驟3.2)中的具體步驟如下：

3.2.1)從輸入模塊、處理通路模塊中各選一種配置情況進行組合，直至兩個子模塊中每一種配置均已被選擇，且不能有剩余；

3.2.2)從處理通路模塊、輸出模塊中各選一種配置情況進行組合，直至兩個模塊中每一種配置均已被選擇，且不能有剩余。

優選的，有效性篩選包括等價性配置篩選、錯誤配置篩選。

優選的，等價性配置篩選是篩選出等價性配置組合，將配置效果等價的組合中的配置保留一個，其他剔除。

優選的，錯誤配置篩選是篩選出不符合硬件設計規則的錯誤配置組合，并將其剔除。