Modellazione e verifica di sistemi embedded ibridi per piattaforme multiprocessore (PRIN 2008)

Data inizio
27 gennaio 2010
Durata (mesi) 
24
Dipartimenti
Informatica, Ingegneria per la medicina di innovazione
Responsabili (o referenti locali)
Fummi Franco

La modellazione e la verifica di piattaforme embedded multiprocessore sono problematiche strettamente legate che vengono ancora gestite con metodologie e linguaggi non correlati. Inoltre, le tradizionali tecniche di modellazione a livello RT, che fino a qualche anno fa permettevano di gestire agevolmente la progettazione di sistemi digitali, non sono più adatte per le moderne piattaforme embedded. Infatti, la complessità di tali piattaforme, costituite da una rete di parti HW e SW interagenti, sta crescendo molto velocemente, in modo particolare per i sistemi ibridi, in cui sono coinvolti sia componenti continue (ad esempio, per analizzare problematiche legate al consumo di potenza) che discrete.
In tale contesto, appare pertanto evidente che le attuali metodologie di sviluppo soffrono, da un lato la mancanza di continuità tra i livelli di astrazione, e dall'altro lo
scarso riutilizzo delle strategie di verifica tra i livelli stessi. L'introduzione della modellazione a livello transazionale (TLM) e di linguaggi di descrizione a livello di sistema quali, ad esempio, SystemC e SystemVerilog, mira al superamento di tali problemi e permette una maggior omogeneità tra modellazione e verifica a tutti i
livelli di astrazione fino al livello RT compreso. Tuttavia, la specifica iniziale di un sistema embedded ibrido necessità di un formalismo ad hoc per la gestione delle componenti continue e discrete del sistema, che è difficile da ottenere usando linguaggi come SystemC o SystemVerilog. In tale ambito, l'utilizzo degli automi ibridi garantisce un implementazione semplice ed efficiente della doppia natura (discreta e continua) di un sistema ibrido.
Pertanto, l'obiettivo di questa unità di ricerca consiste nello sviluppo di una metodologia e di un ambiente di cosimulazione per la modellazione e verifica di sistemi embedded ibridi per piattaforme multiprocessore che sfrutti sia la teoria degli automi ibridi, che le tecniche di modellazione basate su TLM, che le strategie di cosimulazione HW/SW. La metodologia proposta si svilupperà, quindi, in tre attività strettamente correlate:
1. modellazione e verifica di automi ibridi a partire da specifiche definite tramite proprietà formali;
2. generazione semi-automatica e raffinamento di modelli SystemC/C per le componenti HW/SW a partire dai corrispondenti automi ibridi;
3. definizione di un ambiente di cosimulazione HW/SW e configurazione della piattaforma multiprocessore di riferimento per garantire una adeguata verifica del sistema completo.
La strategie di modellazione e verifica proposte saranno implementate in tre prototipi: ARIADNE per la modellazione e verifica di automi ibridi, SEXTRACT per la generazione semi-automatica di modelli HW/SW SystemC/C e HSN per la co-simulazione di sistemi HW/SW.

Enti finanziatori:

PRIN VALUTATO POSITIVAMENTE
Finanziamento: richiesto
Programma: COFIN - Progetti di Ricerca di Interesse Nazionale

Partecipanti al progetto

Franco Fummi
Professore ordinario
Graziano Pravadelli
Professore ordinario
Tiziano Villa
Professore onorario

Attività

Strutture

Condividi