WickedXmas: a tool for deadlock detectionWe
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
|
|