- Timestamp:
- Jul 1, 2010, 10:31:08 AM (14 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
liacs/SCA2010/BDD/report.tex
r138 r139 159 159 maken van formule~\ref{melt-eq}. Let wel op dat dit voorbeeld geen ontbrekende 160 160 laag van nodes heeft, waardoor nodes van alle niveaus beschikbaar zijn. Op het 161 moment dat de $\diamond$ ingevul tgaat worden is het ook zaak om de bladeren161 moment dat de $\diamond$ ingevuld gaat worden is het ook zaak om de bladeren 162 162 (zie vergelijking~\ref{bladeren}) te vereenvoudigen} \end{figure} 163 163 164 164 \section{Introductie BDD} 165 165 Synthese van een Binary Decision Diagram \emph{BDD} is het belangrijke 166 \emph{BDD} algoritme~\cite[p p86]{DK2009}. Welke in essentie een \emph{BDD}166 \emph{BDD} algoritme~\cite[pg 86]{DK2009}. Welke in essentie een \emph{BDD} 167 167 functie,$f$, pakt en deze combineert met een andere \emph{BDD} functie,$g$, 168 168 zodanig dat er een nieuwe \emph{BDD} ontstaat voor de nieuwe functie. … … 177 177 \label{werking} 178 178 De term voor het samenvoegen \emph{BDD} structuren zullen we smelten 179 (\emph{melding}) noemen. Er werkt volgens de volgende princip ies. Men neme179 (\emph{melding}) noemen. Er werkt volgens de volgende principes. Men neme 180 180 $\alpha = (v,l,h)"$ en $\alpha' = (v',l',h')$. De $\alpha \diamond \alpha'$, de 181 181 "\emph{emulsie}" (\emph{meld}) van $\alpha$ en $\alpha'$, is dan als volgt 182 gedefin eerd als $\alpha$ ad $\alpha'$ niet beiden bladeren (\emph{sinks}) zijn:182 gedefinieerd als $\alpha$ ad $\alpha'$ niet beiden bladeren (\emph{sinks}) zijn: 183 183 \begin{equation} 184 184 \label{melt-eq} 185 185 \alpha \diamond \alpha' = \left\{ 186 186 \begin{array}{l l} 187 (v, l \diamond l'), h \diamond h'), & \mathrm{ if~} v = v'; \\188 (v, l \diamond \alpha'), h \diamond \alpha'), & \mathrm{ if~} v < v'; \\189 (v, \alpha \diamond l'), \alpha \diamond h'), & \mathrm{ if~} v > v'. \\187 (v, l \diamond l'), h \diamond h'), & \mathrm{als~} v = v'; \\ 188 (v, l \diamond \alpha'), h \diamond \alpha'), & \mathrm{als~} v < v'; \\ 189 (v, \alpha \diamond l'), \alpha \diamond h'), & \mathrm{als~} v > v'. \\ 190 190 \end{array} \right. 191 191 \end{equation} … … 202 202 Om er weer een 'valide' \emph{BDD} van te maken zullen deze bladeren vervangen 203 203 worden door het uitgerekende blad. Als bijvoorbeeld de $\diamond$ operatie een 204 $EN$ operatie was, wordt de blad rij in~\ref{bladeren} vervangen door de rij204 $EN$ operatie was, wordt de blad-rij in~\ref{bladeren} vervangen door de rij 205 205 $\bot, \bot, \bot, \top$. Nu is het zaak de \emph{BDD} te vereenvoudigen, om zo 206 206 duplicaat bladeren te snoeien (\emph{pruning}). … … 216 216 Deze grenzen worden in voorbeeld~\ref{voorbeeldSamenvoegen} aangescherpt. 217 217 218 Het smelten ligt aan de basis van de daa rwerkelijke synthese. Een simpele218 Het smelten ligt aan de basis van de daadwerkelijke synthese. Een simpele 219 219 variant kan gemaakt worden met algoritme $R$. Maak eerst een reeks van 220 220 alle knopen $\alpha$ in $B(f)$ en $\alpha'$ in $B(g)$ met knoop $\alpha … … 226 226 227 227 Deze 'truc' zorgt ervoor dat de tijd binnen de perken blijft, maar er is dan 228 nog niets gezeg tover de hoeveelheid geheugen er nodig is. Omdat er nu228 nog niets gezegd over de hoeveelheid geheugen er nodig is. Omdat er nu 229 229 $B(f)B(g)$ knopen in geheugen gehouden moet wordt zal dit problemen opleveren 230 bij kleine en grotere algoritmen. Om deze ineffientie aan te pakken is230 bij kleine en grotere algoritmen. Om deze efficiëntie aan te pakken is 231 231 algoritme $S$ \footnote{Algoritme $S$ wordt niet in deze samenvatting gehandeld 232 de vak website~\cite{SCA2010} heeft een verwijzing van de samenvatting van dit232 de vak-website~\cite{SCA2010} heeft een verwijzing van de samenvatting van dit 233 233 algoritme} ontworpen. 234 234 … … 251 251 kunnen worden van de functies $f$ en $g$. 252 252 253 Elke bead van de orde $n - j$ van het geo ordende paar $(f,g)$ zal binnen de253 Elke bead van de orde $n - j$ van het geordende paar $(f,g)$ zal binnen de 254 254 standaard combinatie vallen de $b_{j}b_{j}'$ geordende beats van $(f,g)$. 255 255 vallen of is er eentje uit een meer speciaal gegenereerde reeks van een … … 290 290 = q$. waar $0 \leq p, q \le 2^m$ en $p=q$ dan en slechts als $x_1 = x_3 = \dots 291 291 = 2_{2m-1} = 0$. Dit zorgt dat het eerste deel -het stuk voor de punt 292 comma- van het profiel van $f \land g$ geschreven kan worden als $(1, 2, 4,\dots,292 komma- van het profiel van $f \land g$ geschreven kan worden als $(1, 2, 4,\dots, 293 293 2^{2m-2}, 2^{2m-1} - 2^{m-1}$. 294 Het tweede deel is aanzienlijk moeilijker, welke bestaat uit de sub functies294 Het tweede deel is aanzienlijk moeilijker, welke bestaat uit de sub-functies 295 295 $x_{2m+j} \land \overline x_{2m+k}$ of $\overline x_{2m+j} \land x_{2m+k}$ voor 296 $1 \leq j \le k \leq 2^m$ te samen met de orginelen $x_{2m+j}$ en $\overline296 $1 \leq j \le k \leq 2^m$ tezamen met de originelen $x_{2m+j}$ en $\overline 297 297 x_{2m+j}$ voor $2 \leq j \leq 2^m$. Welke het profiel oplevert van $(2^{m+1}-2, 298 298 2^{m+1}-2, 2^{m+1}-4, 2^{m+1}-6, \dots, 4, 2, 2)$.
Note:
See TracChangeset
for help on using the changeset viewer.