[發明專利]可控性檢驗系統及方法

無效

• 申請號: 201310746659.7
• 申請日: 2013-12-31
• 公開（公告）號: CN104142675A
• 公開（公告）日: 2014-11-12
• 發明（設計）人: 塔米爾·海曼;丹·史密斯;浩崙·梁;胡塞姆·阿布海梅德;約格什·馬哈詹
• 申請（專利權）人: 輝達公司
• 主分類號: G05B23/02
• 分類號: G05B23/02
• 代理公司: 北京市磐華律師事務所 11336
• 代理人: 董巍;謝栒

1.一種可控性檢驗方法，包括：

接收與所分析的控制部件的定義關聯的信息，所述信息包括定義該所分析的控制部件的方程；

基于所接收的信息，執行智能可控性檢驗過程，包括執行正式的可控性檢驗檢查是否可避免對控制信號輸入集的一些可能值的枚舉；以及

返回對該所分析控制部件的可控性分析結果的指示。

2.如權利要求1所述的可控性檢驗方法，其中智能可控性過程包括：

執行初始化過程，包括將可控性環境格式的值轉化為求解器環境格式的值；

執行改進的智能QBF求解；以及

返回該求解的結果。

3.如權利要求2所述的可控性檢驗方法，其中智能可控性過程包括：

在每個求解器環境格式值和相應的所分析控制部件的界面值之間建立映射；以及

維持該映射的列表。

4.如權利要求2所述的可控性檢驗方法，其中該QBF求解的結果包括三個可能值之一：

ABORT意味著該求解器運行時間超出最大時間限制；

UNSAT意味著該求解器發現沒有這樣的賦值；以及

SAT意味著求解器發現賦值。

5.如權利要求2所述的可控性檢驗方法，其中智能可控性檢驗過程尋找C集的賦值A，其具有以下特性：

將A應用于C導致定義所分析的控制部件的方程的輸出是與其他輸入值無關的目標值；以及

若存在這樣的值，則提供該值用于以上的A，否則，則證明這樣的A不存在。

6.如權利要求1所述的可控性檢驗方法，其中智能可控性過程包括：

執行第一可控性檢驗技術，其中該第一可控性檢驗技術具有預定的時間限制約束；以及

若第一可控性檢驗技術的結果無論如何無法得到信號是否提供或不提供可控性的結論，則執行第二可控性檢驗技術。

7.如權利要求1所述的可控性檢驗方法，其中該智能可控性過程包括該結果的驗證。

8.一種智能可控性檢驗系統，包括：

所分析的控制部件；

智能可控性檢驗部件，該部件可操作為對該所分析的控制部件執行智能可控性檢驗，包括執行正式的可控性檢驗，該檢驗檢查是否可避免對控制信號輸入集的一些可能值的枚舉。

9.如權利要求8所述的智能可控性檢驗系統，其中該所分析的控制部件包括于非常大的硬件設計。

10.如權利要求8所述的智能可控性檢驗系統，其中利用改進的智能QBF過程確立對控制信號輸入的智能枚舉的賦值。

11.如權利要求8所述的智能可控性檢驗系統，其中該智能可控性檢驗部件檢查，當應用于定義所分析的控制部件的方程時，對控制信號輸入的賦值是否產生具有與其它輸入的值無關的目標值的輸出。

12.如權利要求8所述的智能可控性檢驗系統，其中該智能可控性檢驗部件包括轉化部件，該部件可操作為在每個求解器環境格式值和相應的所分析的控制部件的界面值之間建立映射以及維持該映射的列表。

13.如權利要求8所述的智能可控性檢驗系統，其中該智能可控性檢驗部件包括可控性環境/QBF環境轉化部件，該部件可操作為在可控性檢驗兼容格式與改進的智能QBF兼容格式之間轉化。

14.如權利要求8所述的智能可控性檢驗系統，其中該智能可控性檢驗部件包括改進的智能QBF部件，該部件可操作為在執行高效的檢驗時智能地避免枚舉一些無關的可能賦值。

15.一種系統，其包括處理器和存儲器，該存儲器用于存儲指導該處理器執行可控性檢驗方法的指令，該方法包括：

接收與所分析的控制部件的定義關聯的信息，包括定義該所分析的控制部件的方程；

基于所接收的所述信息，執行智能可控性檢驗過程，包括執行正式的可控性檢驗，該檢驗檢查是否可避免對控制信號輸入集的一些可能值的枚舉；以及

返回對該所分析的控制部件的可控性分析結果的指示。

16.如權利要求15所述的可控性檢驗系統，其中智能可控性過程包括執行改進的智能QBF可控性檢驗；以及該改進的智能QBF可控性檢驗避免枚舉控制信號輸入集的一些可能值，X傳播可控性檢驗和常數傳播可控性檢驗不避免。