专利快速检索-快速检索全球专利，免费商用专利数据库-IPRDB

1. 发明授权

US09189581B2 Equivalence checking between two or more circuit designs that include division circuits 有权
标题翻译：包含分割电路的两个或多个电路设计之间的等效性检查
公开(公告)号：US09189581B2
公开(公告)日：2015-11-17
申请号：US13665827
申请日：2012-10-31
申请人： Synopsys, Inc.
发明人： Himanshu Jain , Carl P. Pixley
IPC分类号： G06F17/50 , G06F11/00 , G06F7/02 , G06F9/455
CPC分类号： G06F17/5081 , G06F7/4873 , G06F7/4876 , G06F7/5525 , G06F9/3001 , G06F9/455 , G06F17/50 , G06F17/504
摘要： Methods and apparatuses are described for proving equivalence between two or more circuit designs that include one or more division circuits and/or one or more square-root circuits. Some embodiments analyze the circuit designs to determine an input relationship between the inputs of two division (or square-root) circuits. Next, the embodiments determine an output relationship between the outputs of two division (or square-root) circuits based on the input relationship. The embodiments then prove equivalence between the circuit designs by using the input and output relationships.
摘要翻译：描述了用于证明包括一个或多个分割电路和/或一个或多个平方根电路的两个或更多个电路设计之间的等效性的方法和装置。一些实施例分析电路设计以确定两个分割（或平方根）电路的输入之间的输入关系。接下来，实施例基于输入关系确定两个分割（或平方根）电路的输出之间的输出关系。然后，实施例通过使用输入和输出关系来证明电路设计之间的等同性。

2. 发明授权

US09501597B2 Elimination of illegal states within equivalence checking 有权
标题翻译：在等值检查中消除非法国家
公开(公告)号：US09501597B2
公开(公告)日：2016-11-22
申请号：US14329494
申请日：2014-07-11
申请人： Synopsys, Inc.
发明人： Himanshu Jain , Carl Preston Pixley
IPC分类号： G06F9/455 , G06F17/50
CPC分类号： G06F17/5045 , G06F17/504 , G06F17/5081
摘要： A method for equivalence checking includes obtaining a first and a second representation for a semiconductor design and applying a set of inputs to both representations. The outputs of the first representation are compared to the outputs of the second representation. If a mismatch is found, the starting states for the first and second representations are evaluated using a model checker to see if they are reachable from a known legal state such as reset state for that representation. If both of the starting states are reachable, the mismatch is a real mismatch providing a counter-example of the equivalence of the two representations. If one or both of the starting states are unreachable, the mismatch is a spurious mismatch and the model checker can be used to generate an invariant to preclude those starting states in future iterations of the equivalence checker.
摘要翻译：一种用于等效性检查的方法包括获得用于半导体设计的第一和第二表示以及将一组输入应用于两个表示。将第一表示的输出与第二表示的输出进行比较。如果发现不匹配，则使用模型检查器来评估第一和第二表示的起始状态，以查看它们是否可以从已知的合法状态（例如该表示的复位状态）到达。如果两个起始状态都可达到，则不匹配是提供两个表示的等价性的反例的实际失配。如果一个或两个起始状态是不可达的，则不匹配是虚假失配，并且可以使用模型检验器来生成不变量以排除等同检查器的将来迭代中的那些起始状态。

3. 发明申请

