kth.sePublikationer
Ändra sökning
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
Theorem Proving Techniques for Formal Verification of NoC Communications with Non-minimal Adaptive Routing
KTH, Skolan för informations- och kommunikationsteknik (ICT), Elektroniksystem.ORCID-id: 0000-0003-2251-0004
2010 (Engelska)Ingår i: Proceedings of the 13th IEEE International Symposium on Design & Diagnostics of Electronic Circuits & Systems, 2010Konferensbidrag, Publicerat paper (Refereegranskat)
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

Ort, förlag, år, upplaga, sidor
2010.
Nationell ämneskategori
Elektroteknik och elektronik
Identifikatorer
URN: urn:nbn:se:kth:diva-63665DOI: 10.1109/DDECS.2010.5491781ISI: 000411363000056Scopus ID: 2-s2.0-77954918343OAI: oai:DiVA.org:kth-63665DiVA, id: diva2:482702
Konferens
the 13th IEEE International Symposium on Design & Diagnostics of Electronic Circuits & Systems
Anmärkning

Key: Nostrum. QC 20120126

Tillgänglig från: 2012-01-24 Skapad: 2012-01-24 Senast uppdaterad: 2024-03-15Bibliografiskt granskad

Open Access i DiVA

Fulltext saknas i DiVA

Övriga länkar

Förlagets fulltextScopushttp://web.it.kth.se/~axel/papers/2010/DDECS-NostrumVerification.pdf

Person

Jantsch, Axel

Sök vidare i DiVA

Av författaren/redaktören
Jantsch, Axel
Av organisationen
Elektroniksystem
Elektroteknik och elektronik

Sök vidare utanför DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetricpoäng

doi
urn-nbn
Totalt: 30 träffar
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf