Studio e proposta di utlizzo della struttura dati OBDD in alcuni ambiti dell'Informatica

Capitolo 1
Introduzione
I diagrammi binari di decisione (BDD) sono una struttura dati derivata da-
gli alberi binari di decisione (BDT) che consente di rappresentare in modo
compatto ed efficiente le funzioni booleane. Lo studio e l’impiego di tali fun-
zioni costituiscono una parte importante dell’Informatica, poiche´ molti dei
problemi legati alla realizzazione ed alla verifica di sistemi digitali possono
essere espressi sotto forma di funzioni booleane.
Negli ultimi anni, il grado di sviluppo raggiunto nella sintesi di circuiti di-
gitali e nei processi di verifica formale ha favorito la nascita di un gran numero
di sistemi automatizzati atti allo svolgimento di tali operazioni. L’efficienza
di questi sistemi dipende proprio dalle modalita` con le quali essi agiscono
sulle funzioni booleane, soprattutto in termini di:
• applicazione di operazioni logiche (come AND, OR e NOT) tra funzioni;
• verifica della soddisfacibilita` di una data funzione;
• assegnamento di valori alle variabili di input, tale che il valore finale
della funzione sia 1.
Tutti questi compiti sono caratterizzati da un tempo d’esecuzione e da un
dispendio di risorse non trascurabili. A tal proposito, esistono diversi metodi
per la rappresentazione di funzioni booleane: le tavole di verita`, gli albe-
ri sintattici e la logica a due livelli (specialmente nella forma di somma di
prodotti) sono alcuni tra i piu` comuni, ma offrono una rappresentazione che
11
1. Introduzione
non sempre e` sufficientemente compatta (nelle tavole di verita` la dimensione
cresce esponenzialmente in base al numero di variabili) e che spesso rende
problematico lo svolgimento di operazioni quali la verifica dell’equivalenza
tra espressioni booleane [33]. La Tabella 1.1 mostra la difficolta` computazio-
nale di alcune delle operazioni piu` comuni relativamente ai classici metodi di
rappresentazione [32].
Rappresentaz. di Test di Test di
funzione booleana Compatta soddisf. validita` AND OR NOT
Formule proposiz. spesso diff. diff. facile facile facile
Formule in DNF a volte facile diff. diff. facile diff.
Formule in CNF a volte diff. facile facile diff. diff.
Tavole di verita` mai diff. diff. diff. diff. diff.
OBDD ridotti spesso facile facile medio medio facile
Tabella 1.1: Metodi di rappresentazione di funzioni booleane a confronto.
I BDD sono stati proposti nel 1978 da Akers [2] come metodo ottimale per
rappresentare funzioni booleane e sono stati ulteriormente sviluppati nel 1986
da Bryant [6], con l’ideazione di metodi mirati ad ottimizzare una struttura
dati che si presentava gia` estremamente compatta ed efficiente. Nonostan-
te persistessero alcuni importanti problemi legati alla rappresentazione delle
funzioni (su tutti l’ordinamento delle variabili era quello con la maggiore in-
cidenza in termini di difficolta` computazionale), era chiaro sin da allora che
i BDD avrebbero costituito una delle scelte primarie ogni qual volta fosse
servito un modello di rappresentazione valido anche a fronte di funzioni piut-
tosto complesse. Le caratteristiche dei BDD hanno infatti spinto i ricercatori
a sperimentare costantemente nuove tecniche di ottimizzazione che riduces-
sero il tempo e le risorse richiesti per la creazione dei grafi; gli sforzi fatti
in questa direzione hanno permesso di realizzare veri e propri strumenti di
calcolo automatico basati sulla struttura dati BDD che sono stati (e vengono
tuttora) utilizzati in importanti applicazioni della ricerca informatica quali
la sintesi logica [17, 50] e la verifica formale [46, 8].
12
1.1 Obiettivi ed organizzazione della tesi
1.1 Obiettivi ed organizzazione della tesi
Il progetto di tirocinio si propone di fornire una descrizione approfondita dei
BDD e dei loro diversi ambiti di applicazione, oltre a sviluppare in termini
di proposta teorica uno strumento per il calcolo e la visualizzazione di BDD,
concepito ad hoc per la ricerca nei campi dell’informatica.
Il Capitolo 2 rappresenta un’introduzione all’argomento ed espone le ca-
ratteristiche principali dei BDD, confrontando il loro utilizzo con le altre
forme di rappresentazione di formule booleane e descrivendo gli algoritmi
che permettono di ridurre la complessita` computazionale dei BDD ordinati
(OBDD) e di effettuare efficacemente operazioni tra di essi.
Nel Capitolo 3 si analizzano le fasi principali della sintesi logica di circuiti,
un vasto insieme di processi di design che fa un uso esteso della struttura dati
BDD. La prima sezione tratta il problema della minimizzazione, in particolar
modo le questioni relative al ritardo di percorso, al consumo di potenza e
all’affidabilita` nei circuiti; nelle sezioni successive si descrivono la mappatura
tecnologica (con speciale riferimento al concetto di corrispondenza booleana),
il testing di circuiti, le macchine a stati finiti (FSM) e la fattorizzazione
(soprattuto riguardo alla sintesi a due livelli): tutti questi argomenti sono
integrati con esempi, tratti da articoli scientifici, che dimostrano la possibilita`
di utilizzare i BDD con successo nel loro caso specifico.
Il Capitolo 4 offre una panoramica sulla verifica formale, con speciale ri-
guardo ad una sua importante applicazione denominata model checking, un
metodo automatico di verifica di modelli spesso basato sulla logica tempora-
le. Dopo aver tracciato le linee base delle due logiche temporali LTL e CTL
ed aver spiegato come il loro linguaggio si riveli utile per esprimere le formule
(cioe` le proprieta`) da verificare, viene evidenziata la possibilita` di sfruttare i
BDD nel model checking simbolico, con esempi di applicazione ed una breve
spiegazione sul funzionamento di alcuni model checkers quali il NuSMV. Nel-
l’ultima sezione del capitolo si accenna alla verifica di programmi, campo piu`
specifico nel quale i BDD rivestono un ruolo importante in alcuni particolari
processi di analisi, come ad esempio l’analisi points-to.
Il Capitolo 5 sposta il discorso su altri settori dell’informatica nei quali i
13
1. Introduzione
BDD non sono ancora ampiamente utilizzati, ma assumono notevole impor-
tanza in alcuni casi particolarmente interessanti: si delinea dapprima l’ar-
gomento delle reti di Kauffman, modello di rappresentazione di reti di geni
regolatori i cui punti chiave presentano varie similitudini con i problemi tipici
della sintesi logica e della verifica formale; in seguito, si fornisce un esempio
di utilizzo dei BDD nell’ambito della sicurezza dei sistemi, in riguardo alla
protezione delle politiche di sicurezza degli stessi ed alla generazione di mo-
delli di feedback adeguati. Nelle ultime due sezioni, vengono esaminati un
caso particolare di evoluzione all’interno di un sistema multi-agente e alcuni
esempi di utilizzo dei BDD per il calcolo di operazioni su immagini binarie.
Nel Capitolo 6, infine, in base agli esempi studiati nel corso del tirocinio,
si descrive la necessita` di avere a disposizione uno strumento di carattere
generale che permetta di effettuare operazioni di calcolo tra BDD e di vi-
sualizzarne una rappresentazione grafica. Una metodologia di questo tipo
e` ad oggi inesistente, in quanto ci si e` sempre focalizzati sulla creazione di
tool appositi, specifici per l’ambito per il quale vengono sviluppati, ma del
tutto inadatti ad essere sfruttati in altri settori. Pertanto, viene progettato il
funzionamento di un tool interamente basato sul concetto di BDD, in grado
di ricevere in input file contenenti rappresentazioni di funzioni booleane (il
formato indicato e` il PLA) e di costruire i relativi OBDD (tramite un apposi-
to pacchetto quale puo` essere BuDDy), per applicare su di essi le operazioni
logiche richieste dall’utente e visualizzare cos`ı i grafi creati.
14
Capitolo 2
La struttura dati BDD
Questo capitolo si propone di fornire una panoramica sulla struttura dati
dei diagrammi binari di decisione (BDD), descrivendone la natura e le ca-
ratteristiche principali. Come fondamentale approccio alla lettura verranno
fornite le definizioni essenziali per comprendere il concetto di BDD e verran-
no descritti i metodi e le operazioni per cui essi vengono utilizzati nella logica
proposizionale.
2.1 Funzioni booleane, BDT e BDD
Una funzione booleana con n argomenti e` una funzione di tipo f(x1, x2, ..., xn),
in cui le variabili x1, x2, ..., xn sono variabili booleane che possono assumere
solamente i valori 0 e 1. Le principali operazioni tra variabili booleane sono
elencate di seguito:
• 0 = 1 e 1 = 0 (negazione);
• x · y = 1 se x e y valgono 1; altrimenti x · y = 0 (prodotto o AND);
• x+ y = 0 se x e y valgono 0; altrimenti x+ y = 1 (somma o OR);
• x⊕y = 1 se esattamente uno tra x e y vale 1 (somma esclusiva o XOR);
La relazione che la funzione stabilisce tra le variabili booleane puo` essere rap-
presentata in vari modi, i piu` famosi dei quali sono senza dubbio le tavole di
15
2. La struttura dati BDD
verita` e le formule proposizionali. Entrambi questi sistemi di rappresentazio-
ne hanno i loro svantaggi e punti di forza, ma non si puo` affermare che esista,
in generale, un metodo ottimo, ugualmente valido ed efficiente per ogni tipo
di funzione booleana. Una volta completata una tavola di verita`, ad esempio,
svolgere operazioni su di essa e` relativamente semplice, ma basti pensare che,
se la funzione fosse composta da 100 variabili, la tavola conseguente occupe-
rebbe 2100 righe, rendendo altamente inefficienti i calcoli. D’altro canto, se
le formule proposizionali sono considerate una rappresentazione compatta ed
efficiente delle formule booleane, e` altres`ı vero che alcune operazioni, in tale
rappresentazione, sono computazionalmente complesse (in particolar modo il
controllo della soddisfacibilita` e della validita` di una funzione).
x y f(x, y)
1 1 0
0 1 0
1 0 0
0 0 1
Tabella 2.1: Un esempio di tavola di verita`.
E` in questo contesto che si inserisce il modello dei BDD, che sono un
metodo differente (e generalmente piu` efficace, come avremo modo di consta-
tare) per rappresentare funzioni booleane. Per comprendere i BDD, tuttavia,
dobbiamo partire dalla loro piu` semplice forma iniziale, ovvero gli alberi bi-
nari di decisione (BDT). I BDT sono alberi binari complessi i cui nodi interni
sono etichettati con variabili booleane, mentre i nodi terminali (le foglie) so-
no etichettati con i valori 0 o 1. Da ogni nodo interno partono due archi:
il primo, quello di sinistra, e` una linea tratteggiata che si segue nel caso in
cui la variabile associata valga 0; l’arco di destra e` una linea continua che si
segue quando la variabile vale 1. Vediamo un semplice esempio.
La Figura 2.1 riporta un classico albero binario composto dalle variabili
x1, x2 e x3, la cui funzione associata e` quindi f(x1, x2, x3). Il percorso vi-
sualizzato nell’esempio mostra come si arriva, partendo dal nodo iniziale, al
nodo foglia, assumendo i valori x1 = 0, x2 = 1 e x3 = 1. In altre parole,
f(0, 1, 1) = 0.
16
2.1 Funzioni booleane, BDT e BDD
Fig. 2.1: Un esempio di BDT.
I BDT costituiscono un modello di rappresentazione molto simile alle
tavole di verita`. Se la funzione rappresentata dipende da n variabili, la tavola
di verita` corrispondente sara` composta, come abbiamo gia` detto, da 2n righe,
mentre il corrispondente albero binario avra` 2n+1 - 1 nodi. I BDT, dal canto
loro, hanno un grosso vantaggio: contengono delle ridondanze che possono
essere eliminate, rendendo quindi piu` compatta la loro forma e creando quelli
che possiamo finalmente definire BDD [31, 28].
Le strategie di riduzione che descriviamo di seguito sono 2:
• Strategia 1: i nodi che puntano con entrambi gli archi ad uno stesso
sottonodo vengono eliminati;
• Strategia 2: se 2 o piu` nodi distinti hanno la medesima struttura (cioe`
sono sottografi identici), si mantiene solo uno di essi.
E` sottinteso che, in base alla Strategia 2, vengono mantenuti solo 2 nodi
terminali, rappresentanti i valori 0 e 1.
Il risultato di queste trasformazioni e` un BDD che spesso risulta molto
piu` compatto dell’albero iniziale. Il BDD derivato dallo schema di Figura
2.1, ad esempio, e` mostrato in Figura 2.2. Quando su un BDD non e` piu`
possibile applicare le trasformazioni 1 e 2, il BDD si dice ridotto.
I diagrammi binari di decisione sono particolari DAG, ovvero grafi diretti
aciclici. In un DAG, un nodo si definisce iniziale se non ha archi entran-
ti, terminale se invece da esso non parte alcun arco. Un grafo e` aciclico se
ogni nodo non si ripresenta piu` di una volta sullo stesso cammino (ovvero,
se non contiene cicli). L’eventuale presenza di cicli in un BDD, oltre a ge-
nerare informazioni ridondanti, potrebbe portare alla presenza di cammini
17
2. La struttura dati BDD
Fig. 2.2: Il BDD derivato dall’albero di Fig. 2.1.
inconsistenti, cioe` percorsi in cui la variabile si presenta sia diretta che ne-
gata. Questo concetto serve anche a stabilire la soddisfacibilita` e la validita`
della funzione rappresentata da un BDD: la prima si ha se il nodo terminale
1 e` raggiungibile solo attraverso cammini consistenti; la validita` si verifica
quando, viceversa, la foglia 0 non e` raggiungibile da cammini consistenti.
2.2 OBDD e algoritmi
Come anticipato, BDD che contengano piu` occorrenze di una stessa variabile
lungo un percorso sono inefficienti. Per ovviare a questo problema e` necessa-
rio imporre un ordinamento per le variabili contenute in un BDD, rendendo
quindi quest’ultimo un BDD ordinato (o OBDD). Il grafo di Figura 2.1, ad
esempio e` un BDD con ordinamento x1, x2, x3. Cio` comporta che l’OBDD
ridotto che rappresenta una funzione f e` unico e non ci possono essere altri
OBDD con lo stesso ordine di variabili che si riferiscano a quella funzione
ed abbiano struttura diversa. Quindi, un OBDD ridotto e` definito in for-
ma canonica. Tramite la rappresentazione in forma canonica, e` possibile
compiere alcuni test [32]:
• Assenza di variabili ridondanti;
• Test di equivalenza semantica: OBDD ridotti si riferiscono alla
stessa funzione se hanno la medesima struttura;
18
2.2 OBDD e algoritmi
• Test di validita`: f e` una funzione valida se il suo OBDD ridotto
equivale ad 1;
• Test di implicazione: date due funzioni f e g, f ⇒ g se l’OBDD
ridotto per f · g e` 0;
• Test di soddisfacibilita`: f e` soddisfacibile se il suo OBDD ridotto e`
diverso da 0;
Vediamo ora quali sono e come funzionano gli algoritmi che si possono
applicare sui BDD per eseguire operazioni tra di essi o per minimizzarne la
rappresentazione [32].
1. Reduce. Ad ogni nodo n dell’OBDD viene assegnata un’etichetta inte-
ra id(n), in modo che sottografi aventi nodo radice n o m rappresentino
la stessa funzione se e solo se id(n) = id(m). Definiamo inoltre lo(n) il
nodo collegato ad n da linea tratteggiata, hi(n) quello collegato da linea
continua. L’algoritmo procede in questo modo: se l’etichetta id(lo(n))
e` la stessa di id(hi(n)), anche a n viene assegnata la stessa etichetta (n
viene quindi eliminato perche` ridondante); se due nodi n e m sono sul-
lo stesso livello e id(lo(n)) = id(lo(m)) e id(hi(n)) = id(hi(m)), allora
id(n) = id(m) (perche` n e m descrivono la stessa funzione booleana);
negli altri casi non possono essere applicate riduzioni e id(n) prende il
valore della prima etichetta non ancora utilizzata. Questo algoritmo e`
iterato a partire dalle foglie, ovvero dai nodi etichettati con 0 e 1.
Fig. 2.3: Un esempio di applicazione dell’algoritmo reduce.
19
2. La struttura dati BDD
2. Restrict. Indichiamo con f [0/x] la funzione ottenuta sostituendo
tutte le occorrenze di x in f con il valore 0. Lo stesso principio
si applica ad f [1/x]. Dato quindi l’OBDD Bf , chiamare l’algoritmo
restrict(0, x, Bf ) significa applicare f [0/x] alla funzione f . L’algorit-
mo procede nel seguente modo: per ogni nodo n contrassegnato dalla
variabile x gli archi entranti vengono diretti a lo(n) e n viene rimosso.
Nel caso di restrict(1, x, Bf ), i nodi entranti vengono invece diretti a
hi(n). Il concetto di restrizione permette di introdurre un’altra impor-
tante definizione, cioe` la cosiddetta espansione di Shannon: per ogni
variabile x di una funzione booleana f , si ha che f ≡ x·f [0/x]+x·f [1/x].
3. Apply. L’algoritmo apply serve a svolgere le operazioni +, ·, ⊕ e ne-
gazione su due OBDD ridotti. Si indica con apply(op,Bf , Bg) il calcolo
dell’OBDD ridotto per la formula f op g. La funzione apply si basa
sull’espansione di Shannon per f op g :
f op g = x · (f [0/x] op g[0/x]) + x · (f [1/x] op g[1/x]).
L’algoritmo procede nel seguente modo: indichiamo con rf un nodo di
Bf e con rg un nodo di Bg. Se rf e rg sono due nodi terminali (quindi
hanno valore 0 o 1), allora calcoliamo la funzione (rf op rg) in modo
che il sottografo risultante abbia valore 0 o 1; se rf e rg non sono nodi
terminali ma, ad esempio, sono entrambi nodi contenenti la variabi-
le xi, si crea un nuovo nodo xi da cui partira` un arco tratteggiato per
apply(op, lo(rf ), lo(rg)) e un arco continuo per apply(op, hi(rf ), hi(rg))
(cioe` applichiamo la formula derivata dall’espansione di Shannon); se
rf e` un nodo xi e rg e` un nodo terminale, oppure di livello diverso da i,
creiamo un nodo xi con arco tratteggiato per apply(op, lo(rf ), rg), conti-
nuo per apply(op, hi(rf ), rg). L’OBDD che deriva da questa procedura
deve poi essere ridotto.
4. Exists. Una funzione booleana puo` essere vista come un vincolo sulle
variabili che la compongono. Ad esempio, x + (y · z) vale 1 solo se x
e` 1, o se y e` 0 e z e` 1. Puo` essere utile rilassare il vincolo su una o
20