[發明專利]驗證實現整數除法器的硬件設計的方法、系統和介質

有效

• 申請號: 201810029928.0
• 申請日: 2018-01-12
• 公開（公告）號: CN108334306B
• 公開（公告）日: 2023-07-14
• 發明（設計）人: E·莫里尼;S·艾利奧特
• 申請（專利權）人: 想象技術有限公司
• 主分類號: G06F7/535
• 分類號: G06F7/535
• 代理公司: 北京三友知識產權代理有限公司 11127
• 代理人: 呂俊剛;王青芝

1.一種驗證用于實現整數除法器的集成電路硬件設計的計算機實現方法，該整數除法器被配置成接收分子N和分母D并輸出商q和余數r，所述方法包括以下步驟：在一個或更多個處理器中：

驗證所述集成電路硬件設計的基本特性，其中，驗證基本特性的步驟驗證所述集成電路硬件設計的實例化將響應于非負輸入對的子集中的任何輸入對N、D生成正確輸出對q、r，其中，針對每個非負輸入對N、D，N≥0并且D＞0；

通過形式驗證工具在形式上驗證所述集成電路硬件設計的一個或更多個范圍縮減特性，其中，驗證一個或更多個范圍縮減特性的步驟驗證：如果所述集成電路硬件設計的實例化將響應于非負輸入對N、D生成輸出對q、r，則所述集成電路硬件設計的實例化將響應于另一非負輸入對N′、D生成與q和r具有預定關系的輸出對q′、r′，其中，N和N′具有一個或更多個預定關系中的一個；以及

輸出指示所述基本特性和所述一個或更多個范圍縮減特性是否已被成功驗證的信號，

其中，所述一個或更多個范圍縮減特性被配置為使得不在非負輸入對的所述子集中的每個非負輸入對經由所述一個或更多個預定關系中的一個或更多個的組合而與非負輸入對的所述子集中的至少一個非負輸入對相關。

2.根據權利要求1所述的方法，所述方法還包括以下步驟，響應于指示所述基本特性和所述一個或更多個范圍縮減中的至少一個特性沒有被成功驗證的所述信號，修改所述集成電路硬件設計。

3.根據權利要求1所述的方法，所述方法還包括以下步驟，響應于指示所述基本特性和所述一個或更多個范圍縮減特性被成功驗證的所述信號，在集成電路制造系統處制造根據所述集成電路硬件設計的集成電路。

4.根據權利要求1所述的方法，其中，N與N′之間的所述一個或更多個預定關系包括N′＝N＋D。

5.根據權利要求1所述的方法，其中，N與N′之間的所述一個或更多個預定關系包括N′＝N+1。

6.根據權利要求1所述的方法，其中，N與N′之間的所述一個或更多個預定關系包括N′＝2^zN、2^zN+1、2^zN+2、…、2^zN+(2^z-1)，其中，z是整數。

7.根據權利要求6所述的方法，其中，z等于一。

8.根據權利要求7所述的方法，其中，所述一個或更多個范圍縮減特性包括：

如果N′＝2N并且2r＜D，則r′＝2r并且q′＝2q；

如果N′＝2N并且2r≥D，則r′＝2r-D并且q′＝2q+1；

如果N′＝2N+1并且2r＜D，則r′＝2r+1并且q′＝2q；以及

如果N′＝2N+1并且2r≥D，則r′＝2r+1-D并且q′＝2q+1。

9.根據權利要求1所述的方法，其中，N與N′之間的所述一個或更多個預定關系包括N′＝αN、αN+1、αN+2、…、αN+(α-1)，其中，α是整數。

10.根據權利要求5至9中的任一項所述的方法，其中，非負輸入對的所述子集包括非負輸入對N、D，其中N＝0。

11.根據權利要求10所述的方法，其中，所述基本特性是，響應于非負輸入對的所述子集中的任何輸入對，每一個輸出對q、r都滿足q＝0并且r＝0。

12.根據權利要求1至9中的任一項所述的方法，其中，非負輸入對的所述子集包括非負輸入對N、D，其中N＜D。

13.根據權利要求12所述的方法，其中，所述基本特性是，響應于非負輸入對的所述子集中的任何輸入對，每一個輸出對q、r都滿足q＝0并且r＝N。