A formalisation of XMAS
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 mess...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2013-04-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1304.7862v1 |
| _version_ | 1828286346234429440 |
|---|---|
| author | Bernard van Gastel Julien Schmaltz |
| author_facet | Bernard van Gastel Julien Schmaltz |
| author_sort | Bernard van Gastel |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-13T09:30:51Z |
| format | Article |
| id | doaj.art-26aec09b266a444f84b605f21bf89b9f |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-04-13T09:30:51Z |
| publishDate | 2013-04-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-26aec09b266a444f84b605f21bf89b9f2022-12-22T02:52:15ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802013-04-01114Proc. ACL2 201311112610.4204/EPTCS.114.9A formalisation of XMASBernard van GastelJulien SchmaltzCommunication 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.http://arxiv.org/pdf/1304.7862v1 |
| spellingShingle | Bernard van Gastel Julien Schmaltz A formalisation of XMAS Electronic Proceedings in Theoretical Computer Science |
| title | A formalisation of XMAS |
| title_full | A formalisation of XMAS |
| title_fullStr | A formalisation of XMAS |
| title_full_unstemmed | A formalisation of XMAS |
| title_short | A formalisation of XMAS |
| title_sort | formalisation of xmas |
| url | http://arxiv.org/pdf/1304.7862v1 |
| work_keys_str_mv | AT bernardvangastel aformalisationofxmas AT julienschmaltz aformalisationofxmas AT bernardvangastel formalisationofxmas AT julienschmaltz formalisationofxmas |