Formal System Design (ForSyDe) aims to bring the design of multiprocessor systems-on-chip (MPSoCs) to a higher level of abstraction and bridge the abstraction gap by transformational design refinement. The current research is focused on a correct-by-construction design flow, which requires design space exploration including formal models of computation and timepredictable platforms. The latter is widely used for hard real-time systems. In order to make a platform time-predictable, all components, as well as inter-core communication, need to have the worst-case execution time (WCET) estimations and be easily analyzed. Time-division multiplexing (TDM) networks can precisely allocate network resources at each time point and further provide time-predictable guarantees. However, the application developer must take the time to understand the hardware and capabilities of a network-on-chip (NoC) in order to communicate between the cores. Moreover, a wide variety of communication libraries belonging to different platforms increase the learning cost. The Message Passing Interface (MPI) standard inspires this project. For time-predictable communication on TDM-based MPSoCs, a specification with communication primitives should also be necessary for either system designers or application developers. Compared with the MPI standard, this specification should be lighter because it only elaborates on timepredictable communication. Besides, platforms it applies to are limited to real-time NoCs using TDM, which the worst-case communication time (WCCT) could be calculated at an early stage of the design. In this project, we abstracted from concurrency and communication libraries of existing platforms and derived communication primitives to this specification. Two different communication modes, push-based and interactive, are summarized. Push-based communication composes of checking the direct memory access (DMA) status, pushing the message, and checking the receiving buffer. Interactive communication comprises sending, receiving, and acknowledging primitives, which are divided into blocking and non-blocking. In addition, this specification permits the user to calculate WCCT of transmitting a message from one processor to another if one knows the size of messages transmitted and hardware configuration by addingWCET of all communication operations running on a single processor and latency of the communication connection together. The calculation process is shown using an existing platform. 

Formell systemdesign (ForSyDe) syftar till att föra designen av multiprocessor system-on-chip (MPSoC) till en högre abstraktionsnivå och överbrygga abstraktionsgapet genom transformationell designförfining. Den aktuella forskningen är fokuserad på ett designflöde som är korrekt för konstruktion, vilket kräver utforskning av designutrymme inklusive formella beräkningsmodeller och tidsförutsägbara plattformar. Det senare används ofta för hårda realtidssystem. För att göra en plattform tidsförutsägbar måste alla komponenter, såväl som kommunikation mellan kärnor, ha de värsta tänkbara exekveringstiden (WCET) uppskattningar och vara lätta att analysera. Time-division multiplexing (TDM)-nätverk kan exakt allokera nätverksresurser vid varje tidpunkt och ytterligare ge tidsförutsägbara garantier. Applikationsutvecklaren måste dock ta sig tid att förstå hårdvaran och kapaciteten hos ett nätverk-på-chip (NoC) för att kunna kommunicera mellan kärnorna. Dessutom ökar ett brett utbud av kommunikationsbibliotek som tillhör olika plattformar inlärningskostnaden. Message Passing Interface (MPI)-standarden inspirerar detta projekt. För tidsförutsägbar kommunikation på TDM-baserade MPSoC:er bör en specifikation med kommunikationsprimitiver också vara nödvändig för antingen systemdesigners eller applikationsutvecklare. Jämfört med MPI-standarden borde denna specifikation vara lättare eftersom den bara utvecklar tidsförutsägbar kommunikation. Dessutom är plattformar som den gäller begränsade till realtids-NoCs som använder TDM, som den värsta kommunikationstiden (WCCT) skulle kunna beräknas i ett tidigt skede av designen. I detta projekt har vi abstraherat från samtidighets- och kommunikationsbibliotek för befintliga plattformar och härledda kommunikationsprimitiver till denna specifikation. Två olika kommunikationslägen, push-baserade och interaktiva, sammanfattas. Pushbaserad kommunikation består av att kontrollera DMA-statusen (Direct Memory Access), skicka meddelandet och kontrollera mottagningsbufferten. Interaktiv kommunikation innefattar att skicka, ta emot och bekräfta primitiver, som är uppdelade i blockerande och icke-blockerande. Dessutom tillåter denna specifikation användaren att beräkna WCCT för att sända ett meddelande från en processor till en annan om man känner till storleken på skickade meddelanden och hårdvarukonfigurationen genom att lägga till WCET för alla kommunikationsoperationer som körs på en enda processor och latens för kommunikationsanslutningen tillsammans . Beräkningsprocessen visas med en befintlig plattform.