Com'è noto, negli ultimi anni l'aumento della produttività dei progettisti reso possibile dal software Electronic Design Automation non è stato sufficiente per tenere il passo con la crescente complessità dei chip. Le ricerche degli analisti dimostrano infatti che tuttora circa due terzi dei nuovi progetti subisce ritardi rispetto alla tabella di marcia prefissata, una percentuale sostanzialmente identica a quella degli scorsi anni. Inoltre sono ancora rari i casi di “first time silicon success”: soltanto il 30% dei nuovi chip funziona al primo tentativo, per il restante 70% occorrono due o più correzioni (generalmente a causa di problemi di tipo funzionale o legati al clock) seguite da altrettanti prototipi in silicio. Queste difficoltà evidenziano l'insufficienza della principale tecnica di verifica dei progetti, la simulazione, che consiste nel costruire un modello software del chip per poi sottoporlo a stimoli corrispondenti ai vari casi di funzionamento reale. Oltre a richiedere molto tempo, infatti, la simulazione non può coprire tutti i possibili casi reali di funzionamento. Per cambiare questo stato di cose l'industria EDA ripone molte speranze nella verifica formale, una tecnica che consente di confermare la correttezza funzionale del progetto tramite dimostrazioni matematiche. Finora, però, le difficoltà poste da questa soluzione - in particolare la necessità di scrivere manualmente grandi quantità di “asserzioni” - ne hanno limitato l'uso a pochi esperti. Con il recente potenziamento della propria piattaforma “Questa”, Mentor Graphics si propone oggi di semplificare la verifica formale, rendendola così accessibile a tutti i progettisti. Le innovazioni riguardano le funzionalità di clock-domain crossing (Cdc) e l'aggiunta di due nuovi strumenti: Questa AutoCheck, per il controllo formale completamente automatizzato; e Questa CoverCheck, per l'analisi della copertura del codice (code coverage closure). Il potenziamento della piattaforma Questa è stato illustrato da Harry Foster, “chief scientist” di Mentor Graphics per le tecniche di verifica, nel corso di un incontro con la stampa tenutosi recentemente a Los Gatos, in California.
Analisi automatica dei “buchi” nella copertura
La tecnologia Questa CoverCheck consente di accelerare il processo di “code coverage closure”. Quest'attività - che, se svolta senza l'ausilio dell'automazione, può richiedere molte settimane di lavoro - consiste nell'esame dei “buchi” di copertura del codice, ossia dei casi di funzionamento del chip che non possono essere verificati tramite la normale simulazione. I casi non coperti devono infatti essere analizzati per determinare se sia possibile ignorarli senza rischi, o, in alternativa, per scrivere manualmente gli stimoli necessari a coprirli tramite simulazione. Il nuovo strumento facente parte della piattaforma Questa consente di automatizzare l'uso dei metodi formali per individuare e analizzare tutti i “buchi” di copertura, riducendo il tempo necessario per raggiungere il “code coverage sign-off”, cioè l'approvazione del codice dal punto di vista della copertura di verifica.
Verifica formale automatica
Lo strumento Questa AutoCheck analizza il progetto descritto in Rtl e sintetizza automaticamente le “asserzioni” (elementi essenziali per effettuare la verifica formale), le quali vengono successivamente elaborate da potenti engine formali per verificare la correttezza del comportamento sequenziale del futuro chip. In questo modo, automatizzando la verifica formale, Questa consente di verificare facilmente che il progetto sia privo dei più comuni errori funzionali, senza la necessità di scrivere un testbench di simulazione né le asserzioni. Diviene inoltre possibile utilizzare le tecniche formali per migliorare la qualità dei risultati e ridurre l'impiego di risorse di calcolo. La nuova versione della piattaforma comprende anche la funzionalità Questa Formal Multi-Core, che consente di distribuire le elaborazioni di verifica formale su diversi core del medesimo processore o su più computer, per ottimizzare l'uso delle risorse di calcolo.
Verifica del clock-domain crossing
La terza innovazione riguarda, come si è detto, la funzionalità di clock-domain crossing (Cdc), cioè l'individuazione di eventuali errori riguardanti la sincronizzazione tra blocchi del progetto che utilizzano segnali di clock diversi. Lo strumento Questa Cdc, già ampiamente utilizzato dai produttori di semiconduttori, è stato ora potenziato per tenere conto delle dimensioni crescenti dei System-on-Chip. Harry Foster ha concluso ricordando che la verifica formale è finalizzata a controllare la correttezza dei singoli blocchi funzionali; per verificare l'insieme di un chip composto da più blocchi occorrerà sempre utilizzare la simulazione. L'esperto di Mentor Graphics ha aggiunto che una maggiore diffusione della verifica formale potrà ridurre i ritardi che attualmente caratterizzano lo sviluppo dei nuovi chip.
