Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Theorem Proving Techniques for Formal Verification of NoC Communications with Non-minimal Adaptive Routing
KTH, School of Information and Communication Technology (ICT), Electronic Systems.
2010 (English)In: Proceedings of the 13th IEEE International Symposium on Design & Diagnostics of Electronic Circuits & Systems, 2010Conference paper, Published paper (Refereed)
Abstract [en]

This paper focuses on the formal verification of communications in Networks on Chip. We describe how an enhanced version of the GeNoC proof methodology has been applied to the Nostrum NoC which encompasses various non-trivial features such as a deflective non-minimal routing algorithm. We demonstrate how the features of the Nostrum protocol layers can be captured by the current version of GeNoC that enables a step-by-step formalization of communication operations while taking various protocol details into consideration. We prove that packets arrive properly and that packets are never lost. Also, we prove the soundness of the Nostrum data link, network and transport layers

Place, publisher, year, edition, pages
2010.
National Category
Electrical Engineering, Electronic Engineering, Information Engineering
Identifiers
URN: urn:nbn:se:kth:diva-63665DOI: 10.1109/DDECS.2010.5491781Scopus ID: 2-s2.0-77954918343OAI: oai:DiVA.org:kth-63665DiVA: diva2:482702
Conference
the 13th IEEE International Symposium on Design & Diagnostics of Electronic Circuits & Systems
Note
Key: Nostrum. QC 20120126Available from: 2012-01-24 Created: 2012-01-24 Last updated: 2012-01-26Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full textScopushttp://web.it.kth.se/~axel/papers/2010/DDECS-NostrumVerification.pdf

Search in DiVA

By author/editor
Jantsch, Axel
By organisation
Electronic Systems
Electrical Engineering, Electronic Engineering, Information Engineering

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 14 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf