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.
