发明公开
EP1933245A1 Equivalence verification between transaction level models and RTL examples of processors
审中-公开
Äquivalenzüberprüfungzwischen Transaktionsebenenmodellen und RTL-Beispielen von Prozessoren
- 专利标题： Equivalence verification between transaction level models and RTL examples of processors
- 专利标题（中）： Äquivalenzüberprüfungzwischen Transaktionsebenenmodellen und RTL-Beispielen von Prozessoren
-
申请号： EP06026768.9申请日： 2006-12-22
-
公开(公告)号： EP1933245A1公开(公告)日： 2008-06-18
- 发明人: Bormann, Jörg , Beyer, Sven , Skalberg, Sebastian
- 申请人： Onespin Solutions GmbH
- 申请人地址： Theresienhöhe 12, Haus A 80339 München DE
- 专利权人： Onespin Solutions GmbH
- 当前专利权人： Onespin Solutions GmbH
- 当前专利权人地址： Theresienhöhe 12, Haus A 80339 München DE
- 代理机构： Harrison, Robert John
- 优先权： EP06026062 20061215
- 主分类号： G06F17/50
- IPC分类号： G06F17/50
摘要：
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.
- 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.
信息查询