US20160012167A1 ELIMINATION OF ILLEGAL STATES WITHIN EQUIVALENCE CHECKING 有权
标题翻译：在等效检查中消除非法国家
公开(公告)号：US20160012167A1
公开(公告)日：2016-01-14
申请号：US14329494
申请日：2014-07-11
申请人： Synopsys, Inc.
发明人： Himanshu Jain , Carl Preston Pixley
IPC分类号： G06F17/50
CPC分类号： G06F17/5045 , G06F17/504 , G06F17/5081
摘要： A method for equivalence checking includes obtaining a first and a second representation for a semiconductor design and applying a set of inputs to both representations. The outputs of the first representation are compared to the outputs of the second representation. If a mismatch is found, the starting states for the first and second representations are evaluated using a model checker to see if they are reachable from a known legal state such as reset state for that representation. If both of the starting states are reachable, the mismatch is a real mismatch providing a counter-example of the equivalence of the two representations. If one or both of the starting states are unreachable, the mismatch is a spurious mismatch and the model checker can be used to generate an invariant to preclude those starting states in future iterations of the equivalence checker.
摘要翻译：一种用于等效性检查的方法包括获得用于半导体设计的第一和第二表示以及将一组输入应用于两个表示。将第一表示的输出与第二表示的输出进行比较。如果发现不匹配，则使用模型检查器来评估第一和第二表示的起始状态，以查看它们是否可以从已知的合法状态（例如该表示的复位状态）到达。如果两个起始状态都可达到，则不匹配是提供两个表示的等价性的反例的实际失配。如果一个或两个起始状态是不可达的，则不匹配是虚假失配，并且可以使用模型检验器来生成不变量以排除等同检查器的将来迭代中的那些起始状态。

4. 发明授权

US10503853B1 Formal verification using cached search path information to verify previously proved/disproved properties 有权
公开(公告)号：US10503853B1
公开(公告)日：2019-12-10
申请号：US16048063
申请日：2018-07-27
申请人： Synopsys, Inc.
发明人： Arunava Saha , Himanshu Jain , Manish Pandey , Ashvin Dsouza , Per Mattias Bjesse
IPC分类号： G06F9/455 , G06F17/50
CPC分类号： G06F17/504 , G06F17/5045
摘要： A formal verification tool that verifies multiple sequentially-generated versions of a core circuit design by obtaining search path information from the formal verification solver for each property that is proven or disproven during a first formal verification session involving an earlier-generated circuit design version, and utilizing the search path information to perform search-path verification processes during a subsequent formal verification session to quickly verify the proven/disproven properties in a later-generated circuit design version. Each property's search path information includes counterexample traces or proof artifacts identifying the search operations utilized to achieve a corresponding counterexample or proof object that proves/disproves the property. Search-path verification involves applying the stored search path information to the later-generated circuit design version, and determining if the same counterexample or proof object is achieved. The stored search path information is also utilized to perform efficient path-influenced search processes when the search-path verification process fails.

5. 发明申请

US20150213167A1 INVARIANT SHARING TO SPEED UP FORMAL VERIFICATION 审中-公开
标题翻译：不可分割的共享加速形式验证
公开(公告)号：US20150213167A1
公开(公告)日：2015-07-30
申请号：US14167716
申请日：2014-01-29
申请人： Synopsys, Inc.
发明人： Himanshu Jain , Per M. Bjesse , Carl P. Pixley
IPC分类号： G06F17/50
CPC分类号： G06F17/5081 , G06F2217/12 , Y02P90/265
摘要： Methods and apparatuses are described for sharing inductive invariants while performing formal verification of a circuit design. Specifically, some embodiments assume at least an inductive invariant for a property to be true while proving another property. According to one definition, an inductive invariant of a property is an inductive assertion such that all states that satisfy the inductive assertion also satisfy the property. According to one definition, an inductive assertion describes a set of states that includes all legal initial states of the circuit design and that is closed under a transition relation that models the circuit design.
摘要翻译：描述了在执行电路设计的形式验证时共享感应不变量的方法和装置。具体来说，一些实施例假定属性的至少一个归纳不变量是真实的，同时证明另一属性。根据一个定义，属性的感性不变性是归纳断言，使得满足感性断言的所有状态也满足该属性。根据一个定义，电感断言描述了一组状态，其包括电路设计的所有合法初始状态，并且在对电路设计进行建模的过渡关系下闭合。

6. 发明授权

US10325054B2 Invariant sharing to speed up formal verification 有权
公开(公告)号：US10325054B2
公开(公告)日：2019-06-18
申请号：US14167716
申请日：2014-01-29
申请人： Synopsys, Inc.
发明人： Himanshu Jain , Per M. Bjesse , Carl P. Pixley
IPC分类号： G06F17/50
摘要： Methods and apparatuses are described for sharing inductive invariants while performing formal verification of a circuit design. Specifically, some embodiments assume at least an inductive invariant for a property to be true while proving another property. According to one definition, an inductive invariant of a property is an inductive assertion such that all states that satisfy the inductive assertion also satisfy the property. According to one definition, an inductive assertion describes a set of states that includes all legal initial states of the circuit design and that is closed under a transition relation that models the circuit design.

