article

Free access

A formal approach to the verification of networks on chip

Authors:

Dominique Borrione,

Laurence Pierre,

Julien SchmaltzAuthors Info & Claims

EURASIP Journal on Embedded Systems, Volume 2009

Article No.: 2, Pages 1 - 14

https://doi.org/10.1155/2009/548324

Published: 01 January 2009 Publication History

Abstract

The current technology allows the integration on a single die of complex systems-on-chip (SoCs) that are composed of manufactured blocks (IPs), interconnected through specialized networks on chip (NoCs). IPs have usually been validated by diverse techniques (simulation, test, formal verification) and the key problem remains the validation of the communication infrastructure. This paper addresses the formal verification of NoCs by means of a mechanized proof tool, the ACL2 theorem prover. A metamodel for NoCs has been developed and implemented in ACL2. This metamodel satisfies a generic correctness statement. Its verification for a particular NoC instance is reduced to discharging a set of proof obligations for each one of the NoC constituents. The methodology is demonstrated on a realistic and state-of-the-art design, the Spidergon network from STMicroelectronics.

References

[1]

L. Benini and G. De Micheli, "Networks on chips: a new SoC paradigm," Computer, vol. 35, no. 1, pp. 70-78, 2002.

Digital Library

[2]

P. P. Pande, C. Grecu, A. Ivanov, R. Saleh, and G. De Micheli, "Design, synthesis, and test of networks on chips," IEEE Design and Test of Computers, vol. 22, no. 5, pp. 404-413, 2005.

Digital Library

[3]

