WickedXmas : designing and verifying on-chip communication fabrics

S.J.C. Joosten, F. Verbeek, J. Schmaltz

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

11 Citations (Scopus)
125 Downloads (Pure)

Abstract

In modern chip architectures, the increase in parallelization 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. Keywords: Communication Fabrics, Deadlock Detection, Formal Verification Tools
Original languageEnglish
Title of host publicationProceedings of the 3rd International Workshop on Design and Implementation of Formal Tools and Systems (DIFTS'14, Lausanne, Switzerland, October 20, 2014)
Pages1-8
Publication statusPublished - 2014
Eventconference; International Workshop on Design and Implementation of Formal Tools and Systems; 2014-10-20; 2014-10-20 -
Duration: 20 Oct 201420 Oct 2014

Conference

Conferenceconference; International Workshop on Design and Implementation of Formal Tools and Systems; 2014-10-20; 2014-10-20
Period20/10/1420/10/14
OtherInternational Workshop on Design and Implementation of Formal Tools and Systems

Fingerprint Dive into the research topics of 'WickedXmas : designing and verifying on-chip communication fabrics'. Together they form a unique fingerprint.

Cite this