公开(公告)号：US20110225568A1

公开(公告)日：2011-09-15

申请号：US12719971

申请日：2010-03-09

申请人： Sreeranga P. Rajan ,  Mukul Prasad ,  Oksana Tkachuk ,  Indradeep Ghosh

发明人： Sreeranga P. Rajan ,  Mukul Prasad ,  Oksana Tkachuk ,  Indradeep Ghosh

IPC分类号： G06F9/44 ,  G06F3/048

CPC分类号： G06F11/3608 ,  G06F11/3696

摘要： In one embodiment, a method includes accessing an event-driven application input by a user, the event-driven application comprising source code, one or more use cases input by the user for the event-driven application, and one or more functional requirements input by the user for the event-driven application; parsing the use cases and the functional requirements according to the predefined syntax to construct one or more validation modules for validating the event-driven application without any modification to the source code of the event-driven application for validation purposes; formally validating the event-driven application using the validation modules without relying on assertions inserted into the source code of the event-driven application for validation purposes; and if the formal validation finds one or more defects in the event-driven application, generating output for communication to the user identifying the defects.

摘要翻译： 在一个实施例中，一种方法包括访问由用户输入的事件驱动应用程序，事件驱动的应用程序包括源代码，用户为事件驱动的应用程序输入的一个或多个用例以及一个或多个功能需求输入 由用户为事件驱动应用程序; 根据预定义的语法解析用例和功能需求，以构建用于验证事件驱动应用程序的一个或多个验证模块，而不用任何修改事件驱动应用程序的源代码进行验证; 使用验证模块正式验证事件驱动的应用程序，而不依赖插入到事件驱动应用程序的源代码中的断言来进行验证; 并且如果形式验证在事件驱动的应用程序中发现一个或多个缺陷，则产生用于识别缺陷的用户通信的输出。

公开(公告)号：US20070022394A1

公开(公告)日：2007-01-25

申请号：US11185231

申请日：2005-07-19

申请人： Indradeep Ghosh ,  Mukul Prasad

发明人： Indradeep Ghosh ,  Mukul Prasad

IPC分类号： G06F17/50

CPC分类号： G06F17/504

摘要： Estimating the difficulty level of a verification problem includes receiving input comprising a design and properties that may be verified on the design. Verification processes are performed for each property on the design. A property verifiability metric value is established for each property in accordance with the verification processes, where a property verifiability metric value represents a difficulty level of verifying the property on the design. A design verifiability metric value is determined from the property verifiability metric values, where the design verifiability metric value represents a difficulty level of verifying the design.

摘要翻译： 估计验证问题的难度级别包括接收包括可以在设计上验证的设计和属性的输入。 对设计中的每个属性执行验证过程。 根据验证过程为每个属性建立属性验证度量值，其中属性可验证度度值表示验证设计上的属性的难度级别。 设计验证度量值是从属性可验证性度量值确定的，其中设计验证度量值代表验证设计的难度级别。

公开(公告)号：US20050216871A1

公开(公告)日：2005-09-29

申请号：US10807959

申请日：2004-03-23

申请人： Mukul Prasad ,  Rajarshi Mukherjee

发明人： Mukul Prasad ,  Rajarshi Mukherjee

IPC分类号： G06N5/04 ,  G06F17/50

CPC分类号： G06F17/504

摘要： In one embodiment, a method for scheduling events in a Boolean satisfiability (SAT) solver includes collecting one or more first-order statistics on a search for a valid solution to an SAT problem, deriving one or more second-order statistics on the search from the one or more first-order statistics, and scheduling events in the search according to one or more of the second-order statistics.

摘要翻译： 在一个实施例中，一种用于在布尔可满足度（SAT）求解器中调度事件的方法包括在搜索针对SAT问题的有效解决方案时收集一个或多个一阶统计信息，从而导出关于搜索的一个或多个二阶统计信息 一个或多个一阶统计信息，以及根据一个或多个二阶统计量的搜索中的调度事件。

