| 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 |
|
|