[發明專利]一種基于顯示控制系統的形式化驗證方法在審
| 申請號： | 202011399429.4 | 申請日： | 2020-12-05 |
| 公開（公告）號： | CN112579439A | 公開（公告）日： | 2021-03-30 |
| 發明（設計）人： | 馬城城;秦翔;劉暉;田珍;蘇東閣;王晨光 | 申請（專利權）人： | 西安翔騰微電子科技有限公司 |
| 主分類號： | G06F11/36 | 分類號： | G06F11/36 |
| 代理公司： | 西安匠成知識產權代理事務所(普通合伙) 61255 | 代理人： | 商宇科 |
| 地址： | 710054 陜西省西*** | 國省代碼： | 陜西;61 |
| 權利要求書： | 查看更多 | 說明書： | 查看更多 |
| 摘要： | |||
| 搜索關鍵詞： | 一種 基于 顯示 控制系統 形式化 驗證 方法 | ||
1.一種基于顯示控制系統的形式化驗證方法，其特征在于：該方法包括以下步驟：
1)接口劃分：對顯示控制系統的所有接口按照輸入、處理通路、輸出三部分對接口進行劃分，生成輸入模塊接口列表、處理通路模塊接口列表；
2)參數配置：
2.1)根據硬件提供的能力，確定合法參數的范圍，超過該范圍的為非法參數；
2.2)按照各個接口的輸入參數檢查情況，選取合法參數的范圍和非法參數范圍內的相對應的典型參數；
3)接口及參數組合：
3.1)將步驟2.2)中所列的每個接口的典型參數逐次配置到相應接口中，生成多種參數配置情況；
3.2)再依次對輸入模塊、處理通路模塊、輸出模塊內的各接口參數的多種配置進行接口間的排列組合，以覆蓋各模塊中所有功能不同參數的組合；
4)有效性篩選。
2.根據權利要求1所述的基于顯示控制系統的形式化驗證方法，其特征在于：所述步驟1)中所述輸入模塊接口列表包括顯示控制系統輸入配置相關的接口，所述處理通路模塊接口列表包括顯示控制系統處理通路配置相關的接口，所述輸出模塊接口列表包括顯示控制系統輸出配置相關的接口。
3.根據權利要求2所述的基于顯示控制系統的形式化驗證方法，其特征在于：所述步驟3.2)中的具體步驟如下：
3.2.1)從輸入模塊、處理通路模塊中各選一種配置情況進行組合，直至兩個子模塊中每一種配置均已被選擇，且不能有剩余；
3.2.2)從處理通路模塊、輸出模塊中各選一種配置情況進行組合，直至兩個模塊中每一種配置均已被選擇，且不能有剩余。
4.根據權利要求3所述的基于顯示控制系統的形式化驗證方法，其特征在于：所述有效性篩選包括等價性配置篩選、錯誤配置篩選。
5.根據權利要求4所述的基于顯示控制系統的形式化驗證方法，其特征在于：所述等價性配置篩選是篩選出等價性配置組合，將配置效果等價的組合中的配置保留一個，其他剔除。
6.根據權利要求4所述的基于顯示控制系統的形式化驗證方法，其特征在于：所述錯誤配置篩選是篩選出不符合硬件設計規則的錯誤配置組合，并將其剔除。
該專利技術資料僅供研究查看技術是否侵權等信息，商用須獲得專利權人授權。該專利全部權利屬于西安翔騰微電子科技有限公司，未經西安翔騰微電子科技有限公司許可，擅自商用是侵權行為。如果您想購買此專利、獲得商業授權和技術合作，請聯系【客服】
本文鏈接：http://www.szxzyx.cn/pat/books/202011399429.4/1.html，轉載請聲明來源鉆瓜專利網。
