WickedXmas: a tool for deadlock detection

We have developed WickedXmas, a tool to design and verify xMAS networks. The xMAS language is used by Intel and various academia for modelling on-chip communication fabrics.

The complete tool, including deadlock detection and invariant generation, can be downloaded here. For now, it requires Windows and the Z3 SMT solver. Installation instructions can be found in the zip-file.

The name ``WickedXMAS'' is  based on the original  developers of the graphical interface of the tool: Willem Burgers, Christiaan Thijssen and Kevin Reintjes.  They have built this tool for a research project funded by Intel.

Examples

  • The two agents example of Intel ("Verifying deadlock-freedom of communication fabrics", Gotmanov et al., link) VMCAI'11, link) has been modelled in WickedXmas. For sake of demonstration, we have oversized the credit couting queues so that a deadlock occurs. The source files for the examples can be downloaded here.
  • We have modelled Figure 6 from the paper "Scalable progress verification in credit-based flow-control systems" (Ray and Brayton, DATE 2012, link). It concerns an advanced virtual channel where deadlock may occur when, e.g., queue B2 is sized incorrectly. The WickedXmas source file can be downloaded here.
  • A 2D mesh with message dependencies has been designed in WickedXmas. Source files can be downloaded here.

Screenshot