Text size
  • Small
  • Medium
  • Large
  • 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


    Martin Schweikert, Tobias Dornes and Hans Eveking


    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.


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