Le insidie ​​del mescolare formale e simulazione: dove iniziano i problemi

Gli ambienti di verifica funzionale più efficaci utilizzano più tecnologie di analisi, in cui i punti di forza di ciascuno sono combinati per rafforzarsi a vicenda per garantire che il dispositivo sottoposto a test (DUT) si comporti come specificato. Tuttavia, questo crea una sfida intrinseca nel confrontare correttamente e combinare i risultati di ciascuna fonte per fornire un quadro succinto e accurato del vero stato dello sforzo di verifica.

Il problema più comune che vediamo è quando i progettisti vogliono unire i risultati dell’analisi formale con i risultati del codice RTL e della copertura funzionale dal loro banco di prova UVM, ma non comprendono appieno cosa sta fornendo la copertura formale. Quindi, inizieremo sul terreno familiare del codice generato dalla simulazione e della copertura funzionale prima di passare alla definizione della copertura formale.

Codice di simulazione e revisione della copertura funzionale

La copertura del codice è semplicemente la percentuale di codice RTL che misura il numero di istruzioni in un corpo di codice che è stato eseguito attraverso un’esecuzione di test. Sebbene sia importante che il testbench possa esercitare tutto il codice RTL, ad esempio, non c’è codice morto, il che implica un bug nel DUT, il design può ancora mancare di funzionalità importanti e/o i percorsi delle funzioni chiave possono essere in violazione della specifica.

La copertura funzionale dalla simulazione RTL è la metrica di quanta funzionalità di progettazione è stata esercitata, ad esempio, “coperta” dal banco di prova o dall’ambiente di verifica. L’importo della copertura funzionale che deve essere soddisfatta è esplicitamente definito dall’ingegnere della verifica sotto forma di un modello di copertura funzionale.

Nella sua forma di base, è una mappatura definita dall’utente di ciascuna caratteristica funzionale da testare a un punto di copertura e questi punti di copertura hanno determinate condizioni (gamme, transizioni o incroci definiti, ecc.) da soddisfare prima di essere segnalati come 100% coperto durante la simulazione. Tutte queste condizioni per un punto di copertura sono definite sotto forma di contenitori. È possibile acquisire un certo numero di punti di copertura in un gruppo di copertura e un insieme di più gruppi di copertura viene generalmente chiamato modello di copertura funzionale.

Durante la simulazione, quando vengono raggiunte determinate condizioni di un punto di copertura, tali bin (condizioni) vengono coperti e quindi il numero di bin colpiti fornisce una misurazione dell’avanzamento della verifica. Dopo aver eseguito una serie di test case, può essere generato un report grafico per analizzare il report di copertura funzionale e si possono fare piani per “coprire” i “buchi di verifica” creando nuovi test che attraverseranno le aree non ancora esercitate del DUT codice.

Si noti che è importante comprendere che il punteggio di copertura riflette anche la qualità del banco di prova, ad esempio se il banco di prova sta indirizzando tutti i circuiti DUT che è necessario verificare. Infatti, il punteggio di copertura e il numero di buche riflettono la qualità del piano di test di verifica e il suo allineamento con la specifica originale stessa.

Definizione della copertura formale

L’analisi formale fornisce i seguenti tipi di copertura non visti con la simulazione:

Raggiungibilità

Esiste una combinazione di segnali di ingresso che porterà lo stato del circuito a un nodo di importanza specificato? Se non ce ne sono, il punto è irraggiungibile. Quindi, questo fornisce informazioni simili sulla presenza di codice morto come fa la copertura del codice di simulazione.

Osservabilità

Quali sono tutti i possibili percorsi del circuito e dello spazio degli stati da un nodo selezionato ai segnali specificati in un’asserzione? E questi sono i percorsi previsti e soddisfano le specifiche del progetto?

Cono strutturale di influenza (COI)

Lavorando avanti o indietro da un punto selezionato del circuito, qual è tutta la logica che potrebbe influenzare questo nodo? Si tratta di una forma approssimativa di copertura e generalmente non utile per l’analisi di approvazione finale.

Copertura della mutazione basata sul modello

Misura la copertura di un progetto da parte dei correttori inserendo elettronicamente le mutazioni nel modello (il codice sorgente stesso non viene alterato) e controllando se un controllore o un’asserzione lo rileva. La copertura delle mutazioni fornisce indicazioni chiare su dove sono necessarie più asserzioni e rappresenta una metrica più forte rispetto a qualsiasi altro tipo di copertura poiché misura il rilevamento degli errori, non solo l’esercizio della progettazione.

Sebbene queste misurazioni siano fondamentalmente diverse dalla copertura della simulazione, l’applicazione complessiva è la stessa ad alto livello: misurare i progressi e valutare contemporaneamente la qualità del banco di prova formale (composto da vincoli e proprietà di verifica funzionale).

Dove iniziano i guai

La richiesta più comune del progettista è quella di “unire” la simulazione e le metriche di copertura generate formalmente corrispondenti a ciascun punto di copertura specificato; dove spesso l’obiettivo è consentire ai team di verifica di selezionare formali o simulazioni per verificare esclusivamente un sottoinsieme di un progetto. Ad esempio, immagina che un determinato IP contenga un elemento di progettazione che si adatta molto bene all’analisi formale (un arbitro è un esempio) e il resto del progetto potrebbe essere facilmente verificato da entrambe le tecnologie.

Naturalmente, i progettisti vogliono consentire al formale di “prendersi il merito” per la verifica dell’arbitro e unirla perfettamente ai risultati della simulazione sul resto del circuito. È qui che possono iniziare i guai. I maggiori rischi di cui essere consapevoli sono:

• Innanzitutto, indipendentemente dalla tecnologia scelta, solo perché qualcosa è coperto non significa che sia adeguatamente verificato. Ancora una volta, considera la relazione tra copertura del codice e copertura funzionale: solo perché i test possono attraversare il 100% del codice non significa che il codice sia anche funzionalmente corretto.
• La copertura della simulazione riflette solo percorsi in avanti specifici che la simulazione ha attraversato dagli ingressi attraverso lo spazio degli stati per un insieme specifico di stimoli.
• Alcuni tipi di copertura formale riflettono un attraversamento in avanti, ma solo perché l’analisi formale potrebbe attraversare alcuni degli stessi stati di una simulazione, la logica trattata è solitamente maggiore. Inoltre, l’analisi formale ha uno stimolo di input fluttuante ed è valida per tutto il tempo.
• Altri tipi di copertura formale riportano come la logica e la segnalazione “lavorano all’indietro” da un’uscita.
• La simulazione viene eseguita a livello di cluster/system-on-chip (SoC), mentre quella formale viene in genere eseguita a livello di blocco. Pertanto, la copertura del codice rappresenta il test end-to-end rispetto a una funzione più localizzata. Il modo in cui sono stati generati i dati di copertura può andare perduta una volta che i risultati sono stati registrati nel database di copertura.

In conclusione: se non sei attento a comprendere le differenze tra copertura formale e simulazione, se unisci semplicemente i dati di copertura su una base di 1-1 riga/oggetto/punto, puoi concludere erroneamente che la qualità della tua verifica è superiore a quella davvero è. Ad esempio, potresti fuorviare te stesso e i tuoi manager dicendo che hai finito quando la realtà è che ci sono effettivamente aree non verificate del tuo codice e piano di test.

Nota dell’editore: È una serie in tre parti sulle insidie ​​di mescolare copertura formale e simulazione. La seconda parte di questa serie di articoli confronterà i risultati della simulazione e dell’affiancamento formale con esempi di codice RTL DUT progressivamente complessi.

Mark Eslinger è un ingegnere di prodotto nella divisione IC Verification Systems di Siemens EDA, dove è specializzato in metodi basati su asserzioni e verifica formale.

Joe Hupcey III è un product marketing manager per la linea di prodotti formali Design & Verification Technologies di Siemens EDA di applicazioni automatizzate e controllo avanzato delle proprietà.

Nicolae Tusinschi è un product manager per le soluzioni di verifica formale presso Siemens EDA.

Contenuto relativo