Fifth International Workshop on Verification and Evaluation of Computer and Communication Systems (VECoS 2011) (VECOS)
Verification and Evaluation of Computer and Communication Systems (VECoS 2011)
15-16 September 2011
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.