en
Politecnico di Torino
Anno Accademico 2011/12
02LQDOV
Specification and simulation of digital systems
Corso di Laurea Magistrale in Ingegneria Informatica (Computer Engineering) - Torino
Docente Qualifica Settore Lez Es Lab Tut Anni incarico
Camurati Paolo Enrico ORARIO RICEVIMENTO PO IINF-05/A 40 0 20 0 20
SSD CFU Attivita' formative Ambiti disciplinari
ING-INF/05 6 B - Caratterizzanti Ingegneria informatica
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

Programma definitivo per l'A.A.2011/12
Indietro