Skip to Content

WickedXmas: Designing and Verifying on-chip Communication Fabrics

Posted on

Authors:

  • Joosten, Sebastiaan J. C.
  • Verbeek, Freek
  • Schmaltz, Julien

Published in: International Workshop on Design and Implementation of Formal Tools and Systems (DIFTS)

Paper

Abstract:

In modern chip architectures, the increase in parallelisation brings about highly complex on-chip communication fabrics. We present WickedXmas, a tool that facilitates the design and formal verification of such interconnects. The tool is based on the language xMAS, which is a high level design language for communication fabrics, originally proposed by Intel. The use of xMAS ensures that many common modelling errors such as unintended loss of data or dangling wires are prevented by construction. Therefore, the major challenge in verifying xMAS models is establishing deadlock freedom. WickedXmas can automatically detect deadlocks or prove their absence. If a deadlock is found, it is presented to the user for further analysis. Experimental evaluation on a range of interconnects shows good performance and scalability of WickedXmas in contrast to verification from scratch, or using existing model checking techniques. Using WickedXmas, a user can draw a communication fabric and formally verify it automatically.

BibTeX entry:

@inproceedings{Joosten14b,
 abstract = {In modern chip architectures, the increase in parallelisation brings about highly complex on-chip communication fabrics. We present WickedXmas, a tool that facilitates the design and formal verification of such interconnects. The tool is based on the language xMAS, which is a high level design language for communication fabrics, originally proposed by Intel. The use of xMAS ensures that many common modelling errors such as unintended loss of data or dangling wires are prevented by construction. Therefore, the major challenge in verifying xMAS models is establishing deadlock freedom. WickedXmas can automatically detect deadlocks or prove their absence. If a deadlock is found, it is presented to the user for further analysis. Experimental evaluation on a range of interconnects shows good performance and scalability of WickedXmas in contrast to verification from scratch, or using existing model checking techniques. Using WickedXmas, a user can draw a communication fabric and formally verify it automatically.},
 author = {Joosten, Sebastiaan Jozef Christiaan and Verbeek, Freek and Schmaltz, Julien},
 booktitle = {International Workshop on Design and Implementation of Formal Tools and Systems (DIFTS)},
 day = {20},
 month = {Oct},
 title = {WickedXmas: Designing and Verifying on-chip Communication Fabrics},
 year = {2014}
}