WickedXmas : designing and verifying on-chip communication fabrics
Sjc Sebastiaan Joosten, Freek Verbeek, Julien Schmaltz · TU/e Research Portal · 2014
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