[發明專利]驗證用于多級部件的硬件設計

在審

• 申請號: 202011538039.0
• 申請日: 2020-12-23
• 公開（公告）號: CN113051865A
• 公開（公告）日: 2021-06-29
• 發明（設計）人: 羅伯特·麥凱美
• 申請（專利權）人: 暢想科技有限公司
• 主分類號: G06F30/398
• 分類號: G06F30/398;G06F115/02
• 代理公司: 北京東方億思知識產權代理有限責任公司 11258
• 代理人: 郭妍

1.一種用于驗證用于多級部件的硬件設計的方法(300)，所述多級部件被配置為接收輸入數據并且通過在多個連續階段中的每個階段處理所述輸入數據來生成輸出數據，每個階段能夠在每個周期中被啟用或停止，所述方法(300)包括在一個或多個處理器處：

針對從第二階段到最后一個階段的多個階段中的每個階段：

驗證第一屬性，所述第一屬性為如果當在一個周期中所述階段由任何一組輸入啟用并且在后續周期中由第一最小輸入序列啟用任何后續階段時實例化處于相同狀態，則所述硬件設計的所述實例化的所述輸出數據的相關部分相同(304)；以及

驗證第二屬性，所述第二屬性為如果實例化在以下情況下處于相同狀態，則所述硬件設計的所述實例化的所述輸出數據的所述相關部分相同：(i)當在一個周期中所述階段被啟用并且在后續周期中由第二最小輸入序列啟用任何后續階段時，以及(ii)當所述階段停止，然后在下一個周期中所述階段被啟用，并且在后續周期中由所述第二最小輸入序列啟用所述后續階段時(306)。

2.如權利要求1所述的方法(300)，其中在以下約束下針對階段驗證所述第二屬性：當所述階段在周期中停止時，在所述階段之前的階段也停止。

3.如權利要求1所述的方法(300)，其中所述輸出數據的所述相關部分為所有的所述輸出數據，或者其中所述輸出數據的所述相關部分基于對所述多級部件的所述輸入和/或所述多級部件的操作模式。

4.如權利要求1至3中任一項所述的方法(300)，還包括通過驗證當所述階段由最小輸入序列啟用時所述硬件設計的實例化的所述輸出數據對于相同的輸入數據相同而與所述硬件設計的初始狀態無關，驗證所述硬件設計與初始狀態無關。

5.如權利要求1至3中任一項所述的方法(300)，其中對于所述多級部件的每個可能的有效狀態，針對階段驗證所述第一屬性。

6.如權利要求1至3中任一項所述的方法(300)，其中對于所述多級部件的其中階段被啟用的每一組可能的輸入，針對所述階段驗證第一屬性。

7.如權利要求1至3中任一項所述的方法(300)，其中對于僅一個最小輸入序列，針對階段驗證所述第一屬性和所述第二屬性中的至少一者。

8.如權利要求1至3中任一項所述的方法(300)，其中對于所述多級部件的每個可能的有效狀態，針對階段驗證所述第二屬性。

9.如權利要求1至3中任一項所述的方法(300)，其中對于所述多級部件的其中階段停止的每一組可能的輸入，針對所述階段驗證第二屬性。

10.如權利要求1至3中任一項所述的方法(300)，其中用于所述后續階段的最小輸入序列是使相同輸入前進經過所述后續階段的每個階段的輸入序列。

11.如權利要求1至3中任一項所述的方法(300)，其中所述第一最小輸入序列和/或第二最小輸入序列包括其中在連續周期中啟用所述后續階段的輸入序列。

12.如權利要求1至3中任一項所述的方法(300)，還包括輸出指示所述驗證是否成功的一個或多個信號(308)。

13.如權利要求1至3中任一項所述的方法(300)，還包括響應于確定所述驗證中的至少一個驗證不成功(310)，修改所述硬件設計(312)。

14.如權利要求13所述的方法(300)，還包括重新驗證所述修改后的硬件設計。

15.如權利要求1至3中任一項所述的方法(300)，其中使用形式驗證工具來形式驗證所述第一屬性和所述第二屬性中的至少一者。