Using Sequence Diagrams to Specify and to Generate RTL Assertions

In the field of hardware development, it is essential to prove the correctness of a new design. In order to check a design, verification engineers often use assertions written in a property or hardware specification language. Sequence diagrams are well established in the field of software engineering and allow easy and compact specification of protocols. We propose to use sequence diagrams to specify register transfer level (RTL) behaviour and present an approach to automatically generate temporal properties out of these diagrams. The validity of the approach is illustrated by verifying a Wishbone system-on-a-chip (SoC) local interconnect bus.

Content

Author and article information

Contributors

Martin Schweikert

Tobias Dornes

Hans Eveking

Conference

Publication date: September 2011

Publication date (Print): September 2011

Pages: 1-11

Affiliations

[0001]Computer Systems Group

Technische Universität Darmstadt

Merckstr. 25

64283 Darmstadt

Germanywww.rs.tu-darmstadt.de

Article

DOI: 10.14236/ewic/VECOS2011.12

SO-VID: 5591c453-5fd3-48ce-9551-c410dc0a846c

Copyright statement: © Martin Schweikert et al. Published by BCS Learning and Development Ltd. Fifth International Workshop on Verification and Evaluation of Computer and Communication Systems (VECoS 2011), Tunis, Tunisia

License:

This work is licensed under a Creative Commons Attribution 4.0 Unported License. To view a copy of this license, visit http://creativecommons.org/licenses/by/4.0/

Conference name: Fifth International Workshop on Verification and Evaluation of Computer and Communication Systems (VECoS 2011)

Conference acronym: VECOS

Conference number: 5

Conference location: Tunis, Tunisia

Conference date: 15-16 September 2011

Conference sponsor: Electronic Workshops in Computing (eWiC)

Conference theme: Verification and Evaluation of Computer and Communication Systems (VECoS 2011)

Product

Product Information: 1477-9358BCS Learning & Development

Self URI (article page): https://www.scienceopen.com/hosted-document?doi=10.14236/ewic/VECOS2011.12

Self URI (journal page): https://ewic.bcs.org/

Using Sequence Diagrams to Specify and to Generate RTL Assertions

Abstract