Extracting, visualizing, and acting on inconsistencies between a circuit design and its abstraction
    1.
    发明授权
    Extracting, visualizing, and acting on inconsistencies between a circuit design and its abstraction 有权
    提取,可视化和对电路设计与其抽象之间的不一致行为

    公开(公告)号:US07895552B1

    公开(公告)日:2011-02-22

    申请号:US11092994

    申请日:2005-03-28

    IPC分类号: G06F17/50

    CPC分类号: G06F17/504

    摘要: In the field of functional verification of digital designs in systems that use an abstraction for portions of a circuit design to perform the verification proof, a tool is described for resolving inconsistencies between the design and abstractions for the design. The tool provides information to a user about intermediate steps in the verification process. In response, the user may provide insight about the design to allow the tool to adjust the verification analysis of the design. The information provided to the user, including possible conflicts between the design and its abstractions, may include visualization techniques to facilitate the user's understating of any inconsistencies.

    摘要翻译: 在使用电路设计部分的抽象来执行验证证明的系统中的数字设计的功能验证领域中,描述了用于解决设计和设计抽象之间不一致的工具。 该工具向用户提供有关验证过程中的中间步骤的信息。 作为响应,用户可以提供关于设计的洞察,以允许工具调整设计的验证分析。 提供给用户的信息,包括设计与其抽象之间可能的冲突,可能包括可视化技术,以便于用户低估任何不一致之处。

    System and method for identifying design efficiency and effectiveness parameters for verifying properties of a circuit model
    2.
    发明授权
    System and method for identifying design efficiency and effectiveness parameters for verifying properties of a circuit model 有权
    识别电路模型性能的设计效率和有效性参数的系统和方法

    公开(公告)号:US07159198B1

    公开(公告)日:2007-01-02

    申请号:US10745993

    申请日:2003-12-24

    IPC分类号: G06F17/50

    CPC分类号: G06F17/504

    摘要: The present invention is directed to a system and a method for verifying properties of a circuit model while providing information to help the user manually modify a design analysis region and/or environmental constraints. While conventional systems attempt to substantially automate the entire formal verification process, the present invention iteratively provides information to the user about the cost and effect of changes to the environmental constraints and the analysis region. This information enables the user to weigh the effectiveness and efficiency of one or more modifications to the design analysis area and/or to the environmental constraints (assumptions). The information provided to the user can help a user compare a variety of alternative modifications in order to select the modifications that are efficient and effective. In addition, the information can provide alternatives along with the cost and effect of each alternative to the user who otherwise did not identify these alternatives, thus the invention can help the user by identifying suggestions that the user may not have otherwise considered. The present invention then receives information from the user to modify the design analysis area and/or the environmental constraints and will analyze the design with these modified parameters.

    摘要翻译: 本发明涉及一种用于验证电路模型的属性的系统和方法,同时提供信息以帮助用户手动修改设计分析区域和/或环境约束。 虽然常规系统试图使整个形式验证过程大幅自动化,但是本发明向用户反复地提供关于环境约束和分析区域的改变的成本和效果的信息。 该信息使用户能够对设计分析区域和/或环境约束(假设)的一个或多个修改的有效性和效率进行权衡。 提供给用户的信息可以帮助用户比较各种替代修改以选择有效和有效的修改。 此外,该信息可以提供替代方案以及用户的每个备选方案的成本和效果,否则其中没有识别这些替代方案,因此本发明可以通过识别用户可能没有另外考虑的建议来帮助用户。 然后,本发明从用户接收信息以修改设计分析区域和/或环境约束,并将用这些修改的参数分析设计。

    System and method for determining and identifying signals that are relevantly determined by a selected signal in a circuit design
    3.
    发明授权
    System and method for determining and identifying signals that are relevantly determined by a selected signal in a circuit design 有权
    用于确定和识别在电路设计中由选定信号相关确定的信号的系统和方法

    公开(公告)号:US07437694B1

    公开(公告)日:2008-10-14

    申请号:US11063399

    申请日:2005-02-22

    IPC分类号: G06F17/50

    CPC分类号: G06F17/504 G06F17/5022

    摘要: A system and method for identifying, for a selected signal, those signals whose value is relevantly determined based upon a value of the selected signal, where a set of signals to be examined is identified as those signals that satisfy one or more of the following criteria: (1) they are RTL load signals of the selected signal, (2) they are RTL load signals that are also in an analysis region, (3) they are RTL load signals within the analysis region that also contribute to a proof target, and/or 4) they are RTL load signals that contribute to the proof target. In one embodiment of the present invention the selected signal at a selected time step relevantly determines a target signal at an associated time step if one of the following items is true: (1) if the value of the selected signal at the selected time step changes (from 0 to 1 or from 1 to 0), the value of the target signal must change, or (2) if the value of the selected signal does not change, the value of the target signal at its associated time step cannot change regardless of how the rest of the inputs to the logic driving the target signal changes. Another embodiment of the present invention, the selected signal at the selected time step relevantly determines a target signal at an associated time step if the value of the selected signal at the selected time step were different then the value of the target signal at the associated time step would be different.

    摘要翻译: 一种用于针对所选择的信号识别基于所选信号的值相关地确定其值的那些信号的系统和方法,其中要被检查的一组信号被识别为满足以下标准中的一个或多个的信号 (1)它们是所选信号的RTL负载信号,(2)它们也是分析区域中的RTL负载信号,(3)它们是分析区域内也有助于证明目标的RTL负载信号, 和/或4)它们是有助于证明目标的RTL负载信号。 在本发明的一个实施例中,如果以下项目之一为真,则所选择的时间步骤中所选择的信号相关地确定在相关联的时间步长处的目标信号:(1)如果所选择的时间步长上所选信号的值改变 (从0到1或从1到0),目标信号的值必须改变,或(2)如果所选择的信号的值不改变,则在其相关联的时间步长的目标信号的值不能改变 驱动目标信号的逻辑的其余输入如何变化。 本发明的另一个实施例是,在所选择的时间步长中所选择的信号相关地确定在相关联的时间步长处的目标信号,如果所选择的时间步长的所选择的信号的值与相关时间的目标信号的值不同 一步就会有所不同。

    Adjustable, curved keyboard
    4.
    发明授权

    公开(公告)号:US5735619A

    公开(公告)日:1998-04-07

    申请号:US626038

    申请日:1996-04-01

    申请人: Soe Myint

    发明人: Soe Myint

    IPC分类号: G06F3/02 H01H13/84 B41J5/08

    摘要: There is provided an adjustable, curved keyboard having arcuately arranged keys to complement naturally to a user's wrists, hands and fingers. The keyboard is supported by a bracket, which extends from underneath the desktop of a desk, for pivotal, elevational and horizontal adjustment of the keyboard's position relative to the user. The keyboard comprises an elongated base and alphanumeric keys positioned at an upper surface of the base. The base has a longitudinal axis disposed below the upper surface of the elongated base, and the upper surface is curved about the longitudinal axis. Also, the alphanumeric keys are arranged about the longitudinal axis of the base to form an arcuate typing surface that provides a comfortable typing surface for the user and reduces the risks of repetitive stress injury.

    Identifying inconsistent constraints
    5.
    发明授权
    Identifying inconsistent constraints 有权
    识别不一致的约束

    公开(公告)号:US09069699B2

    公开(公告)日:2015-06-30

    申请号:US13074940

    申请日:2011-03-29

    CPC分类号: G06F17/11 G06F17/5018

    摘要: Methods and apparatuses are described for identifying inconsistent constraints. During operation, a system can receive a set of constraints, wherein each constraint is defined over one or more random variables from a set of random variables. If an inconsistency or conflict is detected while solving the set of constraints, the system can identify a phase in a series of phases of the constraint solver where the inconsistency was detected. The system can then try to solve different subsets of the set of constraints to identify smaller subsets of the set of constraints that contain the inconsistency. When the system tries to solve a subset of the set of constraints, the system can determine whether or not an inconsistency is detected in the identified phase while solving the subset of the set of constraints. Next, the system can report the smallest subset of inconsistent constraints that was found to a user.

    摘要翻译: 描述了用于识别不一致约束的方法和装置。 在操作期间,系统可以接收一组约束,其中每个约束被从一组随机变量的一个或多个随机变量上定义。 如果在解决一组约束的同时检测到不一致或冲突,则系统可以识别在检测到不一致的约束求解器的一系列阶段中的阶段。 系统然后可以尝试解决该组约束的不同子集以识别包含不一致性的约束集合的较小子集。 当系统尝试解决约束集合的子集时,系统可以确定在确定的相位集合中是否检测到不一致性,同时解决该组约束的子集。 接下来,系统可以报告对用户发现的不一致约束的最小子集。

    METHOD AND APPARATUS FOR IDENTIFYING INCONSISTENT CONSTRAINTS
    6.
    发明申请
    METHOD AND APPARATUS FOR IDENTIFYING INCONSISTENT CONSTRAINTS 有权
    识别不确定性约束的方法和装置

    公开(公告)号:US20120253754A1

    公开(公告)日:2012-10-04

    申请号:US13074940

    申请日:2011-03-29

    IPC分类号: G06F17/11

    CPC分类号: G06F17/11 G06F17/5018

    摘要: Methods and apparatuses are described for identifying inconsistent constraints. During operation, a system can receive a set of constraints, wherein each constraint is defined over one or more random variables from a set of random variables. If an inconsistency or conflict is detected while solving the set of constraints, the system can identify a phase in a series of phases of the constraint solver where the inconsistency was detected. The system can then try to solve different subsets of the set of constraints to identify smaller subsets of the set of constraints that contain the inconsistency. When the system tries to solve a subset of the set of constraints, the system can determine whether or not an inconsistency is detected in the identified phase while solving the subset of the set of constraints. Next, the system can report the smallest subset of inconsistent constraints that was found to a user.

    摘要翻译: 描述了用于识别不一致约束的方法和装置。 在操作期间,系统可以接收一组约束,其中每个约束被从一组随机变量的一个或多个随机变量上定义。 如果在解决一组约束的同时检测到不一致或冲突,则系统可以识别在检测到不一致的约束求解器的一系列阶段中的阶段。 系统然后可以尝试解决该组约束的不同子集,以识别包含不一致性的约束集合的较小子集。 当系统尝试解决约束集合的子集时,系统可以确定在所确定的阶段中是否检测到不一致性,同时解决该组约束的子集。 接下来,系统可以报告对用户发现的不一致约束的最小子集。

    Adjustable, curved keyboard
    7.
    发明授权
    Adjustable, curved keyboard 失效
    可调节,曲线键盘

    公开(公告)号:US6059470A

    公开(公告)日:2000-05-09

    申请号:US162027

    申请日:1998-09-28

    申请人: Soe Myint

    发明人: Soe Myint

    IPC分类号: G06F3/02 H01H13/84 B41J5/08

    摘要: There is provided an adjustable, curved keyboard having arcuately arranged keys to complement naturally to a user's wrists, hands and fingers. The keyboard is supported by a bracket, which extends from underneath the desktop of a desk, for pivotal, elevational and horizontal adjustment of the keyboard's position relative to the user. The keyboard comprises an elongated base and alphanumeric keys positioned at an upper surface of the base. The base has a longitudinal axis disposed below the upper surface of the elongated base, and the upper surface is curved about the longitudinal axis. Also, the alphanumeric keys are arranged about the longitudinal axis of the base to form an arcuate typing surface that provides a comfortable typing surface for the user and reduces the risks of repetitive stress injury.

    摘要翻译: 提供了一种可调节的曲线键盘,其具有弧形排列的键,以自然地补偿用户的手腕,手和手指。 键盘由支架支撑,支架从桌面的桌面下方延伸,用于相对于用户的键盘位置的关键,高程和水平调整。 键盘包括位于基座的上表面处的细长基座和字母数字键。 基部具有设置在细长基部的上表面下方的纵向轴线,并且上表面围绕纵向轴线弯曲。 此外,字母数字键围绕基座的纵向轴线布置以形成弓形打字表面,其为用户提供舒适的打字表面并且减少重复性应力损伤的风险。