公开(公告)号：US07469392B2

公开(公告)日：2008-12-23

申请号：US11298120

申请日：2005-12-08

申请人： Yiu Chung Mang ,  Pei-Hsin Ho

发明人： Yiu Chung Mang ,  Pei-Hsin Ho

IPC分类号： G06F17/50

CPC分类号： G06F17/504

摘要： One embodiment of the present invention provides a system that refines an abstract model. Note that abstraction refinement is commonly used in formal property verification. During operation, the system receives an abstract model which is a subset of a logic design which can be represented using a set of variables and a set of Boolean functions. Next, the system receives a safety property for the logic design which is desired to be proven. The system also receives a set of counter-examples. A counter-example is a sequence of states that violates the safety property. Note that a state is an assignment of values to the variables, which are determined using the set of Boolean functions and the variable values in the previous state. The system then determines a set of cooperative variables using the set of counter-examples. A cooperative variable is a variable that can help invalidate all counter-examples. The system then refines the abstract model using the set of cooperative variables.

摘要翻译： 本发明的一个实施例提供了一种改进抽象模型的系统。 请注意，抽象精简通常用于形式属性验证。 在操作期间，系统接收抽象模型，该抽象模型是可以使用一组变量和一组布尔函数来表示的逻辑设计的子集。 接下来，系统接收要被证明的逻辑设计的安全属性。 该系统还接收一组反例。 反例是违反安全属性的一系列状态。 请注意，状态是赋值给变量的值，它们使用布尔函数集和前一个状态中的变量值来确定。 然后，系统使用一组反例来确定一组协作变量。 合作变量是一个可以帮助无效所有反例的变量。 然后，系统使用一组合作变量来提炼抽象模型。