Politecnico di Torino | |||||||||||||||||
Anno Accademico 2012/13 | |||||||||||||||||
02LQDOV Specification and simulation of digital systems |
|||||||||||||||||
Corso di Laurea Magistrale in Ingegneria Informatica (Computer Engineering) - Torino |
|||||||||||||||||
|
|||||||||||||||||
|
|||||||||||||||||
Presentazione
The course is taught in English.
Insegnamento dell'orientamento Embedded Systems della Laurea Magistrale in Ingegneria Informatica collocato al II semestre del I anno. Il corso fornisce la capacitą di descrivere progetti digitali a diversi livelli di astrazione mediante il linguaggio VHDL. Il corso completa le tecniche di progetto acquisite negli insegnamenti di base di progetto logico, estendendole a livello register-transfer con orientamento alla sintesi automatica. Il corso utilizza le tecniche di verifica mediante simulazione per lo sviluppo in laboratorio di un progetto e presenta le tecniche di verifica basate su metodi formali, con particolare riferimento alla verifica di equivalenza combinatoria e sequenziale e al model checking. Infine introduce le nozioni basilari di collaudo. |
Risultati di apprendimento attesi
- Conoscenza della sintassi e della semantica del VHDL
- Capacitą di descrivere progetti digitali complessi in VHDL a diversi livelli di astrazione - Conoscenza delle caratteristiche fondamentali dei sistemi embedded - Conoscenza dei criteri di metrica per la valutazione di progetti - Conoscenza delle metodologie di progetti di sistemi a livello register-transfer - Capacitą di progettare sistemi digitali complessi a livello register-transfer mediante sistemi CAD - Capacitą di verificare mediante simulazione progetti di sistemi digitali complessi - Conoscenza delle principali tecniche di verifica formale, con particolare riferimento alla verifica di equivalenza combinatoria e sequenziale e al model checking - Conoscenza delle nozioni basilari di collaudo - Capacitą di generare sequenze di collaudo per circuiti combinatori semplici. |
Prerequisiti / Conoscenze pregresse
Conoscenza delle tecniche elementari di progetto di reti logiche combinatorie e sequenziali sincrone.
|
Programma
VHDL (1.0 cr): struttura dei file VHDL: entity/architecture; stili di descrizione: behavioral, dataflow, strutturale; elementi lessicali; oggetti: segnali, variabili e costanti; tipi di dato: tipi scalari, tipi composite; operatori e attributi; costrutti concorrenti: assegnazione concorrente di segnali, costrutto generate, processi concorrenti, istanziazioni di componenti; costrutti sequenziali: processi, costrutti condizionali, costrutti iterativi; tecniche di partizionamento: block, package, library, component, configuration.
Progetto di sistemi embedded a livello Register Transfer (0.8 cr): metriche di progetto e loro ottimizzazione; le tecnologie fondamentali per i sistemi embedded: tecnologia dei processori, tecnologia dei circuiti integrati, tecnologia di progetto; progetto di processori single-purpose: il modello FSM-D, dall'algoritmo all'FSM-D, sintesi dell'unitą operativa, sintesi dell'unitą di controllo, descrizione in VHDL; ottimizzazione di processori single-purpose, FSM-D, unitą operativa, macchine a stati finiti (FSM); ottimizzazione di FSM: minimizzazione degli stati (algoritmo semplificato ed esatto per la rilevazione di stati equivalenti), euristiche per la codifica degli stati. Progetto di sistemi a livello RT (0.8 cr): grafi di esecuzione (concorrenti, sequenziali, group-sequential); organizzazione dei sistemi (sistemi condivisi, sistemi non condivisi, sistemi single-module); controllo centralizzato vs decentralizzato vs parzialmente centralizzato; specifica e implementazione in VHDL di sistemi a livello RT; metodologia di progetto di sistemi a livello RT. Sottosistemi dati e controllo (0.2 cr): component e organizzazione dei sottosistemi dati; progetto dei sottosistemi dati; implementazione dei sottosistemi controllo come FSM. Verifica formale (0.8 cr): approcci alla verifica di progetto: simulazione vs. verifica formale; theorem proving: logica proposizionale, logica del prim'ordine, logica di ordine superiore; dimostrazione di equivalenza: Binary Decision Diagrams, verifica di equivalenza combinatoria, verifica di equivalenza sequenziale (symbolic reachability analysis, il modello della macchina prodotto); Model Checking: linear-time temporal logic, branching-time temporal logic, proprietą di liveness e safety properties, algoritmi di model checking. Principi collaudo elettronico (0.4 cr): physical failures e modelli di guasto; il modello di guasto stuck-at fault model: fault detection, fault equivalence e collapsing, fault coverage); algoritmi per la generazione dei test pattern generation (differenze Booleane). |
Organizzazione dell'insegnamento
In laboratorio gli studenti utilizzano il pacchetto Xilinx® ISE' 11 per sviluppare un progetto a livello RT second le metodologie illustrate a lezione. Il progetto č valutato su CoolRunnerTM-II Evaluation Board, una piattaforma complete per lo sviluppo di circuiti per lo Xilinx CoolRunner-II CPLD (2.0 cr).
|
Testi richiesti o raccomandati: letture, dispense, altro materiale didattico
Lucidi pubblicati sul Portale. Testi addizionali:
' D. Pellerin, D. Taylor 'VHDL Made easy!', Prentice Hall 1997 ' F. Vahid, T. Givargis 'Embedded System Design: a unified hardware/software introduction', John Wiley, 2002 ' M.Ercegovac, T. Lang, J. Moreno 'Introduction to digital systems', John Wiley, 1999 ' S. Mourad, Y. Zorian 'Principles of Testing Electronic Systems', John Wiley, 2000 ' ISE in-depth tutorial, Xilinx ' CoolRunner-II Evaluation Board Reference Manual, Xilinx |
Criteri, regole e procedure per l'esame
Gli studenti per gruppi di 2/3 svolgono un progetto assegnato nell'ultima parte del corso. Esso consiste in un progetto a livello RT di un sistema complesso descritto in VHDL. L'attivitą inizia in laboratorio durante il corso e poi viene portata a termine dagli studenti. Il progetto viene valutato. Se sufficiente, ogni studente sostiene un esame orale su tutti gli argomenti trattati nel corso. Il voto finale integra il voto del progetto e quello dell'esame orale.
|
Orario delle lezioni |
Statistiche superamento esami |
|