verifica formale e convenzionale di verifica

S

steven852

Guest
Salve,

Mi chiedo quando applicare e quali sarebbero i criteri in termini di utilizzo di strumenti di verifica formale e strumenti di verifica convenzionali (non è sicuro se questo nome è giusto, voglio dire, gli strumenti generali per fare la verifica: Verilog, VHDL, e, ecc.)Nonostante alcune limitazioni di strumenti di verifica formale (quando retiming registro, etc), è piuttosto potente, e allora perché non abbiamo ancora bisogno di strumenti convenzionali?

Grazie

 
Ciao, ho un dubbio.Sono nuovo di questo concetto di VERIFICA formale.U può chiarire se la funzionalità può essere controllato mediante verifica formale?

 
Certo, la verifica formale, non solo può fare la verifica funzionale ma anche fisica di verifica (check netlist).In breve, 4 combinazioni tra RTL e gate-netlist livello può essere verificato, nonché i file di libreria.

 
I due modi di verifica sono
1 - Verifica formale
2 - verifivication funzionale

Ognuno ha le sue metodologie proprie

 
"verifica formale, non in grado di dimostrare che tutte le proprietà di un disegno sono stati elencati, anche se per un immobile dato in grado di dimostrare se la proprietà è soddisfatta."

questa affermazione, ho avuto da un libro.la speranza la sua chiara per rispondere alla prima domanda.

 
Ebbene, tutto ciò che ha detto è vero.Tuttavia, situazioni particolari alle quali sono applicabili era la mia domanda.

Grazie comunque.

 
Verifica formale è utilizzato principalmente a testing a livello di blocco, mentre un progettista scrive il suo modulo di verificare se il modulo funziona nei confronti di tutti i casi (input) in base alle affermazioni di cui il design.Questo può essere sicuramente un vantaggio per la verifica del progetto in una fase precoce.

Thanks & Regards

 
Verifica formale è quello di verificare se è la stessa funzione tra il RTL e netlist.

 
Ritengo che alcuni membri qui non capisco che cosa è esattamente "Formal Verification".Lemme cercare di dare un po 'di storia ....

Verifica formale non è altro che cercare di risolvere un problema formale con metodo matematico.Ci sono 3 tipi coinvolti in essa:
1.Model Checking
2.Verifica di equivalenza
3.Teorema Proving.

"Equivalenza Controllo" è la cosa più comune, nota a tutti ma di cui di solito ad una verifica formale (Strumenti: formalità).Questo è utilizzato per verificare l'equivalenza tra RTL a RTL RTL o di netlist.

"Model Checking" è dove scriviamo proprietà formali che descrivono il comportamento previsto e gli strumenti in grado di dimostrare se la proprietà vale in tutte le condizioni possibili.(Strumenti: Cadence IFV - Incisive formale Verifier)

Alcuni criteri per cercare qui sono:
- Ogni volta che un progetto è il controllo intensivo è un candidato molto buono per il model checking.
- Se il progetto è percorso intensivo di dati è un candidato migliore per le lingue di verifica di alto livello (e-specman, vera ..)Con i migliori saluti,
http://hdlplanet.tripod.com
http://groups.yahoo.com/group/hdlplanet

 
You must log in or register to reply here.

Welcome to EDABoard.com

Sponsor

Back
Top