A formalisation of XMAS
Bernard van Gastel (Open University of the Netherlands), Julien, Schmaltz (Open University of the Netherlands)

TL;DR
This paper formalizes the semantics of the xMAS language in ACL2, enabling rigorous verification of communication fabrics in multi-core processors by modeling message routing and progress.
Contribution
It provides a formal ACL2 semantics for a subset of xMAS, including proofs of key properties like termination and correctness of message progress.
Findings
Formal semantics of xMAS in ACL2 established
Proved properties such as termination and progress correctness
Focus on a subset including queues, functions, and switches
Abstract
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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsEmbedded Systems Design Techniques · Interconnection Networks and Systems · Formal Methods in Verification
