公开(公告)号：EP0445942A2

公开(公告)日：1991-09-11

申请号：EP91301469.2

申请日：1991-02-25

申请人： AT&T Corp.

发明人： Har'El, Zvi ,  Kurshan, Robert P.

IPC分类号： G06F15/60

CPC分类号： G06F17/5045 ,  G06F17/504

摘要： Designs are created through a high-level to low-level transformation in the form of a formal top-down development procedure based upon successive refinement. Starting with a high-level (abstract) model, such as a formal abstraction of a protocol standard, successively more detailed models are created through successive refinement, in a fashion which guarantees that properties verified at one level of abstraction hold in all successive levels of abstraction. The successive refinements end with a low-level "model" which forms the ultimate implementation of the protocol. In one embodiment of this invention, the analysis/development apparatus creates a unique C language code representation of the specified system that is guaranteed to carry out the tasks specified when executed in a stored program controlled machine. In another embodiment, the code is used to create a "net list" for manufacturing the specified system.

摘要翻译： 设计是通过基于连续细化的正式自上而下的开发过程的形式通过高级别到低级别的转换创建的。 从诸如协议标准的正式抽象的高级（抽象）模型开始，通过连续细化来创建连续更详细的模型，以保证在一个抽象级别验证的属性在所有连续级别中保持 抽象。 连续的细化结束于形成协议的最终实现的低级“模型”。 在本发明的一个实施例中，分析/开发装置创建指定系统的唯一C语言代码表示，该指定系统在被存储的程序控制机器中执行时被指定执行指定的任务。 在另一个实施例中，代码用于创建用于制造指定系统的“净列表”。

公开(公告)号：EP0403454A1

公开(公告)日：1990-12-19

申请号：EP90850184.4

申请日：1990-05-17

申请人： Stalmarck, Gunnar Martin Natanael

发明人： Stalmarck, Gunnar Martin Natanael

IPC分类号： G06F17/27

CPC分类号： G06F17/10 ,  G06F17/504 ,  G06N5/006

摘要： The invention relates to a method and apparatus for theorem checking with the intention in so-called tautology checks of establishing whether or not all possible attributions of the truth values (0 and 1) to variables in a boolean formula render the formula true. The problem of known techniques is that checking of the truth content is effected against all variables in an original formula, which requires many calculations to be made and which is highly time-consuming.
According to the invention, an original formula is divided into part-expressions, so-called triplets, each corresponding to a part-formula of the original formula, whereafter logic 0:s and 1:s are instantiated (allotted) to variables in the triplets for the purpose of checking the truth content. The check is thus made against triplets instead of against all variables in the original formula, therewith greatly reducing the number of calculations necessary and providing a considerable saving in time. Apparatus, called a theorem checker, for carrying out the method includes a sequence unit for controlling the calculation sequency, a generator G for generating sequences of ordered variables, a permanent unit P for storing triplets, a plurality of arithmetical units, evaluators (E) and an analyzer A operative to analyze the result obtain from all calculations.

摘要翻译： 本发明涉及一种用于定理检查的方法和装置，其意图在所谓的重复检查中确定真值（0和1）对于布尔公式中的变量的所有可能归属是否使公式为真。 已知技术的问题是检查真实内容是针对原始公式中的所有变量进行的，这需要进行许多计算并且是非常耗时的。 根据本发明，原始公式被分为部分表达式，即所谓的三元组，每个对应于原始公式的部分公式，之后逻辑0：s和1：s被实例化（分配）到 三重组，用于检查真相内容。 因此，检查是针对三元组，而不是原始公式中的所有变量，从而大大减少了必要的计算数量，并大大节省了时间。 称为定理检验器的装置，用于执行该方法，包括用于控制计算顺序的序列单元，用于产生有序变量序列的发生器G，用于存储三元组的永久单元P，多个算术单元，评估器（E） 以及分析器A，用于分析从所有计算获得的结果。

公开(公告)号：EP3408768A1

公开(公告)日：2018-12-05

申请号：EP17702915.4

申请日：2017-01-25

申请人： Imagination Technologies Limited

发明人： DARBARI, Ashish

IPC分类号： G06F17/50

CPC分类号： G06F17/504 ,  G06F17/5022 ,  G06F17/505 ,  G06F2217/06 ,  G06F2217/12

摘要： A method of detecting a bug in a counter of a hardware design that includes formally verifying, using a formal verification tool, an inductive assertion from a non-reset state of an instantiation of the hardware design. The inductive assertion establishes a relationship between the counter and a test bench counter at two or more points in time. If the formal verification tool identifies at least one valid state of an instantiation of the counter in which the inductive assertion is not true, information is output indicating a location of a bug in the hardware design or the test bench counter.

公开(公告)号：EP3382580A1

公开(公告)日：2018-10-03

申请号：EP17163776.2

申请日：2017-03-30

申请人： Technische Universität Wien

发明人： KRIEG, Christian ,  JANTSCH, Axel ,  MOSBECK, Martin

IPC分类号： G06F17/50

CPC分类号： G06F17/5045 ,  G06F17/504

