Intel Keynote sul formale A Mind-Stretcher

Ripubblicato da Platone

Seguaci: 0

Synopsys ha pubblicato sul sito SolvNet un discorso affascinante tenuto dal Dr. Theo Drane di Intel Graphics. L'argomento è il controllo dell'equivalenza del percorso dati. Potrebbe sembrare solo un'altra approvazione DPV formale di Synopsys VC, ma dovresti guardarlo comunque. Questa è una discussione che espande la mente sugli usi e le considerazioni in ambito formale che ti porterà oltre il tipo di presentazione di routine della guida per l'utente in un territorio più affascinante.

Intel Keynote sul formale

Comprensione intellettuale e test su campioni

La simulazione basata sui test in tutte le sue forme è eccellente e spesso insostituibile nel verificare la correttezza di una specifica o di un'implementazione di progettazione. È anche facile iniziare. Basta scrivere un programma di test e iniziare a simulare. Ma il rovescio della medaglia di questa semplicità è che non ne abbiamo bisogno completamente capire cosa stiamo testando per iniziare. Ci convinciamo di aver letto attentamente le specifiche e di aver compreso tutti i casi limite, ma non ci vuole molta complessità per sopraffare la nostra comprensione.

Formal ti incoraggia a comprendere la funzionalità a un livello profondo (almeno se vuoi fornire un risultato prezioso). Nell’esempio sopra, una semplice domanda – z può mai essere tutta 1 – non riesce a dimostrare un esempio in un miliardo di cicli su un simulatore. Non sorprende, dal momento che si tratta di un caso limite estremo. Un test formale fornisce un esempio specifico e molto non ovvio in 188 secondi e può dimostrare che si tratta dell'unico caso simile in un tempo leggermente inferiore.

OK, il formale ha fatto ciò che i test dinamici non potevano fare, ma, cosa ancora più importante, hai imparato qualcosa che il simulatore potrebbe non averti mai detto. Che c'era un solo caso possibile in cui quella condizione poteva verificarsi. Formal ti ha aiutato a comprendere meglio la progettazione a livello intellettuale, non solo come riepilogo probabilistico attraverso una serie finita di casi di test.

Problemi di specifiche

Il prossimo esempio di Theo è basato su un distributore automatico di insetti (così chiamato perché quando premi un pulsante ottieni un bug). Sembra un problema di controllo dell'equivalenza da C a RTL piuttosto semplice, modello C a sinistra, modello RTL a destra. Una sorpresa per Theo nei suoi primi giorni nel mondo formale è stata che il comportamento dello spostamento a destra nel modello C non è completamente definito nello standard C, anche se gcc si comporterà in modo ragionevole. DPV lamenterà però, come è giusto, una discrepanza nel confronto con RTL. Un comportamento indefinito è una cosa pericolosa su cui fare affidamento.

Formale come un distributore automatico di insetti

Il confronto delle specifiche tra C e RTL comporta altri rischi, in particolare riguardo alle larghezze di bit. Il troncamento o la perdita di un bit di riporto in un segnale intermedio (#3 sopra) sono buoni esempi. Sono questi problemi di specifiche? Forse un'area grigia tra le specifiche e le scelte di implementazione.

Oltre il controllo di equivalenza

Lo scopo principale di DPV, sembrerebbe, è verificare l'equivalenza tra un riferimento C o RTL e un'implementazione RTL. Ma questa necessità è relativamente rara e ci sono altri modi utili in cui tale tecnologia potrebbe essere applicata, anche se un po’ fuori dagli schemi. Innanzitutto un classico nel mondo dell'implementazione: ho apportato una modifica, corretto un bug: di conseguenza ho introdotto nuovi bug? Un po' come il controllo SEQ dopo aver aggiunto il clock gating. In alcuni casi l'analisi della raggiungibilità negli output dei blocchi può essere un'altra applicazione utile.

Non solo controllo di equivalenza

Theo diventa ancora più creativo, chiedendo ai tirocinanti di utilizzare controesempi per comprendere meglio il design, risolvere Sudoku or fattorizzare gli interi. Riconosce che il DPV è un modo strano di affrontare tali problemi, ma sottolinea che il suo intento è quello di rompere l'illusione che il DPV serva solo per il controllo dell'equivalenza. Un'idea interessante e certamente impegnativa per affrontare tali sfide. (Confesso di aver subito iniziato a pensare al problema del Sudoku non appena me ne ha parlato.)

Avvolgere

Theo conclude con una discussione sulle metodologie importanti nell'utilizzo della produzione, sui vincoli, sulle regressioni e sui confronti con i modelli RTL legacy. Inoltre, è difficile sapere se ciò che si sta controllando corrisponde effettivamente alle specifiche del linguaggio naturale di livello superiore.

Discorso molto energizzante, vale la pena guardarlo qui su SolvNet!

Condividi questo post tramite: