A formalisation of XMAS

Bernard van Gastel
(Open University of the Netherlands)
Julien Schmaltz
(Open University of the Netherlands)

Communication fabrics play a key role in the correctness and performance of modern multi-core processors and systems-on-chip. To enable formal verification, a recent trend is to use high-level micro-architectural models to capture designers' intent about the communication and processing of messages. Intel proposed the xMAS language to support the formal definition of executable specifications of micro-architectures. We formalise the semantics of xMAS in ACL2. Our formalisation represents the computation of the values of all wires of a design. Our main function computes a set of possible routing targets for each message and whether a message can make progress according to the current network state. We prove several properties on the semantics, including termination, non-emptiness of routing, and correctness of progress conditions. Our current effort focuses on a basic subset of the entire xMAS language, which includes queues, functions, and switches.

In Ruben Gamboa and Jared Davis: Proceedings International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 2013), Laramie, Wyoming, USA , May 30-31, 2013, Electronic Proceedings in Theoretical Computer Science 114, pp. 111–126.
Published: 26th April 2013.

ArXived at: http://dx.doi.org/10.4204/EPTCS.114.9 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org