摘要： A method for automatic detection of a functional primitive in a model of a hardware system, the model being a netlist (2) having cells (2') and net links (2") therebetween, comprising the steps:
a) mapping the cells (2') to nodes (4), each of which having a target node type, and the net links (2") to edges (11) of a target graph (3, 10), and mapping the functional primitive to a search pattern (14) having search nodes (19) and connections therebetween;
b) selecting candidates from those target nodes (4) the target node types of which match a search node type, and selecting a candidate structure from those selected candidates the target nodes (4) and edges (11) of which match the search nodes (19) and connections of the search pattern (14);
c) reverse-mapping the target nodes (4) and edges (11) of the selected candidate structure to the cells (2') and net links (2") of the netlist (2); and
d) outputting said cells (2') and net links (2") as detected functional primitive.

公开(公告)号：EP3236373A1

公开(公告)日：2017-10-25

申请号：EP17166522.7

申请日：2017-04-13

申请人： Semiconductor Manufacturing International Corporation (Shanghai) ,  Semiconductor Manufacturing International Corporation (Beijing)

发明人： HONG, Lin ,  LI, Xue

IPC分类号： G06F17/50

CPC分类号： G06F17/5077 ,  G06F17/504 ,  G06F17/5081 ,  G06F2217/12 ,  Y02P90/265

摘要： A method for optimizing manufacturability of standard cells includes generating random contexts for the standard cells, inserting vias into the standard cells, and performing a lithography verification on the standard cells after the vias have been inserted. The method enables early detection and resolution of potential hot spots on standard cell pin connections and reduction of hot spots that are introduced by the router at the chip level. The early detection and reduction of hot spots shortens the cycle time of a standard-cell based design.

摘要翻译： 用于优化标准单元的可制造性的方法包括为标准单元产生随机上下文，将过孔插入标准单元中，并且在已经插入过孔之后对标准单元执行光刻验证。 该方法使得能够及早检测和解决标准单元引脚连接上的潜在热点并且减少路由器在芯片级引入的热点。 热点的早期检测和减少缩短了基于标准单元的设计的周期时间。

公开(公告)号：EP2414852A4

公开(公告)日：2014-07-30

申请号：EP10749422

申请日：2010-03-05

申请人： SYNOPSYS INC

发明人： GU ZHENYU ,  MCELVAIN KENNETH S

IPC分类号： G01R31/303 ,  G01R19/00 ,  G06F17/50

CPC分类号： G06F17/505 ,  G06F17/5022 ,  G06F17/504 ,  G06F2217/10 ,  G06F2217/78

公开(公告)号：EP2350892A4

公开(公告)日：2014-07-23

申请号：EP09825241

申请日：2009-10-28

申请人： APPLE INC

发明人： NODINE MARK H

IPC分类号： G06F17/50

CPC分类号： G06F17/504

公开(公告)号：EP2720149A2

公开(公告)日：2014-04-16

申请号：EP13183531.6

申请日：2013-09-09

申请人： Samsung Electronics Co., Ltd

发明人： Jung, Jin-Sae ,  Shim, Hee-Jun ,  Cho, Young-Chul ,  Han, Yen-Jo

IPC分类号： G06F11/263

CPC分类号： G06F8/43 ,  G06F8/41 ,  G06F17/5022 ,  G06F17/5031 ,  G06F17/504

摘要： Exemplary embodiments disclose a method for generating an assertion based on a user program code. The method may include receiving a user program comprising at least one assertion directive, a compiled result of the user program, and architecture information of a processor, and generating, based on the compiled result of the user program and the architecture information of the processor, an assertion which states an operation that the processor needs to perform in accordance with a code of the user program indicated by each of the at least one assertion directive.

摘要翻译： 示例性实施例公开了一种用于基于用户的程序代码在断言生成的方法。 该方法可以包括：接收用户程序包括至少一个断言指令，用户程序和处理器的体系结构的信息，以及生成的一个编译的结果，基于用户程序和处理器的体系结构的信息的经编译的结果， 哪些国家的主张手术做的处理器需要在雅舞蹈与每个至少一个断言指令指示的用户程序的代码来执行。

公开(公告)号：EP2718859A1

公开(公告)日：2014-04-16

申请号：EP12732964.7

申请日：2012-06-06

申请人： Hyperion Core, Inc.

发明人： VORBACH Martin

IPC分类号： G06F17/50

CPC分类号： G06F8/443 ,  G06F8/4434 ,  G06F8/447 ,  G06F17/504 ,  G06F17/5045 ,  G06F17/5054

摘要： The present invention relates to a method for compiling high-level software code into hardware, transforming each instruction into a respective hardware block and using an execution control signal representing the program pointer for triggering the execution within each respective hardware block.

摘要翻译： 本发明涉及一种用于将高级软件代码编译成硬件的方法，将每个指令变换成相应的硬件块，并且使用表示程序指针的执行控制信号来触发各个硬件块内的执行。

公开(公告)号：EP2382570A4

公开(公告)日：2013-11-27

申请号：EP10736234

申请日：2010-01-19

申请人： SYNOPSYS INC

发明人： DSOUZA ASHVIN M

IPC分类号： G06F19/00 ,  G01R31/28 ,  G06F17/50

CPC分类号： G06F17/5022 ,  G06F17/504