公开(公告)号：US20050262456A1

公开(公告)日：2005-11-24

申请号：US11119489

申请日：2005-04-29

申请人： Mukul Prasad

发明人： Mukul Prasad

IPC分类号： G06F17/50

CPC分类号： G06F17/504

摘要： In one embodiment, a method for satisfiability (SAT)-based bounded model checking (BMC) includes isolating information learned from a first iteration of an SAT-based BMC process and applying the isolated information from the first iteration of the SAT-based BMC process to a second iteration of the SAT-based BMC process subsequent to the first iteration.

摘要翻译： 在一个实施例中，一种基于可满足性（SAT）的有界模型检查（BMC）方法包括隔离从基于SAT的BMC过程的第一次迭代中学习的信息，并从基于SAT的BMC过程的第一次迭代中应用隔离信息 到第一次迭代之后的基于SAT的BMC进程的第二次迭代。

公开(公告)号：US08453117B2

公开(公告)日：2013-05-28

申请号：US12719971

申请日：2010-03-09

申请人： Sreeranga P. Rajan ,  Mukul Prasad ,  Oksana Tkachuk ,  Indradeep Ghosh

发明人： Sreeranga P. Rajan ,  Mukul Prasad ,  Oksana Tkachuk ,  Indradeep Ghosh

IPC分类号： G06F9/44 ,  G06F3/00

CPC分类号： G06F11/3608 ,  G06F11/3696

摘要： In one embodiment, a method includes accessing an event-driven application input by a user, the event-driven application comprising source code, one or more use cases input by the user for the event-driven application, and one or more functional requirements input by the user for the event-driven application; parsing the use cases and the functional requirements according to the predefined syntax to construct one or more validation modules for validating the event-driven application without any modification to the source code of the event-driven application for validation purposes; formally validating the event-driven application using the validation modules without relying on assertions inserted into the source code of the event-driven application for validation purposes; and if the formal validation finds one or more defects in the event-driven application, generating output for communication to the user identifying the defects.

摘要翻译： 在一个实施例中，一种方法包括访问由用户输入的事件驱动应用程序，事件驱动的应用程序包括源代码，用户为事件驱动的应用程序输入的一个或多个用例以及一个或多个功能需求输入 由用户为事件驱动应用程序; 根据预定义的语法解析用例和功能需求，以构建用于验证事件驱动应用程序的一个或多个验证模块，而不用任何修改事件驱动应用程序的源代码进行验证; 使用验证模块正式验证事件驱动的应用程序，而不依赖插入到事件驱动应用程序的源代码中的断言来进行验证; 并且如果形式验证在事件驱动的应用程序中发现一个或多个缺陷，则产生用于识别缺陷的用户通信的输出。

公开(公告)号：US20060212837A1

公开(公告)日：2006-09-21

申请号：US11082592

申请日：2005-03-17

申请人： Mukul Prasad

发明人： Mukul Prasad

IPC分类号： G06F17/50

CPC分类号： G06F17/504

摘要： A method for verifying a digital system design is provided. A first abstraction of a digital system design is performed to obtain an abstract model of the digital system design. One or more first steps of a multiple-step model checking process are performed using the abstract model, the multiple-step model checking process being operable to verify the digital system design. During the multiple-step model checking process, a second abstraction is performed to refine the abstract model. One or more second steps of the multiple-step model checking process are then performed using the refined abstract model.

摘要翻译： 提供了一种用于验证数字系统设计的方法。 执行数字系统设计的第一次抽象以获得数字系统设计的抽象模型。 使用抽象模型执行多步模型检查过程的一个或多个第一步骤，多步模型检查过程可操作以验证数字系统设计。 在多步模型检查过程中，执行第二次抽象以改进抽象模型。 然后使用精细抽象模型执行多步模型检查过程的一个或多个第二步骤。