Finalità

Il corso si propone di fornire una panoramica sulle tecniche di verifica formale applicate nell'ambito del progetto di circuiti digitali, protocolli e software, con particolare enfasi al primo ambiente.

Tali tecniche hanno assunto un progressivo interesse e applicazione come metodi complementari e/o alternativi alla simulazione, a causa della dimensione crescente dei sistemi progettati.

Il corso fornirà sia basi teoriche che esperienze applicative (uso di strumenti di verifica formale).

Argomenti trattati durante il corso

• Verifica di proprietà logiche e temporali (model checking)
• Verifica di equivalenza per circuiti combinatori e sequenziali
• Theorem proving
• Linguaggi orientati alla verifica
• Manipolazioni simboliche mediante Binary Decision Diagram
• Analisi di soddisfacibilità (SAT solving)
• Interazioni tra verifica e testing
• Verifica di sistemi reattivi

Laboratorio

Alcuni argomenti di particolare rielievo verranno analizzati con strumenti accademici di CAD; in particolare si prevedono laboratori mediante l'uso di strumenti software sui seguenti argomenti:

• Rappresentazione di funzioni mediante Binary Decision Diagrams
• Analisi di raggiungibilità
• Verifica di equivalenza e di proprietà

Testi consigliati

Dispense specifiche saranno rese disponibili dai docenti durante il corso.

Riferimenti bibliogafici saranno in essi indicati qualora necessario.