Il supporto della Open Verification Library nella verifica formale.

• 
• Tweet
• Pin It
• Condividi per email

Moduli di asserzione per la verifica funzionale

Ciascun modulo denominato anche monitor d’asserzione, è in grado di identificare specifiche condizioni ed avvisare l’utente per un evento inaspettato. La stesura dei moduli è fatta con una normale sintassi HDL. La libreria OVL contiene un gruppo di monitor d’asserzione che possono facilmente essere posizionati nei vari punti del progetto, anche internamente, per evidenziare istantaneamente le violazioni delle specifiche di funzionamento senza che esse si debbano propagare necessariamente ai punti circuitali d’uscita per la loro individuazione. La libreria OVL può essere facilmente scaricata dal web (http://www.verificationlib.org). L’attuale versione 1.1.0, è un set di 26 moduli. Altri moduli potranno essere aggiunti in un prossimo futuro anche con l’apporto d’ogni singolo utente. La libreria è, infatti, libera e ciascuno potrà aggiungere, aggiornare i moduli rendendo disponibile la propria esperienza a tutti senza vincoli di licenza. Ciascun modulo può inoltre essere usato come obiettivo di una prova formale o come restrizione. Uno dei principali benefici dei metodi sopra descritti è che le asserzioni sono immediatamente disponibili in tutti i simulatori standard HDL e non è richiesta nessuna particolare interfaccia proprietaria per estrarre le asserzioni OVL da un progetto RTL.

Uso di un’asserzione OVL in BlackTie

I modi operativi in BlackTie possono essere così descritti: durante il setup, l’utente definisce gli ingressi di clock, di reset e qualsiasi altra restrizione ambientale richiesta per definire un corretto funzionamento. Durante il setup viene altresì definito lo stato iniziale dei dati. Quando il design HDL è letto, il programma automaticamente estrae le asserzioni OVL incluse nel progetto o contenute in un separato file alla fine. L’utente potrà quindi passare in modalità di verifica e selezionare le asserzioni che desidera siano verificate. Il programma tenta di verificare in modo esaustivo le asserzioni selezionate e ritorna i risultati veri o falsi delle varie prove, fornendo inoltre un contro esempio in caso di errore. L’esempio contrario mostra come la violazione dell’asserzione può avvenire, rappresentando gli eventi in maniera sequenziale sottoforma di una serie di forme d’onda rappresentate nell’ambiente di sviluppo integrato di BlackTie (Debug). Ogni utente sarà in grado di identificare la causa d’errore con l’ausilio di programma di rappresentazione temporale per forme d’onda e un analizzatore di codice sorgente. Se un’asserzione non può essere verificata in modo esaustivo, l’utente può optare per un ciclo limitato di verifica in BlackTie per ottenere un risultato d’analisi parziale e/o usare la stessa asserzione come verifica di simulazione.

Considerazioni conclusive

Nuove tecniche di verifica sono sempre di più oggi necessarie per la verifica della funzionalità di circuiti sempre più ampi e complessi. Gli strumenti formali per la verifica dei progetti RTL aiutano ad identificare più errori in meno tempo riducendo quindi lo sforzo richiesto. La libreria OVL include un gruppo standard di moduli d’asserzione che non solo sono un valore aggiunto in fase di simulazione ma facilitano anche l’adozione di strumenti di verifica formale RTL. I moduli OVL sono scritti in linguaggio standard HDL ed in quanto tale, non è richiesto nessun linguaggio proprietario per specificare i comportamenti circuitali da verificare. Le stesse asserzioni possono essere usate sia in ambiente di simulazione sia nell’ambiente di verifica formale fornendo un ininterrotto meccanismo di transizione tra i due ambienti. Usando una verifica formale è possibile evidenziare le accresciute potenzialità di verifica in termini temporali raggiunte dai tradizionali mezzi di simulazione.

• 
• Tweet
• Pin It
• Condividi per email