公开(公告)号：EP2088521A1

公开(公告)日：2009-08-12

申请号：EP08002479.7

申请日：2008-02-11

申请人： Onespin Solutions GmbH

发明人： Beyer, Sven ,  Schönherr, Jens ,  Bormann, Jörg

IPC分类号： G06F17/50

CPC分类号： G06F17/504

摘要： A method for verifying at least one aspects of a digital circuit, the method comprising: providing a set of operations to be performed by the digital circuit, each one of the set of operations having at least one functional element; identifying a first subset of a plurality of the at least one functional element; describing in a description the plurality of the at least one functional element of the identified first subset in terms of properties, each one of the properties having an assumption component and a proof component; formally verifying each one of the properties; arranging the plurality of the at least one functional element of the identified first subset to be proven for the digital circuit in an arrangement with temporal relations satisfying at least said description; analysing completeness of the arrangement of the plurality of the at least one functional element to verify that the at least one aspects of the digital circuit are completely verified.

摘要翻译： 1。一种用于验证数字电路的至少一个方面的方法，所述方法包括：提供将由所述数字电路执行的一组操作，所述一组操作中的每一个具有至少一个功能元件; 识别多个所述至少一个功能元件的第一子集; 在描述中在特性方面描述所识别的第一子集的多个所述至少一个功能元件，所述特性中的每一个具有假设部件和证明部件; 正式验证每一个属性; 将所识别的第一子集的所述至少一个功能元件的所述多个功能元件布置成具有满足至少所述描述的时间关系的布置; 分析所述多个所述至少一个功能元件的布置的完整性以验证所述数字电路的所述至少一个方面被完全验证。

公开(公告)号：EP1933245A1

公开(公告)日：2008-06-18

申请号：EP06026768.9

申请日：2006-12-22

申请人： Onespin Solutions GmbH

发明人： Bormann, Jörg ,  Beyer, Sven ,  Skalberg, Sebastian

IPC分类号： G06F17/50

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

摘要： A method for formally verifying the equivalence of an architecture description with an implementation description is disclosed. The method comprises:
- reading an implementation description;
- reading an architecture description;
- demonstrating that during execution of a same program with same initial values an architecture sequence of data transfers described by the architecture description is mappable to an implementation sequence of data transfers implemented by the implementation description, such that the mapping is bijective and ensures that the temporal order of the architecture sequence of data transfers corresponds to the temporal order of the implementation sequence of data transfers;
- outputting a result of the verification of the equivalence of the architecture description with the implementation description.

摘要翻译： 公开了一种用于正式验证体系结构描述与实现描述的等价性的方法。 该方法包括： - 读取实现描述; - 阅读建筑描述; - 表明在执行具有相同初始值的相同程序期间，由架构描述描述的架构数据传输序列可映射到由实现描述实现的数据传输的实现序列，使得映射是双射的并且确保时间 数据传输的架构序列的顺序对应于数据传输的实现顺序的时间顺序; - 输出结构描述的等同性的验证结果与实现描述。

公开(公告)号：EP2088521B1

公开(公告)日：2010-12-15

申请号：EP08002479.7

申请日：2008-02-11

申请人： Onespin Solutions GmbH

发明人： Beyer, Sven ,  Schönherr, Jens ,  Bormann, Jörg

IPC分类号： G06F17/50

CPC分类号： G06F17/504