7. 发明授权

US09870442B2 Equivalence checking between two or more circuit designs that include square root circuits 有权
公开(公告)号：US09870442B2
公开(公告)日：2018-01-16
申请号：US14860549
申请日：2015-09-21
申请人： Synopsys, Inc.
发明人： Himanshu Jain , Carl P. Pixley
IPC分类号： G06F17/50 , G06F9/455 , G06F7/487 , G06F9/30 , G06F7/552
CPC分类号： G06F17/5081 , G06F7/4873 , G06F7/4876 , G06F7/5525 , G06F9/3001 , G06F9/455 , G06F17/50 , G06F17/504
摘要： Methods and apparatuses are described for proving equivalence between two or more circuit designs that include one or more division circuits and/or one or more square-root circuits. Some embodiments analyze the circuit designs to determine an input relationship between the inputs of two division (or square-root) circuits. Next, the embodiments determine an output relationship between the outputs of two division (or square-root) circuits based on the input relationship. The embodiments then prove equivalence between the circuit designs by using the input and output relationships.

8. 发明授权

US10657307B1 Using runtime information from solvers to measure quality of formal verification 有权
公开(公告)号：US10657307B1
公开(公告)日：2020-05-19
申请号：US16023849
申请日：2018-06-29
申请人： Synopsys, Inc.
发明人： Himanshu Jain , Per M. Bjesse , Pratik Mahajan
IPC分类号： G06F30/00 , G06F30/3323 , G06F30/30
摘要： Systems and techniques are described for using runtime information to identify a verification hole and/or compute a verification metric. Runtime information (RI) for a set of proven assertions can be determined, wherein the RI includes a first set of registers, a first set of inputs, and a first set of constraints that were used by a formal verification engine during runtime to prove one or more assertions for a design under verification (DUV). Next, a second set of registers, a second set of inputs, and a second set of constraints that are not present in the RI can be determined. The second set of registers, the second set of inputs, and/or the second set of constraints can then be used to (1) identify a verification hole and/or (2) compute a verification metric.

9. 发明申请

US20160012177A1 EQUIVALENCE CHECKING BETWEEN TWO OR MORE CIRCUIT DESIGNS THAT INCLUDE SQUARE ROOT CIRCUITS 审中-公开
标题翻译：在包括平方根电路的两个或多个电路设计之间的等效检查
公开(公告)号：US20160012177A1
公开(公告)日：2016-01-14
申请号：US14860549
申请日：2015-09-21
申请人： Synopsys, Inc.
发明人： Himanshu Jain , Carl P. Pixley
IPC分类号： G06F17/50
CPC分类号： G06F17/5081 , G06F7/4873 , G06F7/4876 , G06F7/5525 , G06F9/3001 , G06F9/455 , G06F17/50 , G06F17/504
摘要： Methods and apparatuses are described for proving equivalence between two or more circuit designs that include one or more division circuits and/or one or more square-root circuits. Some embodiments analyze the circuit designs to determine an input relationship between the inputs of two division (or square-root) circuits. Next, the embodiments determine an output relationship between the outputs of two division (or square-root) circuits based on the input relationship. The embodiments then prove equivalence between the circuit designs by using the input and output relationships.
摘要翻译：描述了用于证明包括一个或多个分割电路和/或一个或多个平方根电路的两个或更多个电路设计之间的等效性的方法和装置。一些实施例分析电路设计以确定两个分割（或平方根）电路的输入之间的输入关系。接下来，实施例基于输入关系确定两个分割（或平方根）电路的输出之间的输出关系。然后，实施例通过使用输入和输出关系来证明电路设计之间的等同性。

你已经成功收藏专利！

检索式保存成功!

IPRDB

热门服务

关于我们

友情链接

联系方式