Inference of channel types in micro-architectural models of on-chip communication networks

B. Gastel, van; F. Verbeek; J. Schmaltz

doi:10.1109/VLSI-SoC.2014.7004168

Inference of channel types in micro-architectural models of on-chip communication networks

B. Gastel, van
, F. Verbeek
, J. Schmaltz

Formal System Analysis

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

Abstract

In the multi-core era, on-chip communication networks are key to system correctness and performance. To deal with their growing complexity, micro-architectural models capture the intent of architects and provide means for formal analysis. However, the analysis of such micro-architectural models is restricted to non-scalable and/or very specific approaches. We present a novel scalable approach to support the symbolic channel type inference of large micro-architectural models described in the xMAS language proposed by Intel. We define an algorithm that computes all possible messages that can occur in a communication channel, treating their payload symbolically. These results can be used for further analysis such as verifying absence of misrouting, deriving inductive invariants and deadlock detection. We illustrate our approach on a Spidergon network developed at STMicroelectronics.

Original language	English
Title of host publication	22nd IFIP/IEEE International Conference on Very Large Scale Integration (VLSI-SOC'14, Playa del Carmen, Mexico, October 6-8, 2014)
Editors	L. Garcia
Publisher	Institute of Electrical and Electronics Engineers
Pages	1-6
ISBN (Print)	978-1-4799-6016-3
DOIs	https://doi.org/10.1109/VLSI-SoC.2014.7004168
Publication status	Published - 2014
Event	22nd IFIP/IEEE International Conference on Very Large Scale Integration; 2014-10-06; 2014-10-08 - Duration: 6 Oct 2014 → 8 Oct 2014

Conference

Conference	22nd IFIP/IEEE International Conference on Very Large Scale Integration; 2014-10-06; 2014-10-08
Period	6/10/14 → 8/10/14
Other	22nd IFIP/IEEE International Conference on Very Large Scale Integration

Access to Document

10.1109/VLSI-SoC.2014.7004168

Cite this

Gastel, van, B., Verbeek, F., & Schmaltz, J. (2014). Inference of channel types in micro-architectural models of on-chip communication networks. In L. Garcia (Ed.), 22nd IFIP/IEEE International Conference on Very Large Scale Integration (VLSI-SOC'14, Playa del Carmen, Mexico, October 6-8, 2014) (pp. 1-6). Institute of Electrical and Electronics Engineers. https://doi.org/10.1109/VLSI-SoC.2014.7004168

@inproceedings{a7a1292d00a647f68ef49442a586c0d9,

title = "Inference of channel types in micro-architectural models of on-chip communication networks",

abstract = "In the multi-core era, on-chip communication networks are key to system correctness and performance. To deal with their growing complexity, micro-architectural models capture the intent of architects and provide means for formal analysis. However, the analysis of such micro-architectural models is restricted to non-scalable and/or very specific approaches. We present a novel scalable approach to support the symbolic channel type inference of large micro-architectural models described in the xMAS language proposed by Intel. We define an algorithm that computes all possible messages that can occur in a communication channel, treating their payload symbolically. These results can be used for further analysis such as verifying absence of misrouting, deriving inductive invariants and deadlock detection. We illustrate our approach on a Spidergon network developed at STMicroelectronics.",

author = "\{Gastel, van\}, B. and F. Verbeek and J. Schmaltz",

year = "2014",

doi = "10.1109/VLSI-SoC.2014.7004168",

language = "English",

isbn = "978-1-4799-6016-3",

pages = "1--6",

editor = "L. Garcia",

booktitle = "22nd IFIP/IEEE International Conference on Very Large Scale Integration (VLSI-SOC'14, Playa del Carmen, Mexico, October 6-8, 2014)",

publisher = "Institute of Electrical and Electronics Engineers",

address = "United States",

note = "22nd IFIP/IEEE International Conference on Very Large Scale Integration; 2014-10-06; 2014-10-08 ; Conference date: 06-10-2014 Through 08-10-2014",

}

Gastel, van, B, Verbeek, F & Schmaltz, J 2014, Inference of channel types in micro-architectural models of on-chip communication networks. in L Garcia (ed.), 22nd IFIP/IEEE International Conference on Very Large Scale Integration (VLSI-SOC'14, Playa del Carmen, Mexico, October 6-8, 2014). Institute of Electrical and Electronics Engineers, pp. 1-6, 22nd IFIP/IEEE International Conference on Very Large Scale Integration; 2014-10-06; 2014-10-08, 6/10/14. https://doi.org/10.1109/VLSI-SoC.2014.7004168

Inference of channel types in micro-architectural models of on-chip communication networks. / Gastel, van, B.; Verbeek, F.; Schmaltz, J.
22nd IFIP/IEEE International Conference on Very Large Scale Integration (VLSI-SOC'14, Playa del Carmen, Mexico, October 6-8, 2014). ed. / L. Garcia. Institute of Electrical and Electronics Engineers, 2014. p. 1-6.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Inference of channel types in micro-architectural models of on-chip communication networks

AU - Gastel, van, B.

AU - Verbeek, F.

AU - Schmaltz, J.

PY - 2014

Y1 - 2014

N2 - In the multi-core era, on-chip communication networks are key to system correctness and performance. To deal with their growing complexity, micro-architectural models capture the intent of architects and provide means for formal analysis. However, the analysis of such micro-architectural models is restricted to non-scalable and/or very specific approaches. We present a novel scalable approach to support the symbolic channel type inference of large micro-architectural models described in the xMAS language proposed by Intel. We define an algorithm that computes all possible messages that can occur in a communication channel, treating their payload symbolically. These results can be used for further analysis such as verifying absence of misrouting, deriving inductive invariants and deadlock detection. We illustrate our approach on a Spidergon network developed at STMicroelectronics.

AB - In the multi-core era, on-chip communication networks are key to system correctness and performance. To deal with their growing complexity, micro-architectural models capture the intent of architects and provide means for formal analysis. However, the analysis of such micro-architectural models is restricted to non-scalable and/or very specific approaches. We present a novel scalable approach to support the symbolic channel type inference of large micro-architectural models described in the xMAS language proposed by Intel. We define an algorithm that computes all possible messages that can occur in a communication channel, treating their payload symbolically. These results can be used for further analysis such as verifying absence of misrouting, deriving inductive invariants and deadlock detection. We illustrate our approach on a Spidergon network developed at STMicroelectronics.

U2 - 10.1109/VLSI-SoC.2014.7004168

DO - 10.1109/VLSI-SoC.2014.7004168

M3 - Conference contribution

SN - 978-1-4799-6016-3

SP - 1

EP - 6

BT - 22nd IFIP/IEEE International Conference on Very Large Scale Integration (VLSI-SOC'14, Playa del Carmen, Mexico, October 6-8, 2014)

A2 - Garcia, L.

PB - Institute of Electrical and Electronics Engineers

T2 - 22nd IFIP/IEEE International Conference on Very Large Scale Integration; 2014-10-06; 2014-10-08

Y2 - 6 October 2014 through 8 October 2014

ER -

Gastel, van B, Verbeek F, Schmaltz J. Inference of channel types in micro-architectural models of on-chip communication networks. In Garcia L, editor, 22nd IFIP/IEEE International Conference on Very Large Scale Integration (VLSI-SOC'14, Playa del Carmen, Mexico, October 6-8, 2014). Institute of Electrical and Electronics Engineers. 2014. p. 1-6 doi: 10.1109/VLSI-SoC.2014.7004168

Inference of channel types in micro-architectural models of on-chip communication networks

Abstract

Conference

Access to Document

Fingerprint

Cite this