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 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), della verifica basata su asserzioni (ABV) 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 insieme di prototipi 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 e verifica basate su TLM e ABV. La
metodologia proposta si svilupperà, quindi, in quattro attività strettamente correlate:
1. modellazione e verifica di automi ibridi a partire da specifiche definite tramite proprietà formali;
2. estrazione di vincoli funzionali e temporali da automi ibridi per la generazione semi-automatica di modelli SystemC TLM;
3. raffinamento e verifica dei modelli SystemC tramite asserzioni e generazione automatica di sequenze di test (necessarie per la verifica dinamica delle asserzioni);
4. applicazione dei modelli SystemC ottenuti dopo i passi precedenti e configurazione della piattaforma multiprocessore di riferimento.
La strategie di modellazione e verifica proposte saranno implementate in quattro prototipi: ARIADNE per la modellazione e verifica di automi ibridi, SEXTRACT per
la generazione semi-automatica di modelli SystemC TLM, MILEDI per il raffinamento dei modelli SystemC lungo tutti i livelli TLM, e MultiCover per la verifica
post-raffinamento.