Il supporto della Open Verification Library nella verifica formale

• 
• Tweet
• Pin It
• Condividi per email

Per molti anni, i gruppi di progettazione di microelettronica hanno fatto affidamento sulla sola simulazione come strumento primario ed affidabile per la verifica a livello “Register Transfer Level”(RTL). Recentemente, tuttavia, ulteriori mezzi di supporto hanno incominciato ad affermarsi e si è incominciato ad incorporare nei processi di verifica nuovi strumenti e tecnologie, tra i quali i più importanti sono i tool per l’automazione dei testbench e nuovi strumenti di verifica formale.
Le ragioni per questo sono ovvie; la simulazione da sola non è sufficiente a garantire una verifica nei tempi richiesti. Essa rappresenta ancora una parte critica dei processi di verifica, tuttavia, le nuove tecnologie necessitano ancora di essere integrate nella simulazione per poter ottenere dei risultati efficaci ed essere semplici da implementare. Una verifica formale RTL ed un metodo basato su un’asserzione sono stati combinati per permettere ad una verifica formale di lavorare in un ambiente di simulazione.

La necessità di verifica formale

Con l’attuale dimensione circuitale ormai formata da milioni di transistori è virtualmente impossibile simulare in modo esaustivo un progetto, poiché il numero di vettori richiesti risulta essere una funzione esponenziale del numero delle configurazioni di stato e degli ingressi possibili. In generale, solo una frazione degli stati raggiungibili sarà esplorata durante la simulazione e quindi possibili malfunzionamenti non potranno essere identificati. Una verifica formale non richiede vettori di simulazione ed assicura l’identificazione dei bachi in modo più veloce e ne rende semplice l’eliminazione. Un metodo di verifica formale offre al progettista quindi uno strumento più intelligente per la verifica del componente. Piuttosto che applicare degli stimoli agli ingressi e comparare le risposte ottenute con i risultati previsti, una verifica formale analizza un circuito matematicamente per provare o smentire le sue proprietà funzionali. Viene così meno la necessità di creare dei vettori di test funzionali ad eccezione per quelle parti del disegno dove una verifica con simulazione ha senso. A differenza della simulazione che mostra solo la presenza degli errori, una verifica formale ne può provare la loro assenza. Uno strumento di verifica formale quando trova un errore genera un esempio contrario per dimostrare la condizione d’errore. Mette quindi il progettista nelle condizioni di verificare più velocemente il progetto e di avere un più alto livello di confidenza sull’affidabilità dello stesso. L’avvento dei banchi automatici di collaudo ha aiutato molto i progettisti nei processi di verifica anche se l’ammontare delle funzionalità coperte dai programmi di test è ancora relativamente basso. Lo sviluppo delle simulazioni per i banchi di collaudo necessita inoltre di un tempo di progetto a volte non indifferente. Una tecnica di verifica formale, invece, non richiede la generazione dei programmi di test e nemmeno un investimento nei banchi automatici di collaudo. Di conseguenza, il miglior strumento di verifica risulta essere un approccio di combinazioni tra simulazione e verifica formale attraverso una metodologia di specifiche asserzioni. Ciascuna asserzione rappresenta un’istruzione di comportamenti funzionali; verificando quindi ciascun’asserzione si verifica la correttezza della funzionalità del circuito in esame. La “Open Verification Library “ (OVL), posta di pubblico dominio da Verplex Systems, offre uno strumento di congiunzione tra simulazione e verifica formale. OVL fornisce un set standard di moduli d’asserzione che possono essere usati per analizzare il comportamento del circuito da verificare. Ciascun modulo può essere scritto una sola volta e usato in multipli strumenti di verifica, che includono simulatori standard HDL e strumenti di verifica formale come il BlackTie di Verplex Systems. Per semplicità, OVL usa un linguaggio di sintassi HDL (Verilog) e BlackTie permette di lavorare con progetti di larghe dimensioni. Vengono così superate due delle più grosse difficoltà incontrate dai progettisti per questi tipi di metodologie.

Verifica funzionale RTL tramite uso di metodi formali

L’applicazione di una tecnica formale RTL per la verifica di un progetto assicura che il circuito sia conforme alle specifiche attraverso la verifica matematica delle asserzioni. Ciascuna asserzione rappresenta un’istruzione che descrive il comportamento previsto del circuito. Per la verifica di queste istruzioni, vengono generate tutte le possibili combinazioni degli ingressi e tutti gli stati raggiungibili sono identificati.

• 
• Tweet
• Pin It
• Condividi per email