F. Clermidy, D. Varreau, and D. Lattard, "A NoC-based communication framework for seamless IP integration in complex systems," in Proceedings of the International Workshop on IP-Based System-on-Chip Design (IPSoC '05), Grenoble, France, December 2005.

[4]

D. Wiklund and D. Liu, "SoCBUS: switched network on chip for hard real time embedded systems," in Proceedings of the 17th International Parallel and Distributed Processing Symposium (IPDPS '03), pp. 78-85, Nice, France, April 2003.

[5]

A. Sangiovanni-Vincentelli, "Defining platform-based design," EEDesign of EETimes, February 2002.

[6]

R. Dubey, "Elements of verification," SOCcentral, March 2005.

[7]

J. Schmaltz and D. Borrione, "A functional formalization of on chip communications," Formal Aspects of Computing, vol. 20, no. 3, pp. 241-258, 2008.

[8]

D. Borrione, A. Helmy, L. Pierre, and J. Schmaltz, "A generic model for formally verifying NoC communication architectures: a case study," in Proceedings of the 1st International Symposium on Networks-on-Chip (NOCS '07), pp. 127-136, Princeton, NJ, USA, May 2007.

Digital Library

[9]

M. Kaufmann, P. Manolios, and J. Strother Moore, Computer Aided Reasoning: An Approach, Kluwer Academic Publishers, Dordrecht, The Netherlands, 2002.

Digital Library

[10]

M. Coppola, R. Locatelli, G. Maruccia, L. Pieralisi, and A. Scandurra, "Spidergon: a novel on-chip communication network," in Proceedings of the International Symposium on System-on-Chip, pp. 1-15, Tampere, Finland, November 2004.

[11]

J. S. Chenard, S. Bourduas, N. Azuelos, M. Boulé, and Z. Zilic, "Hardware assertion checkers in online detection of network-on-chip faults," in Proceedings of the Workshop on Diagnostic Services in Networks-on-Chips, Nice, France, April 2007.

[12]

IEEE Std 1850-2005, "IEEE Standard for Property Specification Language (PSL)," IEEE, 2005.

[13]

K. Goossens, B. Vermeulen, R. van Steeden, and M. Bennebroek, "Transaction-based communication-centric debug," in Proceedings of the 1st International Symposium on Networks-on-Chip (NOCS '07), pp. 95-106, Princeton, NJ, USA, May 2007.

Digital Library

[14]

E. M. Clarke, O. Grumberg, and S. Jha, "Verifying parameterized networks," ACM Transactions on Programming Languages and Systems, vol. 19, no. 5, pp. 726-750, 1997.

Digital Library

[15]

S. Creese and A. Roscoe, "Formal verification of arbitrary network topologies," in Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications (PDPTA '99), vol. 2, pp. 1033-1039, Las Vegas, Nev, USA, June-July 1999.

[16]

K. L. McMillan, Symbolic Model Checking, Kluwer Academic Press, Dordrecht, The Netherlands, 1993.

Digital Library

[17]

A. Roychoudhury, T. Mitra, and S. R. Karri, "Using formal techniques to debug the AMBA system-on-chip bus protocol," in Proceedings of the Conference on Design, Automation and Test in Europe (DATE '03), pp. 828-833, Munich, Germany, March 2003.

[18]

G. Salaün, W. Serwe, Y. Thonnart, and P. Vivet, "Formal verification of CHP specifications with CADP illustration on an asynchronous network-on-chip," in Proceedings of the 13th IEEE International Symposium on Asynchronous Circuits and Systems (ASYNC '07), pp. 73-82, Berkeley, Calif, USA, March 2007.

Digital Library

[19]

M. Gordon and T. Melham, Introduction to HOL: A Theorem Proving Environment for Higher Order Logic, Cambridge University Press, Cambridge, UK, 1993.

Digital Library

[20]

P. Curzon, "Experiences formally verifying a network component," in Proceedings of the 9th Annual Conference on Computer Assurance (COMPASS '94), pp. 183-193, IEEE Press, Gaithersburg, Md, USA, June 1994.

[21]

R. Bharadwaj, A. Felty, and F. Stomp, "Formalizing inductive proofs of network algorithms," in Proceedings of the Asian Computing Science Conference on Algorithms, Concurrency and Knowledge (ACSC '95), pp. 335-349, Pathumthani, Thailand, December 1995.

[22]

Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development--Coq'Art: The Calculus of Inductive Constructions, Springer, Berlin, Germany, 2004.

[23]

G. J. Holzmann, "The model checker SPIN," IEEE Transactions on Software Engineering, vol. 23, no. 5, pp. 279-295, 1997.

Digital Library

[24]

H. Amjad, "Model checking the AMBA protocol in HOL," Tech. Rep., Computer Laboratory, University of Cambridge, Cambridge, UK, September 2004.

[25]

B. Gebremichael, F. W. Vaandrager, M. Zhang, K. Goossens, E. Rijpkema, and A. Radulescu, "Deadlock prevention in the Æthereal protocol," in Proceedings of the 13th IFIP WG 10.5 Advanced Research Working Conference Correct Hardware Design and Verification Methods (CHARME '05), pp. 345-348, Saarbrücken, Germany, October 2005.

Digital Library

[26]

J. Strother Moore, "A formal model of asynchronous communication and its use in mechanically verifying a biphase mark protocol," Formal Aspects of Computing, vol. 6, no. 1, pp. 60-91, 1994.

[27]

R. S. Boyer and J. Strother Moore, A Computation Logic Handbook, Academic Press, New York, NY, USA, 1988.

[28]

D. Herzberg and M. Broy, "Modeling layered distributed communication systems," Formal Aspects of Computing, vol. 17, no. 1, pp. 1-18, 2005.

[29]

J. Rushby, "Systematic formal verification for fault-tolerant time-triggered algorithms," IEEE Transactions on Software Engineering, vol. 25, no. 5, pp. 651-660, 1999.

Digital Library

[30]

L. Pike, "A note on inconsistent axioms in Rushby's "systematic formal verification for fault-tolerant time-triggered algorithms" IEEE Transactions on Software Engineering, vol. 32, no. 5, pp. 347-348, 2006.

Digital Library

[31]

L. Pike, "Modeling time-triggered protocols and verifying their real-time schedules," in Proceedings of Formal Methods in Computer Aided Design (FMCAD '07), pp. 231-238, Austin, Tex, USA, November 2007.

Digital Library

[32]

P. S. Miner, A. Geser, L. Pike, and J. Maddalon, "A unified fault-tolerance protocol," in Proceedings of the Joint International Conferences on FormalModeling and Analysis of Timed Systmes and Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT '04), Y. Lakhnech and S. Yovine, Eds., vol. 3253 of Lecture Notes in Computer Science, pp. 167-182, Springer, Grenoble, France, September 2004.

[33]

F. Karim, A. Nguyen, and S. Dey, "An interconnect architecture for networking systems on chips," IEEE Micro, vol. 22, no. 5, pp. 36-45, 2002.

Digital Library

[34]

A. Jantsch, "Models of computation for networks on chip," in Proceedings of the 6th International Conference on Application of Concurrency to System Design (ACSD '06), pp. 165-176, IEEE Computer Society, Turku, Finland, June 2006.

Digital Library

[35]

A. Tanenbaum, Computer Networks, Prentice-Hall, Englewood Cliffs, NJ, USA, 2002.

Digital Library

[36]

W. Dally and B. Towles, Principles and Practices of Interconnection Networks, Morgan Kaufmann, San Francisco, Calif, USA, 2003.

Digital Library

[37]

F. Moraes, N. Calazans, A. Mello, L. Möller, and L. Ost, "HERMES: an infrastructure for low area overhead packet-switching networks on chip," Integration, the VLSI Journal, vol. 38, no. 1, pp. 69-93, 2004.

Digital Library

Cited By

(2018)An improved fault-tolerant routing algorithm for a Network-on-Chip derived with formal analysisScience of Computer Programming10.1016/j.scico.2016.01.002118:C(24-39)Online publication date: 31-Dec-2018
https://dl.acm.org/doi/10.1016/j.scico.2016.01.002
Verbeek FSchmaltz J(2012)Easy Formal Specification and Validation of Unbounded Networks-on-Chips ArchitecturesACM Transactions on Design Automation of Electronic Systems10.1145/2071356.207135717:1(1-28)Online publication date: 1-Jan-2012
https://dl.acm.org/doi/10.1145/2071356.2071357
Kamali MPetre LSere KDaneshtalab M(2011)Refinement-Based modeling of 3d nocsProceedings of the 4th IPM international conference on Fundamentals of Software Engineering10.1007/978-3-642-29320-7_16(236-252)Online publication date: 20-Apr-2011
https://dl.acm.org/doi/10.1007/978-3-642-29320-7_16
Show More Cited By

Index Terms

A formal approach to the verification of networks on chip
1. Hardware

Recommendations

Application of Formal Methods for System-Level Verification of Network on Chip
ISVLSI '11: Proceedings of the 2011 IEEE Computer Society Annual Symposium on VLSI

Network on chip (NoC) is a system design methodology that uses on-chip routers for integrating the resources on a system on chip (SoC). Applications on the SoC communicate through a layered communication protocol implemented on the NoC's router-based ...
Flattened Butterfly Topology for On-Chip Networks

With the trend towards increasing number of cores in a multicore processors, the on-chip network that connects the cores needs to scale efficiently. In this work, we propose the use of high-radix networks in on-chip networks and describe how the ...
Triplet-based topology for on-chip networks

Most CMPs use on-chip network to connect cores and tend to integrate more simple cores on a single die. As the number of cores increases, on-chip network will play an important role in the performance of future CMPs. Due to the tradeoff between the ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image EURASIP Journal on Embedded Systems

EURASIP Journal on Embedded Systems Volume 2009, Issue

January 2009

124 pages

ISSN:1687-3955

EISSN:1687-3963

Issue’s Table of Contents

Publisher

Hindawi Limited

London, United Kingdom

Publication History

Accepted: 04 February 2009

Published: 01 January 2009

Received: 01 August 2008

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

4
Total Citations
View Citations
168
Total Downloads

Downloads (Last 12 months)24
Downloads (Last 6 weeks)8

Reflects downloads up to 09 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

(2018)An improved fault-tolerant routing algorithm for a Network-on-Chip derived with formal analysisScience of Computer Programming10.1016/j.scico.2016.01.002118:C(24-39)Online publication date: 31-Dec-2018
https://dl.acm.org/doi/10.1016/j.scico.2016.01.002
Verbeek FSchmaltz J(2012)Easy Formal Specification and Validation of Unbounded Networks-on-Chips ArchitecturesACM Transactions on Design Automation of Electronic Systems10.1145/2071356.207135717:1(1-28)Online publication date: 1-Jan-2012
https://dl.acm.org/doi/10.1145/2071356.2071357
Kamali MPetre LSere KDaneshtalab M(2011)Refinement-Based modeling of 3d nocsProceedings of the 4th IPM international conference on Fundamentals of Software Engineering10.1007/978-3-642-29320-7_16(236-252)Online publication date: 20-Apr-2011
https://dl.acm.org/doi/10.1007/978-3-642-29320-7_16
Verbeek FSchmaltz JDe Micheli GAl-Hashimi BMueller WMacii E(2010)Formal specification of networks-on-chipsProceedings of the Conference on Design, Automation and Test in Europe10.5555/1870926.1871339(1701-1706)Online publication date: 8-Mar-2010
https://dl.acm.org/doi/10.5555/1870926.1871339

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Figures

Tables

Media

View Issue’s Table of Contents