Determining one or more reachable states in a circuit using distributed computing and one or more partitioned data structures
    1.
    发明授权
    Determining one or more reachable states in a circuit using distributed computing and one or more partitioned data structures 失效
    使用分布式计算和一个或多个分区数据结构确定电路中的一个或多个可达状态

    公开(公告)号:US07216312B2

    公开(公告)日:2007-05-08

    申请号:US10704234

    申请日:2003-11-07

    IPC分类号: G06F17/50

    CPC分类号: G06F17/504

    摘要: In one embodiment, a method for determining one or more reachable states in a circuit using distributed computing and one or more partitioned data structures includes, at a first one of multiple computing systems, receiving a first partition of a circuit. The first partition corresponds to a first binary decision diagram (BDD) having a first density. The method includes performing a first reachability analysis on the first partition using the first BDD until a fixed point in the first partition has been reached and, if, during the first reachability analysis, the size of the first BDD exceeds a threshold, discarding the first BDD. The method includes communicating with at least one second one of the multiple computing systems. The second one of the multiple computing systems has received a second partition of the circuit. The second one of the multiple computing systems has performed a second reachability analysis on the second BDD without discarding the second BDD.

    摘要翻译: 在一个实施例中,用于使用分布式计算和一个或多个分区数据结构来确定电路中的一个或多个可达状态的方法包括在多个计算系统中的第一个处接收电路的第一分区。 第一分区对应于具有第一密度的第一二进制决策图(BDD)。 该方法包括使用第一BDD对第一分区执行第一可达性分析,直到达到第一分区中的固定点,并且如果在第一可达性分析期间第一BDD的大小超过阈值,则丢弃第一 BDD。 该方法包括与多个计算系统中的至少一个第二个通信。 多个计算系统中的第二个已经接收到电路的第二分区。 多个计算系统中的第二个对第二BDD进行了第二次可达性分析,而不丢弃第二个BDD。

    Circuit verification
    2.
    发明授权
    Circuit verification 失效
    电路验证

    公开(公告)号:US07571403B2

    公开(公告)日:2009-08-04

    申请号:US11279177

    申请日:2006-04-10

    IPC分类号: G06F17/50

    CPC分类号: G06F17/504

    摘要: In one embodiment, a method for verifying one or more particular properties of a circuit using a learning strategy to determine suitable values of particular verification parameters includes classifying each of multiple properties of a circuit according to circuit size and selecting a candidate property from the properties. The candidate property set includes one or more particular properties from each property class. The method also includes attempting to verify one or more particular properties of the circuit using the candidate property set and particular values of particular verification parameters. The method also includes determining suitable values of the particular verification parameters according the attempted verification of the particular properties of the circuit using the candidate property set and the particular values of the particular verification parameters.

    摘要翻译: 在一个实施例中,使用学习策略来验证电路的一个或多个特定属性以确定特定验证参数的合适值的方法包括根据电路大小对电路的多个属性进行分类,并从属性中选择候选属性。 候选属性集包括每个属性类的一个或多个特定属性。 该方法还包括使用候选属性集和特定验证参数的特定值来尝试验证电路的一个或多个特定属性。 该方法还包括根据使用候选属性集和特定验证参数的特定值的电路的特定属性的尝试验证来确定特定验证参数的合适值。

    Circuit verification
    3.
    发明授权
    Circuit verification 失效
    电路验证

    公开(公告)号:US07028279B2

    公开(公告)日:2006-04-11

    申请号:US10444782

    申请日:2003-05-23

    IPC分类号: G06F9/45 G06F17/50

    CPC分类号: G06F17/504

    摘要: In one embodiment, a system for verifying a circuit using a scheduling technique includes one or more partitioned ordered binary decision diagram (POBDD) modules that collectively generate one or more POBDDs. Each POBDD corresponds to one or more partitions of a state space of the circuit and includes a number of states and a number of nodes in the partition. The system also includes one or more cost metrics modules that collectively determine a processing cost of each of the partitions of each of the POBDDs. The system also includes one or more scheduling modules that collectively schedule processing of the partitions of the POBDDs for semiformal verification of a circuit. The schedule is based, at least in part, on the determined processing costs of the partitions of the POBDDs.

    摘要翻译: 在一个实施例中,用于使用调度技术验证电路的系统包括共同生成一个或多个POBDD的一个或多个分区排序二进制决策图(POBDD)模块。 每个POBDD对应于电路的状态空间的一个或多个分区,并且包括分区中的多个状态和多个节点。 该系统还包括共同确定每个POBDD的每个分区的处理成本的一个或多个成本度量模块。 该系统还包括一个或多个调度模块,其共同调度POBDD的分区的处理以对电路进行半正式验证。 该计划至少部分地基于POBDD分区的确定的处理成本。

    System and method for executing image computation associated with a target circuit
    4.
    发明授权
    System and method for executing image computation associated with a target circuit 有权
    用于执行与目标电路相关联的图像计算的系统和方法

    公开(公告)号:US07032197B2

    公开(公告)日:2006-04-18

    申请号:US10454207

    申请日:2003-06-04

    IPC分类号: G06F17/50

    CPC分类号: G06F17/504

    摘要: A method for verifying a property associated with a target circuit is provided that includes receiving information associated with a target circuit, the information identifying a property within the target circuit to be verified. One or more operations may be executed in order to generate a set of transition relations for performing a reachability analysis associated with the target circuit. An image associated with the target circuit may be partitioned into a plurality of leaves that may each represent a subset of a final image to be generated by a partitioned ordered binary decision diagram (POBDD) data structure. An analysis may be computed of one or more of the leaves using a selected one or both of conjunction and quantification operations separately.

    摘要翻译: 提供了一种用于验证与目标电路相关联的属性的方法,其包括接收与目标电路相关联的信息,所述信息标识要验证的目标电路内的属性。 可以执行一个或多个操作,以便生成用于执行与目标电路相关联的可达性分析的一组过渡关系。 与目标电路相关联的图像可以被划分成多个叶,每个叶各自表示将由分区有序二元决策图(POBDD)数据结构生成的最终图像的子集。 可以分别使用选择的一个或两个连接和定量操作来计算一个或多个叶子的分析。

    System and method for evaluating an erroneous state associated with a target circuit
    5.
    发明授权
    System and method for evaluating an erroneous state associated with a target circuit 有权
    用于评估与目标电路相关联的错误状态的系统和方法

    公开(公告)号:US07788556B2

    公开(公告)日:2010-08-31

    申请号:US10390982

    申请日:2003-03-17

    IPC分类号: G01R31/28

    CPC分类号: G06F17/504

    摘要: A method for evaluating an erroneous state associated with a target circuit is provided that includes receiving information associated with a target circuit, the information identifying a property within the target circuit to be verified. One or more partitioned ordered binary decision diagram (POBDD) operations are executed using the information in order to identify an erroneous state associated with a sub-space within the target circuit. A path associated with the erroneous state is identified. The path reflects a correlation between an initial state associated with the erroneous state and a point where the erroneous state was encountered.

    摘要翻译: 提供了一种用于评估与目标电路相关联的错误状态的方法,包括接收与目标电路相关联的信息,所述信息标识要验证的目标电路内的属性。 使用该信息执行一个或多个分区排序二进制决策图(POBDD)操作,以便识别与目标电路内的子空间相关联的错误状态。 识别与错误状态相关联的路径。 该路径反映与错误状态相关联的初始状态与遇到错误状态的点之间的相关性。

    System and method for verifying a plurality of states associated with a target circuit
    6.
    发明授权
    System and method for verifying a plurality of states associated with a target circuit 失效
    用于验证与目标电路相关联的多个状态的系统和方法

    公开(公告)号:US06904578B2

    公开(公告)日:2005-06-07

    申请号:US10391282

    申请日:2003-03-17

    IPC分类号: G06F17/50 G01R31/28 G06F9/45

    CPC分类号: G06F17/504

    摘要: A method for verifying a property associated with a target circuit is provided that includes receiving information associated with a target circuit, the information identifying a property within the target circuit to be verified. One or more partitioned ordered binary decision diagram (POBDD) operations are then executed using the information in order to generate a first set of states at a first depth associated with a sub-space within the target circuit. Bounded model checking may be executed using the first set of states in order to generate a second set of states at a second depth associated with the sub-space within the target circuit. The first set of states may be used as a basis for the second set of states such that the second depth is greater than the first depth.

    摘要翻译: 提供了一种用于验证与目标电路相关联的属性的方法,其包括接收与目标电路相关联的信息,所述信息标识要验证的目标电路内的属性。 然后使用该信息执行一个或多个分区有序二元判定图(POBDD)操作,以便产生与目标电路内的子空间相关联的第一深度的第一组状态。 可以使用第一组状态来执行有界模型检查,以便在与目标电路内的子空间相关联的第二深度处产生第二组状态。 可以将第一组状态用作第二组状态的基础,使得第二深度大于第一深度。

    Circuit Verification
    7.
    发明申请
    Circuit Verification 失效
    电路验证

    公开(公告)号:US20060173666A1

    公开(公告)日:2006-08-03

    申请号:US11279177

    申请日:2006-04-10

    IPC分类号: G06F17/50

    CPC分类号: G06F17/504

    摘要: In one embodiment, a method for verifying one or more particular properties of a circuit using a learning strategy to determine suitable values of particular verification parameters includes classifying each of multiple properties of a circuit according to circuit size and selecting a candidate property from the properties. The candidate property set includes one or more particular properties from each property class. The method also includes attempting to verify one or more particular properties of the circuit using the candidate property set and particular values of particular verification parameters. The method also includes determining suitable values of the particular verification parameters according the attempted verification of the particular properties of the circuit using the candidate property set and the particular values of the particular verification parameters.

    摘要翻译: 在一个实施例中,使用学习策略来验证电路的一个或多个特定属性以确定特定验证参数的合适值的方法包括根据电路大小对电路的多个属性进行分类,并从属性中选择候选属性。 候选属性集包括每个属性类的一个或多个特定属性。 该方法还包括使用候选属性集和特定验证参数的特定值来尝试验证电路的一个或多个特定属性。 该方法还包括根据使用候选属性集和特定验证参数的特定值的电路的特定属性的尝试验证来确定特定验证参数的合适值。

    Method and apparatus for steady state analysis of a voltage controlled oscillator
    8.
    发明授权
    Method and apparatus for steady state analysis of a voltage controlled oscillator 有权
    压控振荡器的稳态分析方法和装置

    公开(公告)号:US07332974B1

    公开(公告)日:2008-02-19

    申请号:US11045241

    申请日:2005-01-27

    IPC分类号: G06F17/50 G01R23/06

    CPC分类号: G06F17/5036 G06F17/504

    摘要: A computer-implemented method computes the steady-state and control voltage of a voltage controlled oscillator, given a known frequency or a known period of oscillation of the voltage controlled oscillator. Differential algebraic equations representative of the voltage controlled oscillator are generated, where the differential algebraic equations includes a known period or frequency of oscillation and an unknown control voltage of the voltage controlled oscillator. The differential algebraic equations are modified using a finite difference method, a shooting method, or a harmonic balance method, to obtain a set of matrix equations corresponding to the differential algebraic equations. A solution to the matrix equations is obtained using a Krylov subspace method, using a preconditioner for the Krylov subspace method that is derived from a Jacobian matrix corresponding to the matrix equations, where the solution includes the control voltage of the voltage controlled oscillator in steady state.

    摘要翻译: 给定已知频率或压控振荡器的已知振荡周期,计算机实现的方法计算压控振荡器的稳态和控制电压。 产生代表压控振荡器的差分代数方程,其中微分代数方程包括已知的振荡周期或频率以及压控振荡器的未知控制电压。 使用有限差分法,拍摄方法或谐波平衡法来修正差分代数方程,以获得对应于微分代数方程的一组矩阵方程。 使用Krylov子空间方法获得矩阵方程的解,使用从矩阵方程对应的雅可比矩阵导出的Krylov子空间方法的预处理器,其中解包括稳压状态下的压控振荡器的控制电压 。