发明名称 |
Method and system for case-splitting on nodes in a symbolic simulation framework |
摘要 |
A method for performing verification includes receiving a design and building for the design an intermediate binary decision diagram set containing one or more nodes representing one or more variables. A first case-splitting is performed upon a first fattest variable from among the one or more variables represented by the one or more nodes by setting the first fattest variable to a primary value, and a first cofactoring is performed upon the intermediate binary decision diagram set with respect to the one or more nodes using an inverse of the primary value to generate a first cofactored binary decision diagram set. A second cofactoring is performed upon the intermediate binary decision diagram set with respect to the one or more nodes using the primary value to generate a second cofactored binary decision diagram set, and verification of the design is performed by evaluating a property of the second cofactored binary decision diagram set.
|
申请公布号 |
US7475371(B2) |
申请公布日期 |
2009.01.06 |
申请号 |
US20070963290 |
申请日期 |
2007.12.21 |
申请人 |
INTERNATIONAL BUSINESS MACHINES CORPORATION |
发明人 |
JACOBI CHRISTIAN;JANSSEN GEERT;PARUTHI VIRESH;WEBER KAI OLIVER |
分类号 |
G06F9/45;G06F17/50 |
主分类号 |
G06F9/45 |
代理机构 |
|
代理人 |
|
主权项 |
|
地址 |
|