Text size
  • Small
  • Medium
  • Large
Contrast
  • Standard
  • Blue text on blue
  • High contrast (Yellow text on black)
  • Blue text on beige

    Using Sequence Diagrams to Specify and to Generate RTL Assertions

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

    Tunis, Tunisia, 15-16 September 2011

    AUTHORS

    Martin Schweikert, Tobias Dornes and Hans Eveking

    ABSTRACT

    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.

    PAPER FORMATS

    PDF filePDF Version of this Paper (1,691kb)