% arara: pdflatex
% arara: pdflatex
% arara: pdflatex

% options:
% thesis=B bachelor's thesis
% thesis=M master's thesis
% czech thesis in Czech language
% slovak thesis in Slovak language
% english thesis in English language
% hidelinks remove colour boxes around hyperlinks

\documentclass[thesis=B,czech,russian]{FITthesis}[2019/12/23]

\usepackage[utf8]{inputenc} % LaTeX source encoded as UTF-8

\usepackage{amsmath} %advanced maths
% \usepackage{amssymb} %additional math symbols

\usepackage{graphicx}

\usepackage{xcolor}
\usepackage{textcomp}

\usepackage{dirtree} %directory tree visualisation
\usepackage[]{algorithm2e}
\usepackage{listings}
\lstset{language=C++,
	basicstyle=\ttfamily,
	keywordstyle=\color{blue}\ttfamily,
	stringstyle=\color{red}\ttfamily,
	commentstyle=\color{green}\ttfamily,
	morecomment=[l][\color{magenta}]{\#}
}

\usepackage{hyperref}
\hypersetup{
	colorlinks=true,
	linkcolor=black,
	filecolor=black,      
	urlcolor=black,
}

\usepackage{dirtree} %directory tree visualisation

% % list of acronyms
% \usepackage[acronym,nonumberlist,toc,numberedsection=autolabel]{glossaries}
% \iflanguage{czech}{\renewcommand*{\acronymname}{Seznam pou{\v z}it{\' y}ch zkratek}}{}
% \makeglossaries

%\newcommand{\tg}{\mathop{\mathrm{tg}}} %cesky tangens
%\newcommand{\cotg}{\mathop{\mathrm{cotg}}} %cesky cotangens

% % % % % % % % % % % % % % % % % % % % % % % % % % % % % % 
% ODTUD DAL VSE ZMENTE
% % % % % % % % % % % % % % % % % % % % % % % % % % % % % % 

\department{Katedra softwarového inženýrství}
\title{Komprese testu pro RAS architekturu založená na řešení SAT problému}
\authorGN{Karel} %(křestní) jméno (jména) autora
\authorFN{Pajskr} %příjmení autora
\authorWithDegrees{Mgr. Karel Pajskr} %jméno autora včetně současných akademických titulů
\author{Karel Pajskr} %jméno autora bez akademických titulů
\supervisor{doc. Ing. Petr Fišer, Ph.D.}
\acknowledgements{Rád bych vyjádřil dík doc. Ing. Petru Fišerovi, Ph.D. za ochotu a trpělivost, se kterou tuto práci vedl, jakožto i všechny poskytnuté konzultace, rady a materiály.}
\abstractCS{Bakalářská práce se zabývá problematikou vytváření komprimovaného testu pro číslicové obvody s RAS architekturou. Práce se sestává z teoretického úvodu do problematiky, popisu a analýzy řešiče Minisat+, jeho integrace ve formě knihovny do frameworku LogSynth a tvorby programu pro generování testu, který je založen na novém originálním algoritmu.}
\abstractEN{This thesis deals with the problematics of test pattern generation for circuits with RAS architecture. The thesis consists of a theoretical introduction, description and analysis of Minisat+ solver, its integration into LogSynth framework as a library and a creation of a test pattern generator base on a novel algorithm.}
\placeForDeclarationOfAuthenticity{V~Praze}
\declarationOfAuthenticityOption{1} %volba Prohlášení (číslo 1-6)
\keywordsCS{Random access scan, Minisat+, Pseudo-booleovská optimalizace}
\keywordsEN{Random access scan, Minisat+, Pseudo-boolean optimization}
% \website{http://site.example/thesis} %volitelná URL práce, objeví se v tiráži - úplně odstraňte, nemáte-li URL práce

\begin{document}

% \newacronym{CVUT}{{\v C}VUT}{{\v C}esk{\' e} vysok{\' e} u{\v c}en{\' i} technick{\' e} v Praze}
% \newacronym{FIT}{FIT}{Fakulta informa{\v c}n{\' i}ch technologi{\' i}}

\begin{introduction}
Integrované obvody patří k technologiím, ve kterých za poslední desítky let došlo k neuvěřitelnému vývoji a dnes ovlivňují již téměř každou oblasti lidské činnosti. Tvoří jádra mobilů a počítačů, nalezneme je v průmyslu, dopravních prostředcích i ve spotřební elektronice. Dnešní čipy jako např. procesory či jádra grafických karet mívají miliardy tranzistorů. S nároky na technologii rostou i nároky na testování.

Ačkoliv se jedná řešení NP-úplného problému, představují SAT řešiče praktický, pohodlný a velice univerzální nástroj, který lze aplikovat i při návrhu integrovaných obvodů a jejich testování. V této práci se zabývám úpravou a použitím řešiče pro obvody s architekturou RAS, výsledkem je upravená knihovna a aplikace pro generování testů. 

\end{introduction}

\chapter{Cíl práce}
Cílem bakalářské práce bylo navrhnout, implementovat a otestovat, příp. experimentálně vyhodnotit nový přístup k generování komprimovaného testu pro číslicové obvody s RAS architekturou založený na pseudo-booleovské optimalizaci vzdálenosti mezi testovacími vektory a odezvou. V rámci tohoto úkolu byl zapracován řešič Minisat{\footnotesize +} jako knihovna do frameworku LogSynth.
\section*{Existující řešení}
Komprese testu je kvůli svým výhodám obvyklý postup a existuje řada možných způsobů, jak kompresi provést, přičemž obvykle pracují se standardní architekturou scan-chain a předkládané řešení pro architekturu RAS je zcela nové a řadí ke kompresním metodám založených na podobnosti vektorů. 

Co se použitých technologií týče, dostupnách SAT řešičů (včetně PBO) existuje několik\footnote{viz http://www.satlive.org/solvers/}, původní  DPLL\footnote{Davis–Putnam–Logemann–Loveland} algoritmus vznikl již v roce 1962, a většina novějších řešičů je na tomto algoritmu stále založena, přičemž modifikují heuristiku. Velký rozvoj nastal teprve po roce 2001 po publikaci článku \cite{moskewicz2001chaff} a řešiče Chaff na Princeton University. 

Na téma aplikace pseudo-booleovské optimalizace na výpočet testovacích vektorů, existuje práce \cite{balcarek}, která se zabývá optimalizací z hlediska maximalizace počtu neurčených bitů v testovacích vektorech pro RESPIN architekturu. 
\section*{Analýza požadavků} 
\subsection*{Funkční požadavky}
Funkční požadavky popisují nároky na funkce softwarového díla (co má program dělat). Ze zadání bakalářské práce a konzultaci s vedoucím jsem vyvodil následující požadavky:
\begin{itemize}
	\item Implementace nového algoritmu ATPG pro RAS architekturu
	\item Program spustitelný z příkazové řádky s parametry a funkcemi obdobnými jako modul ATPG z frameworku
\end{itemize}
\subsection*{Nefunkční požadavky}
Nefunkční požadavky popisují ostatní požadavky na systém (jak to má program dělat)
\begin{itemize}
	\item Využítí řešiče MiniSAT+ ve formě knihovny
	\item Implementace za použití a v rámci frameworku LogSynth, z čehož dále vyplývá
	\begin{itemize}
		\item Použití jazyka C++
		\item Možnost kompilace jak pod systémem Windows, tak i pod Linuxem
	\end{itemize}
\end{itemize}

\chapter{Testování integrovaných obvodů}
\section{Výroba integrovaných obvodů}
Dle \cite{ababei} a \cite{mitsp01} se obvyklý postup vývoje integrovaných obvodů skládá z následujících činností: 
\begin{enumerate}
	\item Návrh
	\begin{itemize}
		\item Funkce obvodu je popsána v jazyce typu VHDL či Verilog.
		\item Proběhne verifikace, tj. testování správné funkce na logické úrovni a syntéza obvodu (převod do hradel)
	\end{itemize} 
	\item Tvorba automatizovaného testu 
	\begin{itemize} 
		\item Algoritmicky je připravena sada testovacích vstupů pro obvod  (tzv. testovacích vektorů).
	\end{itemize}
	\item Výroba čipu
	\item Testování
	\begin{itemize} 
		\item Čip je připojen a otestován pomocí ATE: na vstupy obvodu jsou posílány testovací vektory a odezva (výstup) obvodu je porovnávána s teoretickou (správnou) odezvou 
	\end{itemize}
	\item Analýza
	\begin{itemize} 
		\item Výstup z testování je použit ke kontrole kvality (jde rozhodnout, zda daný čip je vadný či nikoliv) a též ke kontrole a optimalizaci předchozích kroků
	\end{itemize}
	
\end{enumerate}
\section{Motivace k testování, terminologie a stuck-at model}
Na ose integrovaný obvod, deska (např. grafická karta, základní deska,...), zařízení (PC, ...) se celkem logicky ukazuje, že ekonomicky nejvýhodnější je provádět testování už na úrovni integrovaných obvodů, neboť testování o každou úrovneň výše je přibližně desetkrát dražší (tzv. pravidlo deseti).

Při výrobě integrovaných obvodů dochází vinou různých vlivů jako např. nedokonalost výrobní technologie, nečistoty či fyzikální procesy k tvorbě defektů. Reprezentace defektu na úrovni hradel se nazývá porucha, přičemž častým typem defektů jsou přerušené či zkratované vedení signálu. K testování se používá tzv. stuck-at model, ve kterém jsou poruchami signály s trvalou hodnotou 1 (stuck-at-one) či 0 (stuck-at-0) na vstupech a výstupech hradel či na větveních. V daném modelu se nejčastěji též předpokládá současná přítomnost pouze jedné stuck-at poruchy v obvodu.   

\section{Jak testovat?}
\begin{figure}[t]
	\includegraphics[width=0.8\textwidth]{includes/testing}
	\centering
	\caption[Testování obvodu.]{Testování obvodu. Převzato z \cite{ababei}.}
\end{figure}
\begin{figure}[h]
	
	\includegraphics[width=\textwidth]{includes/checkpoint_theorem}
	\centering
	\caption[Poruchy v obvodu.]{\label{includes/obr_checkpoint_theorem} Jaké poruchy je nutné testovat - příklad. Kompletní a redukovaná množina poruch pro úplný test daného obvodu.  $\textrm{t}_1$ = stuck-at-1, $\textrm{t}_0$ = stuck-at-0.   Adaptováno z \cite{mitsp02}.}
\end{figure}
Mějme kombinační obvod skládájící se z hradel a v něm stuck-at poruchu. Vstupy obvodu označme jako PI\footnote{primary inputs}, výstupy jako PO\footnote{primary outputs}. Testování poruchy spočívá v nalezení takového ohodnocení PI, že dojde k
\begin{itemize}
	\item  excitaci poruchy = na místo se stuck-at-0 je přivedena 1 a naopak
	\item propagaci poruchy na PO = je "zcitlivěna" cesta od místa poruchy k PO tak, že porucha projde až na výstup obvodu, tj. pro daný vstup se liší výstupy obvodu s poruchou a bez poruchy
\end{itemize}
Smysl propagace je znázorňen na Obr. \ref{obr_propagace}.

Daný problém tedy spočívá v nalezení testovacího vektoru pro danou poruchu a obecně v nalezení množiny testovacích vektorů, jejichž aplikace na obvod  otestují co nejvíce možných poruch (je dosaženo požadované pokrytí). Hledat testovací vektor pro zadanou poruchu je možné pomocí několika různých algoritmů, přičemž nás dále bude zajímat především algoritmus založený na hledání splnitelnosti booleovské formule, tzv. SAT z anglického satisfiability problem.
\begin{figure}[h]
	
	\includegraphics[width=\textwidth]{includes/propagace}
	\centering
	\caption[Excitace a propagace poruchy.]{\label{obr_propagace} Excitace a propagace poruchy v případě jednoduchého hradla. Značení výstupu je: bez-poruchy/s-poruchou. S-a-1 = stuck-at-1, tj. tento signál je v bodě poruchy trvale připojen na 1. Adaptováno z \cite{mitsp02}.}
\end{figure}
\section{Hledání testovacích vektorů pomocí SAT}
\subsection*{SAT aneb Boolean satisfiability problem}
Mějme zadaný booleovský výraz (formuli) tvořený proměnnými a logickými operacemi (např. or, and, negace). Problém splnitelnosti booleovské formule označuje hledání takového ohodnocení proměnných, že výsledný výraz je pravdivý. SAT je NP-úplný problém, nicméně existují algoritmy, které ho řeší poměrně efektivně, přičemž většina dnešních SAT solverů (řešičů) ho řeší v tzv. CNF-SAT podobě, kdy tyto algoritmy pracují s výrazy v konjunktivní normální formě. Přejděme k definicím z \cite{minisatp}:
\\

\begin{description}
	\item [Problém SAT] Logická formule je v \textbf{konjunktivní normální formě}, pokud se jedná o konjunkci disjunkcí literálů. Literálem se myslí $x$ či negace $\neg x$, kde $x$ je booleovská proměnná. Jednotlivé disjunkce se označují jako klauzule. Problém splnitelnosti booleovské formule či SAT spočívá v nalezení takového ohodnocení proměnných, že celkový výrok je pravdivý, což je ekvivalentní tomu, že při takovém ohodnocení se v každé klauzuli nachází alespoň jeden pravdivý literál.
	\item [Pseudo-booleovská optimalizace] Pseudo-booleovská podmínka je nerovnost typu $C_{0}p_{0}+C_{1}p_{1}+\ldots+C_{n-1}p_{n-1}\geq C_{n}$, kde pro všechna $i$ je $p_i$ literál a $C_i$ celočíselný koeficient, přičemž pravdivý literál je vyhodnocen jako 1 a nepravdivý jako 0. Výraz z levé strany rovnice, tj. lineární kombinace literálů má význam funkce. PB optimalizace spočívá v nalezení ohodnocení, pří kterém je zadaná množina PB podmínek pravdivá a pro které je hodnota zadané (lineární) minimalizační funkce minimální. \textit{Poznámka:} Pro $C_i=1$ pro všechna $i$ je PB podmínka ekvivalentní klauzuli v CNF.
\end{description}

\subsubsection*{Konjunktivní normální forma}
Každou booleovskou formuli lze převést do konjunktivní normální formy, což si zde předvedeme na výrazu $\textrm{A} \land \left(\textrm{B} \Leftrightarrow \textrm{C}\right)$
\begin{table}[h!]
	\centering
	\begin{tabular}{|c|c|c|c|}
		\hline 
		A & B & C & $\textrm{A} \land \left(\textrm{B} \Leftrightarrow \textrm{C}\right)$ \\ 
		\hline 
		0& 0 &0  &0  \\ 
		\hline 
		0&0  &1  &0  \\ 
		\hline 
		0&1  &0  & 0 \\ 
		\hline 
		0& 1 & 1 &  0\\ 
		\hline 
		1& 0 & 0 & 1 \\ 
		\hline 
		1& 0 & 1 & 0 \\ 
		\hline 
		1& 1 & 0 & 0 \\ 
		\hline 
		1& 1 & 1 &  1\\ 
		\hline 
	\end{tabular} 
	\caption[Pravdivostní tabulka - příklad.]{Pravdivostní tabulka pro formuli $\textrm{A} \land \left(\textrm{B} \Leftrightarrow \textrm{C}\right)$.}
	\label{tab_cnf}
\end{table}
Postup transformace výroku do CNF (či KNF):
\begin{enumerate}
	\item Sestavím si tabulku pravdivostních hodnot.
	\item Pro řádky, ve kterých je formule nepravdivá sestavím disjunkci negací původních elementárních proměnných.
	\item Sestavím konjunkci těchto disjunkcí.
\end{enumerate}
Z tabulky pro výraz $\textrm{A} \land \left(\textrm{B} \Leftrightarrow \textrm{C}\right)$ (viz tab. \ref{tab_cnf}) vidíme, že platí
\begin{align*}
\textrm{A}\land\left(\textrm{B}\Leftrightarrow\textrm{C}\right) & =\left(\textrm{A}\lor\textrm{B}\lor\textrm{C}\right)\land\left(\neg\textrm{A}\lor\textrm{B}\lor\neg\textrm{C}\right)\land\\
& \left(\textrm{A}\lor\neg\textrm{B}\lor\textrm{C}\right)\land\left(\textrm{A}\lor\neg\textrm{B}\lor\neg\textrm{C}\right)\land\\
& \left(\textrm{\ensuremath{\neg}A}\lor\textrm{B}\lor\neg\textrm{C}\right)\land\left(\neg\textrm{A}\lor\neg\textrm{B}\lor\textrm{C}\right)
\end{align*}
\subsubsection*{Tseitinova transformace}
Pro převod kombinačních obvodů do CNF se používá Tseitinova\footnote{V originále \foreignlanguage{russian}{Цейтин Г. С.} (autor)} transformace. Hradla v obvodu jsou popsána charakteristickými funkcemi v CNF a jejich vzájemným vynásobením je získána CNF pro celý obvod. Transformace je lineární s počtem hradel, avšak zvyšuje počet použitých proměnných. Příkladem charakteristické funkce v konjunktivní normální formě je funkce $\chi_F = (F'+x).(F'+y).(F+x'+y')$ pro hradlo $F=\textrm{AND}(x,y)$. Charakteristická funkce popisuje správnou funkci hradla, tj. zde platí $\chi_F = 1$ pro ohodnocení $\{F,x,y\} = \{1,1,1\}$, $\{0,1,0\}$, $\{0,0,1\}$ a $\{0,0,0\}$.

\subsection*{Generování testovacích vektorů pomocí SAT} \label{cr_Miter}
Hledání testovacího vektoru pro zadanou poruchu lze jednoduše zformulovat jako problém pro SAT následujícím postupem:
\begin{enumerate}
	\item Vezmu bezporuchový obvod
	\item Vezmu obvod s poruchou
	\item odpovídající PO obvodů spojím XOR hradlem
	\item výstupy XOR hradel spojím do OR hradla
	\begin{itemize}
		\item výstup bude 1, liší li se alespoň jeden výstup poruchového a bezporuchového obvodu, tj. pokud se porucha propaguje na PO
	\end{itemize}
	\item Celý obvod popíšu pomocí charakteristických funkcí všech hradel v CNF
	\item Tyto CNF spojím do jedné formule, kterou předám SAT solveru
	\item Pokud je CNF splnitelná, řešením SAT problému je testovací vektor pro danou poruchu
\end{enumerate}
Postup je pro jednoduchý obvod znázorněn na obr. \ref{cr_Miter}, výraz \ref{eq:CNF} pak představuje výsledné CNF.
\begin{figure}[h]
	
	\includegraphics[width=\textwidth]{includes/miter}
	\centering
	\caption[Obvod pro výpočet SAT.]{Obvod pro výpočet SAT (Pro více výstupů obvodu by byly výstupy z XOR hradel spojeny do OR hradla). Bezporuchový obvod (v rámečku) je spojen přes XOR hradlo s obvodem s poruchou. Platí $\textrm{Y} = 1$ pokud je porucha detekována. Adaptováno z \cite{mitsp03}.}
	\label{obr_miter}
\end{figure}
% Náhled zdrojového kódu pro odstavec 0




% Náhled zdrojového kódu pro odstavec 1

\begin{align}
\left(\textrm{D'}+\textrm{A}\right)\cdot\left(\textrm{D'}+\textrm{B}\right)\cdot\left(\textrm{D}+\textrm{A'}+\textrm{B'}\right)\cdot\nonumber \\
\left(\textrm{C}+\textrm{E}\right)\cdot\left(\textrm{C'}+\textrm{E}'\right)\cdot\nonumber \\
\left(\textrm{X}+\textrm{D'}\right)\cdot\left(\textrm{X}+\textrm{E'}\right)\cdot\left(\textrm{X'}+\textrm{D}+\textrm{E}\right)\cdot\nonumber \\
\left(\textrm{D}_{\textrm{F}}\right)\cdot\label{eq:CNF}\\
\left(\textrm{X}_{\textrm{F}}+\textrm{\ensuremath{\textrm{D}_{\textrm{F}}}'}\right)\cdot\left(\textrm{X}_{\textrm{F}}+\textrm{E'}\right)\cdot\left(\textrm{X'}+\textrm{D}_{\textrm{F}}+\textrm{E}\right)\cdot\nonumber \\
\left(\textrm{C}+\textrm{E}\right)\cdot\left(\textrm{C'}+\textrm{E'}\right)\cdot\nonumber \\
\left(\textrm{X'}+\textrm{X}_{\textrm{F}}+\textrm{Y}\right)\cdot\left(\textrm{X}+\textrm{X}_{\textrm{F}}'+\textrm{Y}\right)\cdot\left(\textrm{X}+\textrm{X}_{\textrm{F}}+\textrm{Y'}\right)\cdot\left(\textrm{X'}+\textrm{X}_{\textrm{F}}'+\textrm{Y'}\right)\cdot\textrm{Y}\nonumber 
\end{align}



\section{Testování sekvenčních obvodů}
Testování kombinačních obvodů sestává z aplikace testovacích vektorů, které excitují a propagují danou poruchu. V případě sekvenčních obvodů je situace složitější, neboť obecně stav a chování obvodu závisí na jeho vnitřním stavu, což problém hledání testovacího vektoru značně zesložiťuje (\cite{mitsp04}). Možným a používaným řešením je převedení daného sekvenčního obvodu na kombinační, resp. využití jeho rozdělení na kombinační a DFF část a následné testování této kombinační části, přičemž množina vstupů (výstupů) obvodu je nyní tvořena jak vstupy (výstupy) původního obvodu, označovanými jako primární vstupy (výstupy), tak i vstupy (výstupy) z klopných obvodů, tzv. pseudoprimárních vstupů (výstupů), jak je znázorněno na obr. \ref{obr_sekvencni}.
\begin{figure}[h]	
	\hspace*{-2cm}\includegraphics[width=0.9\textwidth]{includes/Sekvencni_obvod}
	\centering
	\caption[Model sekvenčního obvodu.]{\label{obr_sekvencni} Model sekvenčního obvodu. Převzato z \cite{mitsp08}.}
\end{figure}
Tímto postupem se problém převedl na testování kombinačního obvodu, které je jednodušší ale zároveň i na problém, jak dostat do DFF data pro PPI.
\section{Architektura RAS a komprese testu}
Architektura Random Access Scan (RAS) řeší tento problém  jednoduše tím, že jednotlivé buňky paměti (klopné obvody) jsou přímo adresovatelné. Pokud má obvod  $n$ klopných obvodů, pak adresa má velikost $\log_2 n$ bitů a na aplikaci jednoho testovacího vektoru obecně připadá $n.\log_2 n$ bitů. RAS architektura avšak umožňuje měnit pouze potřebné bity. Po aplikaci funkčních hodin se totiž v klopných obvodech nachází odezva na předchozí testovací vektor \cite{mitsp11} a minimalizací Hammingovy vzdálenosti mezi odezvou a následujícím testovacím vektorem tudíž dosahnu komprese testu, tj. zmenšení objemu zasílaných dat (či zkrácení doby testování). Obvykle používaný algoritmus komprese pro RAS obvody se skládá z
\begin{enumerate}
	\item Vygenerování testovacích vektorů
	\item Změny pořadí testovacích vektorů tak, aby se minimalizovala Hammingova vzdálenost pro celý test
\end{enumerate}
Tento problém je ekvivalentní s problémem obchodního cestujícího v jeho asymetrické variantě. Architektura RAS je znázorněna na obr. \ref{obr_RAS} a princip komprese pro RAS obvod, tj. nutnost nasunutí pouze změněných bitů v PPI, na obr. \ref{obr_RAS_komprese}. 
\\
\\

\begin{figure}[h]
	\hspace*{2.5cm}\includegraphics[width=0.9\textwidth]{includes/RAS_architecture}
	\centering
	\caption[Architektura RAS]{\label{obr_RAS} Architektura RAS. Tato architektura umožňuje přímý zápis do klopných obvodů pomocí $\log_2 n$ adresních bitů, kde $n$ je počet klopných obvodů. Převzato z \cite{baikRAS}.}
\end{figure}

\begin{figure}[b]
	\includegraphics[width=0.9\textwidth]{includes/RAS}
	\centering
	\caption[Komprese v architektuře RAS.]{\label{obr_RAS_komprese} Architektura RAS. Znázornění možnosti měnit jen některé bity. Převzato z \cite{baikRAS}.}
\end{figure}

\chapter{Navrhovaný algoritmus} \label{chapter:alg}
\subsection*{Komprese testu pro RAS pomocí pseudo-booleovské optimalizace}
V této práci jsme se pokusili o jiný přístup, a to o hledání testovacích vektorů minimalizujících Hammingovu vzdálenost již při řešení SAT. Algoritmus spočívá v tom, že se při hledání testovacích vektorů pomocí SAT přidá PBO podmínka s cílem minimalizovat bitovou (Hammingovu) vzdálenost od předchozí odezvy pro PPI a od předchozího testovacího vektoru u PI. Minimum se hledá přes všechny zbývající poruchy. Níže je algoritmus popsán v pseudokódu:
\\

%\subsection*{Algoritmus hledání testovacích vektorů} \label{cl_RASAlgoritmus}
\begin{algorithm}[H]
	Vygeneruj seznam poruch\;
	Vyber poruchu, vygeneruj testovací vektor a poruchy nalezené tímto vektorem odeber ze seznamu\;
	\BlankLine
	\While{seznam poruch je neprázdný}{
		\ForEach{porucha v seznamu} {
			vygeneruj testovací vektor s nejmenší vzdáleností pro RAS pomocí SAT s PBO
		}
		vyber testovací vektor s nejmenší vzdáleností pro přes všechny zbývající poruchy\;
		poruchy nalezené tímto vektorem odeber ze seznamu\;
	}
	%	\caption{How to write algorithms}
\end{algorithm}
\subsection*{Minimalizace vzdálenosti pomocí PBO}
PBO lze využít k minimalizaci vzdálenosti vektorů hledaných pomocí SAT. Přepis CNF klauzulí do PB-podmínek je přímočarý; Podmínku minimalizující vzdálenost hledaného vektoru lze zadat zvolením koeficientů v minimalizační funkci: pokud chceme, aby hledaný literál $p_i$ nabýval hodnoty 1, volíme koeficient $C_i=-1$ v objektivní funkci a podobně pokud chceme, aby $p_i$ nabýval hodnoty 0, za koeficient volíme $C_i = -1$. Nalezený literál, jehož hodnota je odlišná od cílové hodnoty zvyšuje hodnotu objektivní funkce, přičemž SAT solver hledá minimum, tj. v důsledku co nejméně vzdálený vektor. Příklad je zobrazen v tab. \ref{tab_pbo}. Zde hledáme vektor $x_{0}x_{1}x_{2}x_{3}x_{4}$ tak, aby byl co nejméně vzdálený vektoru 10110.
\begin{table}[b]
	\begin{centering}
		\begin{tabular}{|>{\centering}p{5cm}|c|c|c|c|c|}
			\hline 
			literál & $x_{0}$ & $x_{1}$ & $x_{2}$ & $x_{3}$ & $x_{4}$\tabularnewline
			\hline 
			cílová hodnota & 1 & 0 & 1 & 1 & 0\tabularnewline
			\hline 
			funkce pro minimalizaci solverem& \multicolumn{5}{c|}{$-x_{0}+x_{1}-x_{2}-x_{3}+x_4$}\tabularnewline
			\hline 
		\end{tabular}
		\par\end{centering}
	\caption[Minimalizační funkce pro PBO - příklad.]{\label{tab_pbo}P\v{r}íklad \uv{goal} funkce minimalizující vzdálenost pro vektor hledaný SAT. Hodnota objektivní funkce je zde rovna mínus třem plus počtu změněných bitů.}
\end{table}

\chapter{Analýza}
\section {LogSynth}
LogSynth je framework pro manipulaci s logickými funkcemi vyvíjený na Katedře číslicového návrhu FIT ČVUT. Jádrem frameworku jsou moduly Kernel-PLA a Kernel-multilevel, které definují datové typy a třídy umožňující načtení a práci s obvody tvořenými sítí vzájemně propojených hradel. Další z mnoha modulů, modul ATPG, je určen pro hledání testovacích vektorů pomocí SAT a obsahuje funkcionalitu nutnou pro generování množiny poruch pro daný obvod, CNF pro danou poruchu v obvodu a pro simulaci testovacího vektoru a následné určené poruch detekovaných tímto vektorem.
Základní rozhraní pro práci s logickými obvody je v použitém frameworku LogSynth tvořeno třídami \lstinline|Network| a \verb|ATPG_alg|. Třída \lstinline|Network| reprezentuje celý logický obvod tvořený hradly (popsané objekty třídy \verb|Node|), které jsou vzájemně propojené \uv{dráty} (třída \verb|Signal|). Hradlo (\verb|Node|) je popsáno objektem třídy \verb|PLA|, což je tabulka popisující výstupy hradla pro dané vstupy. Třída \verb|Cube| pak reprezentuje bitový vektor. 


Zde je popis použitých metod z Kernel-multilevel:
\begin{figure}[h]	
	\includegraphics[width=\textwidth]{includes/LogSynthCD}
	\centering
	\caption[Diagram použitých modulů z LogSynth.]{Zjednodušený diagram tříd modulů ATPG, Kernel-multilevel a Kernel-PLA frameworku LogSynth.}
\end{figure}
\begin{itemize}
	\item \verb|void Network::LoadBlif(string filename)|, \\\verb|void Network::LoadBench(string filename)| -- načte vstupní soubor (logický obvod) ve formátu .blif či .bench do objektu
	\item \verb|int Network::getDFFs()|,\\
	\verb|int Network::inputs()|,\\
	\verb|int Network::outputs()| -- vrátí počet DFF, PI, PO v načteném obvodu
	\item \verb|SoPLA* Network::ToCNF(void) const| -- Zkonvertuje daný obvod do CNF (pro předání do řešiče)
	\item \verb|vector<Literal> Network::Simulate(const Cube &t, Fault *flt, bool all)| -- simulace testovacího vektoru v daném obvodu
\end{itemize}
Modul ATPG frameworku obsahuje funkcionalitu pro generátor ATPG, koncentrující se převážně ve třídě \verb|ATPG_alg|. Použité metody: 
\begin{itemize} 
	\item \verb|ATPG_alg::ATPG_alg (Network& network)| -- vygeneruje instanci ATPG pro daný obvod
	\item \verb|FaultList& ATPG_alg::FaultListRef()| reprezentuje seznam poruch pro daný obvod
	\item \verb|Network *ATPG_alg::GenerateMiter(SA_Fault *flt)| vygeneruje obvod pro testování pomocí SAT (viz. \ref{cr_Miter}) 
	\item \verb|void ATPG_alg::Drop(list<TestPattern>::iterator p_it)| detekuje poruchy nalezené daným testovacím vektorem a označí je v seznamu poruch
	
\end{itemize}
Framework je v práci využit se souhlasem autora/autorů.
\section {Minisat\texttt{+}}
Minisat\texttt{+} je SAT-PBO řešič od autorů Niklase Eéna a Niklase Sörenssona. Jedná se o pozměněný řešič MiniSat od stejných autorů, respektive o nástavbu, převádějící PB podmínky na problém SAT a využívající Minisat jako backend. Program se zdrojovými kódy je dostupný volně ke stažení na webových stránkách autorů\footnote{\href{http://minisat.se/MiniSat+.html}{http://minisat.se/MiniSat+.html}}. Webová stránka ani kód samotný (stažený z těchto stránek) neobsahuje licenční ujednání, nicméně jeden z autorů kód umístil i na GitHub\footnote{\href{https://github.com/niklasso/minisatp}{https://github.com/niklasso/minisatp}}, kde jako licenční ujednání uvedl licenci MIT.
\begin{figure}[h]	
	\includegraphics[width=0.6\textwidth]{includes/minisatp_cygwin_cut}
	\centering
	\caption[Minisat+ pod Cygwin.]{\label{obr_minisatp_cygwin} Minisat+ spuštěný v prostředí Cygwin pod Windows. Spuštění a) bez parametru, b) se souborem garden9x9.opb z adresáře Examples.}
\end{figure}

\begin{figure}[h]	
	\includegraphics[width=\textwidth]{includes/minisatp_format2}
	\centering
	\caption[Původní zdrojový formát pro Minisat+.]{\label{obr_minisatp_format} Formát zdrojového souboru pro Minisat+ na příkladu garden9x9.opb z adresáře Examples. Je zde vidět funkce pro minimalizaci (objektivní funkce) a CNF klauzule. (Soubor na obrázku není celý.)}
\end{figure}
Zdrojové kódy jsou určené pro kompilátor gcc/g++ pod linuxem a součástí archivu s programem je i spustitelný binární soubor pro linux a několik ukázkových souborů. Na obr. \ref{obr_minisatp_cygwin} je běh programu v prostředí Cygwin a na \ref{obr_minisatp_format} je ukázka zdrojového formátu, tj. zadání PBO problému.



Minisat+ se skládá z části převádějící PB podmínky do CNF a z SAT řešiče Minisat. Pro převod PB podmínek do CNF se využívá lineární převoditelnost logických obvodů do CNF, přičemž PB podmínku lze do logického obvod u převést pomocí (\cite{minisatp}):
\begin{itemize}
	\item BDD (Binary decision diagramů)
	\item sčítaček
	\item třídících sítí
\end{itemize}
Minimalizace objektivní funkce je realizována iterativním voláním řešiče - v první iteraci je vyhodnocena její hodnota $f(p_{i})=k$ a v následném volání je přidána PB podmínka $f(p_{i})< k$. Pokud řešič vrátí nesplnitelnost, je $k$ minimum, v opačném případě je řešič volán znova s podmínkou se zmenšenou hodnotou $k$.
Jako řešič SAT je použit Minisat, jehož algoritmus je popsán v článku \cite{minisat_paper}.

\iffalse
\SetKwFor{Loop}{loop}{}{endloop}
\begin{algorithm}[h]
	\Loop{}{propagate()\tcc*{Odvoď hodnoty dalších proměnných z aktuálního ohodnocení a klauzulí.}
		\eIf{nenastane konflikt}{
			\eIf{všechny proměnné jsou ohodnocené}{return SATISFIABLE\;}{decide()\tcc*{Vyber neohodnocenou proměnnou a ohodnoť ji.}}}{
			analyze()\tcc*{Přidej k CNF klauzuli zabraňující konfliktnímu ohodnocení.}
			\eIf {nastane konflikt na nejvyšší úrovni ohodnocování}{return UNSATISFIABLE\;}{
				backtrack()\tcc*{backtracking z konfliktního ohodnocení}}
		}
	}
\end{algorithm}
\fi
Zdrojový kód Minisat+ bohužel nemá k disposici dokumentaci a kód obsahuje poměrně málo komentářů. Z kódu programu ve funkci main však bylo možné vytvořit si představu o fungování tříd PbSolver, Solver a MiniSat. V tab. \ref{tab_minisatp} je sestaven popis nejdůležitějších programových modulů.

Z analýzy dále vyplynulo, že samotný řešič, reprezentovaný objektem třídy PbSolver je ovládán metodami a proměnnými:

\begin{itemize}
	\item \verb|void PbSolver::allocConstrs(int n_vars, int n_constrs)| -- alokuje datové struktury pro řešení problému o daném počtu proměnných a PB podmínek.
	\item \verb|int PbSolver::getVar(const char *name)| - alokuje v solveru booleovskou proměnnou s daným indexem
	\item \verb|bool PbSolver::addConstr| \\
	\verb|(const vec<Lit>& ps, const vec<Int>& Cs, Int rhs, int ineq)| - přidá do solveru danou PB podmínku
	\item \verb|void PbSolver::addGoal(const vec<Lit>& ps, const vec<Int>& Cs)| - přidá do solveru danou objektivní funkci pro minimalizaci
	\item \verb|int PbSolver::solve(solve_Command cmd = sc_Minimize)| - řeší zadaný problém
	\item \verb|Int PbSolver::best_goalvalue| - Int\_MAX v případě UNSAT či hodnota objektivní funkce pro nalezené (minimální) řešení
	\item \verb|vec<bool> PbSolver::best_model| - nalezené nejlepší řešení problému
\end{itemize}
Heuristika solveru (např. výběr metody převodu zadání do CNF) je ovládána pomocí statických proměnných a solver též využívá několik statických datových proměnných pro urychlení výpočtů v programovém modulu Hardware\_clausify.



% Náhled zdrojového kódu pro odstavec 0

% Náhled zdrojového kódu pro odstavec 2

\begin{table}
	\begin{centering}
		\begin{tabular}{|>{\centering}p{6cm}|>{\centering}p{6cm}|}
			\hline 
			Programový modul  & Popis\tabularnewline
			\hline 
			\hline 
			VecAlloc, StackAlloc  & alokátory pam\v{e}ti\tabularnewline
			\hline 
			Map, Heap  & definice datových typ\r{u}\tabularnewline
			\hline 
			VecMaps  & optimalizovaný vektor bool hodnot;
			
			VecMap: vektor; DeckMap: vektor s $\pm$ indexy\tabularnewline
			\hline 
			Int, SolverTypes, Global  & definice datových typ\r{u}:\v{c}íslo, booleovská prom\v{e}nná, literál,lbool
			(true, false, undef, error)\tabularnewline
			\hline 
			FEnv  & reprezentace logických výraz\r{u} a operací\tabularnewline
			\hline 
			Solver  & interface pro backend SAT solver\tabularnewline
			\hline 
			MiniSat, SatELite  & t\v{r}ída backend SAT solveru\tabularnewline
			\hline 
			PbSolver  & definice t\v{r}ídy Linear (uložení PB podmínky); t\v{r}ída PbSolver
			(PBO solver)\tabularnewline
			\hline 
			Hardware a Hardware\_X 
			
			PbSolver\_convert a PbSolver\_convertY & funkce pro p\v{r}evod PB podmínek do CNF; X=adders, clausify,sorters;
			Y=Add, Bdd, Sort\tabularnewline
			\hline 
		\end{tabular}
		\par\end{centering}
	\caption{\label{tab_minisatp}Popis programových modul\r{u} ze zdrojového kódu
		Minisat+.}
\end{table}



\chapter{Realizace}
V této kapitole popisuji implementaci algoritmu z kapitoly \ref{chapter:alg} využívající framework LogSynth a knihovnu Minisat+. Minisat+ (původně aplikace) bylo nutné převést do formy knihovny a vytvořit rozhraní pro zadávání a řešení PB problémů. Toto rozhraní je posléze využito z C++ aplikace pro příkazový řádek a napojeno na jádro frameworku Logsynth, které poskytuje funkcionalitu pro práci s logickými obvody. Ovládání programu je řešeno parametry (\uv{přepínači}), zadávanými z příkazové řádky, jejichž struktura je převzata z modulu ATPG frameworku.
\section{Volba technologie}
V návaznosti na fakt, že Minisat+ i LogSynth jsou napsané v C++ bylo ve vývoji pokračováno též v jazyce C++. Využito bylo vývojové prostředí Visual Studio.
\section{Převod Minisat+ na knihovnu}
Původní kód Minisat+ (program) bylo poměrně jednoduché importovat do Visual Studia a upravit na statickou knihovnu, neboť nekompatibilita s kompilátorem ve Windows byla způsobena převážně POSIX voláními ve funkci \verb|main| programu. Po odstranění funkce \verb|main| zbyly převážně třídy pracující s daty, avšak výsledné funkce přišly o možnost přerušovat (dlouhé) výpočty pomocí Ctrl-C s vypsáním dosud nejlepšího nalezeného řešení.
\subsection*{Změny v kódu a interface}
Analýzou zdrojového kódu Minisat+ bylo zjištěno, že hlavní částí řešiče je třída \verb|PbSolver|. Objekt této třídy slouží k definici zadání daného PB problému a hledání řešení. Dále však bylo zjištěno, že chod PbSolveru závisí na řadě globálních proměnných. Tyto bylo možné rozdělit na dvě kategorie. První část jsou proměnné s předponou \texttt{opt\_}, které v původním programu sloužily pro předávání speciálních parametrů do řešiče. Tyto proměnné jsou zmíněny v tab. \ref{tab:opt}. Druhou část posléze byly globální proměnné sloužící jako sdílené datové struktury mezi částmi řešiče. Využití globálních proměnných zřejmě bylo zvoleno kvůli optimalizaci rychlosti. Zde se jedná statické proměnné třídy \verb|Clausifier|, tj. o\\ \\ \verb|CMap<int> Clausifier::occ|\\ \verb|CMap<Var> Clausifier::vmap|\\ \verb|CMap<Lit,true> Clausifier::vmapp|\\ 


% Náhled zdrojového kódu pro odstavec 0
\begin{table}
	\makebox[\textwidth][c]{
		\begin{tabular}{|c|c|c|c|c|}
			\hline 
			Globální prom\v{e}nná & Popis & 1 & 2 &3 \tabularnewline
			\hline 
			\hline 
			\texttt{opt\_satlive} & zm\v{e}na tvaru výpis\r{u} pro SAT competition  & ne & ne & \texttt{true}\tabularnewline
			\hline 
			\texttt{opt\_ansi} & ANSI kódy ve výpisech & ne & ne & \texttt{true}\tabularnewline
			\hline 
			\texttt{opt\_cnf} & soubor pro výpis v CNF & ano & ne & \texttt{NULL}\tabularnewline
			\hline 
			\texttt{opt\_verbosity} & nastavení množství výpis\r{u} & ano & ne & \texttt{1}\tabularnewline
			\hline 
			\texttt{opt\_try} & nastavení parsování vstup\r{u} & ne & ne & \texttt{false}\tabularnewline
			\hline 
			\texttt{opt\_solver} & volba backend solveru & ano & ne & \texttt{st\_MiniSat}\tabularnewline
			\hline 
			\texttt{opt\_convert} & zp\r{u}sob p\v{r}evodu PB podmínek do CNF & ano & ano & \texttt{ct\_Mixed}\tabularnewline
			\hline 
			\texttt{opt\_convert\_goal} & zp\r{u}sob p\v{r}evodu goal funkce do CNF & ano & ne & \texttt{ct\_Undef}\tabularnewline
			\hline 
			\texttt{opt\_convert\_weak} & ekvivalence místo implikací p\v{r}i p\v{r}evodu klauzulí & ano & ne & \texttt{true}\tabularnewline
			\hline 
			\texttt{opt\_bdd\_thres} & práh preference BDD v mixed módu & ano & ne & \texttt{3.0}\tabularnewline
			\hline 
			\texttt{opt\_sort\_thres} & práh preference t\v{r}ídících sítí v mixed módu  & ano & ano & \texttt{20.0}\tabularnewline
			\hline 
			\texttt{opt\_goal\_bias} & násobící konstanta pro opt\_sort\_thres & ano & ne & \texttt{3.0}\tabularnewline
			\hline 
			\texttt{opt\_goal} & po\v{c}áte\v{c}ní hodnota (limit) pro goal funkci & ano & ne & \texttt{Int\_MAX}\tabularnewline
			\hline 
			\texttt{opt\_command} & nastavení módu \v{r}ešení & ne & ne & \texttt{cmd\_Minimize}\tabularnewline
			\hline 
			\texttt{opt\_branch\_pbvars} & omezení heuristiky na p\r{u}vodní prom\v{e}nné & ano & ne & \texttt{false}\tabularnewline
			\hline 
			\texttt{opt\_polarity\_sug} & nastavení polarity SAT v\r{u}\v{c}i goal funkci & ano & ne & \texttt{1}\tabularnewline
			\hline 
			\texttt{opt\_input} & jméno vstupního souboru & ne & ne & \texttt{NULL}\tabularnewline
			\hline 
			\texttt{opt\_result} & jméno výstupního souboru & ne & ne & \texttt{NULL}\tabularnewline
			\hline 
	\end{tabular}}
	\caption[Globální proměnné v původním Minisat+.]{Globální proměnné opt\_XXXXX v Minisat+. 1 = PbSolver závisí na proměnné, 2 = PbSolver může měnit, 3 = Výchozí nastavení.}
	\label{tab:opt}
\end{table}

\noindent a též o globální proměnné z namespace FEnv:
\\ \\
\verb|vec<NodeData> FEnv::nodes| \\
\verb|Map<NodeData, int> FEnv::uniqueness_table| \\
\verb|vec<int> FEnv::stack| \\

Jelikož cílem bylo použít Minisat+ jako knihovnu, bylo nutné při návrhu rozhraní zajistit, aby se pro opakování volání řešiče datové globální proměnné vymazaly. Dalším specifikem bylo, že řešič v původní formě programu nalezená řešení pouze vypisoval na obrazovku a tedy nové rozhraní muselo umožnit předávání nalezených řešení a nikoliv jenom výpis, přičemž řešič PbSolver pracuje ve třech možných módech: minimalizace zadané funkce, hledání prvního řešení (bez minimalizace), hledání všech řešení (bez minimalizace). 

Návrh jsem tedy volil takový, aby
\begin{itemize}
	\item rozhraní odstínilo komplikované vzájemné závislosti programových modulů Minisat+
	\item celé rozhraní řešiče bylo objektové, tj. bez nutnosti práce s globálními parametry
	\item se zjednodušila definice PB podmínek, zejména definice literálů
	\item použití řešiče nemění globální parametry a automaticky resetuje globální datové struktury
	\item řešič podporoval všechny módy, tj. byl schopný vracet 0, 1 i více řešení	
\end{itemize}
V následující části popisuji navržené a využité třídy.
\subsection*{PBLit}
Třída reprezentující literál vynásobený celočíselnou konstantou.

V zadání PB podmínek a minimalizační funkce se vyskytuj výrazy typu 
$k\cdot\textrm{p}\left('\right)$, kde $k$ je celočíselná konstanta a p booleovská proměnná (s případnou negací). Původní složitou registraci jména literálu u objektu třídy \verb|PbSolver| jsem nahradil třídou \verb|PBLit|, jejíž objekty reprezentují celý tento výraz. Popis atributů/metod níže.
% Náhled zdrojového kódu pro odstavec 1
\\

\makebox[\textwidth][c]{
	\begin{tabular}{|>{\centering}p{3cm}|>{\centering}p{3cm}|>{\centering}p{8cm}|}
		\hline 
		Název atributu & Datový typ & Popis\tabularnewline
		\hline 
		\hline 
		\texttt{c} & int & konstanta násobící literál v PB podmínce\tabularnewline
		\hline 
		\texttt{var} & size\_t & \v{c}íslo PB prom\v{e}nné\tabularnewline
		\hline 
		\texttt{neg} & bool & true pokud je prom\v{e}nná v negaci\tabularnewline
		\hline 
\end{tabular}}

% Náhled zdrojového kódu pro odstavec 2
\subsection*{Params}
Touto třídou jsem zakryl původní přístup k globálním parametrům Minisat+. Nepotřebné parametry (tj. \uv{ne} v obou sloupcích v tab. \ref{tab:opt}) jsem mohl zcela vynechat.

Popis atributů/metod níže.
\\

\makebox[\textwidth][c]{
	\begin{tabular}{|>{\centering}p{3cm}|>{\centering}p{3cm}|>{\centering}p{8cm}|}
		\hline 
		Název metody & Návratový typ & Popis\tabularnewline
		\hline 
		\hline 
		\texttt{setDefaults} & \texttt{void} & statická metoda\tabularnewline
		\hline 
		\texttt{setOptVerbosity}, \texttt{getOptVerbosity}, ... & \texttt{void} & statické metody\tabularnewline
		\hline 
\end{tabular}}

\subsection*{Helper}
Třída reprezentující řešení PB problému. Třída využívá návrhový vzor Observer - objekt této třídy se zaregistruje u objektu třídy Solver a pokud je v rámci metody \verb|solve| nalezeno řešení, je zavolána metoda solution, přičemž v atributu \verb|v| se nachází toto řešení. Dle parametrů volání Solveru je možné, že je solution volána 0, 1 i vícekrát. Sekvenční diagram viz obr \ref{fig:seq_diag}.
\\

% Náhled zdrojového kódu pro odstavec 0
\makebox[\textwidth][c]{
	\begin{tabular}{|>{\centering}p{3cm}|>{\centering}p{3cm}|>{\centering}p{8cm}|}
		\hline 
		Název atributu  & Datový typ  & Popis\tabularnewline
		\hline 
		\hline 
		\texttt{values}  & \texttt{vector<bool>}  & vektor s \v{r}ešením\tabularnewline
		\hline 
		\hline 
		Název metody  & Návratový typ  & Popis\tabularnewline
		\hline 
		\hline 
		\texttt{solution} & \texttt{void}  & metoda volána po nalezení \v{r}ešení\tabularnewline
		\hline 
\end{tabular}}


\subsection*{Solver}
Třída reprezentující řešič/zadání PB problému a tvořící adaptér nad originální třídou PbSolver z Minisat+. Třída využívá návrhový vzor Singleton. 

Voláním statické metody \texttt{getInstance} je vrácena reference na singleton objekt. Voláním metody \texttt{init} je specifikován počet proměnných a počet PB podmínek. Následně je možné pracovat s objekty typu \texttt{PBLit} s atributem \texttt{var} v rozsahu 1 až $n$, kde $n$ je počet proměnných předaných konstruktoru Solveru. Levé strany PB podmínek a funkce pro minimalizaci jsou pak určeny jako \texttt{vector<PBLit>}. Jako první je nutné přidat minimalizační funkci pomocí metody \texttt{addGoal} a posléze stejný počet PB podmínek, jako byl určen v konstruktoru. Dalšími parametry při přidání PB podmínky je typ znaménka s možnostmi \texttt{INEQ\_LT} ($<$), \texttt{INEQ\_LE}($\leq$), \texttt{INEQ\_EQ}($=$), \texttt{INEQ\_GE}($\ge$), \texttt{INEQ\_GT}($>$) a celočíselná konstanta na pravé straně podmínky. Metoda \texttt{solve} provede hledání řešení. Jejím parametrem je typ řešení, které se má hledat s možnostmi \texttt{FIND\_ALL} (hledá všechna řešení bez ohledu na objektivní funkci), {FIND\_FIRST} (hledá první řešení bez ohledu na minimalizační funkci), \texttt{FIND\_MINIMIZE} (hledá řešení minimalizující goal funkci). Ukázkový kód se nachází ve výpisu \ref{lst:code}.
\\

\makebox[\textwidth][c]{
	% Náhled zdrojového kódu pro odstavec 0
	
% Náhled zdrojového kódu pro odstavec 3

\begin{tabular}{|>{\centering}p{3cm}|>{\centering}p{3cm}|>{\centering}p{8cm}|}
	\hline 
	Název metody  & Návratový typ  & Popis\tabularnewline
	\hline 
	\hline 
	\texttt{getInstance} & \texttt{Solver\&}& vrací referenci na singleton objekt (statická metoda)\tabularnewline
	\hline 
	\texttt{init} & \texttt{void} & nastavuje solver na daný po\v{c}et prom\v{e}nných a podmínek a provádí
	reset
	
	parametry: \texttt{int n\_vars, n\_constrs}\tabularnewline
	\hline 
	\texttt{addGoal}  & \texttt{void}  & nastaví funkce pro minimalizaci
	
	parametry: \texttt{vector<PBLit> \&v}\tabularnewline
	\hline 
	\texttt{addConstr}  & \texttt{void}  & p\v{r}idá PB podmínku
	
	parametry: \texttt{vector<PBLit> \&v}
	
	\texttt{Solver::Inequality eq}
	
	\texttt{int val}\tabularnewline
	\hline 
	\texttt{solve}  & \texttt{void}  & hledání \v{r}ešení
	
	parametry: \texttt{Solver::Command cmd}\tabularnewline
	\hline 
\end{tabular}

}






\begin{lstlisting}[language=c++, caption={Solver - ukázka kódu.}, label={lst:code}]
#include "minisatp/include/PBLit.h"
#include "minisatp/include/Params.h"
#include "minisatp/include/Helper.h"
#include "minisatp/include/Solver.h"

class WriteSolution : public Helper {
	void solution () {
		cout << "Nalezene reseni:" << endl;
		for (size_t i = 0; i < v.size(); ++i) {
			cout << v[i] << " "
		}
		cout << endl;
	}
}

int main(void) {	
	Params::setDefaults();
	Solver& s = Solver::getInstance();
	s.init(3,1);
	WriteSolution h;
	s.setHelper(&h);

	vector<PBLit> v1{PBLit(1, 1, false),
	PBLit(1, 2, false),
	PBLit(1, 3, false)}
//vektor reprezentujici levou stranu LS = 1*x1 + 1*x2 + 1*x3
	s.addConstr(v1, Solver::INEQ_GE, 1);
//PB podminka ve tvaru LS >= 1
	s.solve(Solver::FIND_ALL);	
//postupne vypise vsechna reseni {x1, x2, x3} = 
//{1, 0, 0}, {0, 1, 0}, {0, 0, 1},
//{0, 1, 1}, {1, 0, 1}, {1, 1, 0} a 
//{1, 1, 1}
}
\end{lstlisting}

\begin{figure}[h]
	
	\includegraphics[width=\textwidth]{includes/Solver_seq_diagram}
	\centering
	\caption{Sekvenční diagram spolupráce tříd Solver a Helper.}
	\label{fig:seq_diag}
\end{figure}

\section{Hlavní program}
V následujcím texu podávám popis použitých tříd v hlavním programu nazvaném ATPG\_RAS. Načtení obvodu je provedeno přímo frameworkem LogSynth. Další výpočty pak probíhají v rámci instance třídy RAS a pomocná data jsou předávána instancemi třídy Crate. 

\subsection*{Crate}
Pomocná třída reprezentující návratovou hodnotu z výpočtů, tj. počty změněných bitů a nalezených poruch.
\\

% Náhled zdrojového kódu pro odstavec 0
\makebox[\textwidth][c]{
	\begin{tabular}{|>{\centering}p{3cm}|>{\centering}p{3cm}|>{\centering}p{8cm}|}
		\hline 
		Název atributu & Datový typ & Popis\tabularnewline
		\hline 
		\hline 
		\texttt{changedBitsPI} & \texttt{unsigned int} & po\v{c}et zm\v{e}n\v{e}ných bit\r{u} v PI\tabularnewline
		\hline 
		\texttt{changedBitsFF} & \texttt{unsigned int} & po\v{c}et zm\v{e}n\v{e}ných bit\r{u} v FF\tabularnewline
		\hline 
		\texttt{droppedFaults} & \texttt{unsigned int} & po\v{c}et nalezených poruch\tabularnewline
		\hline 
\end{tabular}}

\subsection*{RAS}
Hlavní třída programu.

Popis atributů viz níže.
\\

% Náhled zdrojového kódu pro odstavec 0

\makebox[\textwidth][c]{
	\begin{tabular}{|>{\centering}p{3cm}|>{\centering}p{3cm}|>{\centering}p{8cm}|}
		\hline 
		Název atributu & Datový typ & Popis\tabularnewline
		\hline 
		\hline 
		\texttt{network} & Network\& & Sí\v{t} obvodu\tabularnewline
		\hline 
		ATPG & ATPG\_alg\& & ATPG obvodu\tabularnewline
		\hline 
		remainingFaults & unsigned int & po\v{c}et zbývajích poruch\tabularnewline
		\hline 
		numPI & unsigned int & po\v{c}et PI\tabularnewline
		\hline 
		numPO & unsigned int & po\v{c}et PO\tabularnewline
		\hline 
		numFF & unsigned int & po\v{c}et FF\tabularnewline
		\hline 
		testVector & Cube{*} & poslední vygenerovaný testovací vektor\tabularnewline
		\hline 
		response & vector$<$Literal$>${*} & odezva obvodu na poslední testovací vektor\tabularnewline
		\hline 
		patterns & list$<$Cube{*}$>$ & na\v{c}tené externí testovací vektory\tabularnewline
		\hline 
\end{tabular}}



% Náhled zdrojového kódu pro odstavec 1
Popis metod viz níže.
\\


\makebox[\textwidth][c]{
	\begin{tabular}{|>{\centering}p{3cm}|>{\centering}p{3cm}|>{\centering}p{8cm}|}
		\hline 
		Název metody & Návratový typ & Popis\tabularnewline
		\hline 
		\hline 
		SAT & bool & nalezne testovací vektor pro první dostupnou poruchu z Faultlistu\tabularnewline
		\hline 
		SAT\_PBO & bool & nalezne testovací vektor s minimální vzdáleností dle RAS\tabularnewline
		\hline 
		fillDCs & void & nahradí DC hodnoty v\tabularnewline
		\hline 
		loadPatterns & void & na\v{c}te testovací vektory z externího souboru
		
		parametry: string pr\_filename\tabularnewline
		\hline 
		calculate & Crate & provede fault dropping a simulaci pro aktuální testovací vektor. Vrátí
		po\v{c}et zm\v{e}n\v{e}ných bit\r{u} a po\v{c}et nalezených poruch\tabularnewline
		\hline 
		\end{tabular}
}	





\subsection*{Parametry spuštění}
Program (spustitelný soubor) je na příkazové řádce spouštěn příkazem ve tvaru 
\begin{verbatim}
ATPG_RAS parametry zdrojový-soubor[.blif|.bench]
\end{verbatim} 
kde jako parametry akceptuje následující přepínače:
\begin{itemize}
	\item \texttt{-v} Vypíše verzi programu.
	\item \texttt{-pw jmeno-souboru} Nastaví výpisování nalezených testovacích vektorů do daného souboru.
	\item \texttt{-pr jmeno-souboru} Z daného souboru jsou načteny a aplikovány testovací vektory, posléze jsou vektory hledány algoritmem pro RAS.
	\item -flw soubor Do daného souboru vypíše faultlist
	\item -ud soubor Do daného souboru jsou vypsány nalezené nedetekovatelné poruchy
	\item -rep soubor Nastaví vypisování informací o řešení do daného souboru. Do souboru jsou zapisovány informace o počtu změněných bitů a o počtu nalezených poruch. \textbf{Povinný parametr}.
	\item -nomin Vypne hledání minimální vzdálenosti přes zbývající poruchy.
	\item -rnd n Aplikace vygeneruje n náhodných testovacích vektorů do souboru zadaného pomocí -pw a skončí.
	\item -dc DC\footnote{don't care} hodnoty v nalezených testovacích vektorech jsou doplňovány náhodně 0/1. 
	\item -verbose n Nastaví množství informací výpisovaných na standardní výstup z vlastní aplikace (n = 0 až 2, 0 = nejméně výpisů)
	\item -mv0, -mv1, -mv2 Nastaví množství informací výpisovaných na standardní výstup z výpočtu Minisat+ (-mv0 nejméně informací)
\end{itemize}

\section{Testování}
Výslednou aplikaci jsem podrobil manuálnímu testování. Vytvořil jsem několik jednoduchých obvodů, viz např. obr. \ref{fig:test_circuit2} a následně jsem tyto použil jako vstup programu. 

\begin{figure}[h]
	
	\includegraphics[width=0.6\textwidth]{includes/test_circuit2}
	\centering
	\caption{Jednoduchý testovací obvod.}
	\label{fig:test_circuit2}
\end{figure}

Při testování jsem zkoumal
\begin{itemize}
	\item zda funguje simulace obvodu - výstupy obvodu odpovídají vstupům
	\item funkce řešiče z hlediska SAT - zda testovací vektor vypočtený pomocí SAT pro jistou poruchu tuto poruchu i skutečne nalezne
	\item funkce řešiče z hlediska PBO - zda u po sobě jdoucích testovacích vektorů skutečně nastává nějaká minimalizace bitové vzdálenosti
\end{itemize}

Pro obr. \ref{fig:test_circuit2} je v tabulce \ref{tab:testing_example} přehled výstupů z testu. 
% Náhled zdrojového kódu pro odstavec 0

% Náhled zdrojového kódu pro odstavec 0

\begin{table}[h]
	\makebox[\textwidth][c]{
	\begin{centering}
		\begin{tabular}{|>{\centering}p{2cm}|>{\centering}p{2cm}|>{\centering}p{2cm}|c|>{\centering}p{4cm}|}
			\hline 
			vstup (pi1, pi2, lo1) & výstup (po1, li1) & zm\v{e}nene bity (pi, FF) & SAT porucha & nalezené poruchy\tabularnewline
			\hline 
			\hline 
			11 1 & 1 0 & 2 1 & pi1 / 0 & pi1 / 0
			
			lo1 / 0
			
			d $\rightarrow$ li1 / 0
			
			d $\rightarrow$ po1 /0\tabularnewline
			\hline 
			11 0 & 0 1 & 0 0 & pi2 / 0 & pi2 / 0
			
			lo1 / 1
			
			d $\rightarrow$ li1 / 1
			
			d $\rightarrow$ po1 / 1\tabularnewline
			\hline 
			01 1 & 0 1 & 1 0 & pi1 / 1 & pi1 / 1\tabularnewline
			\hline 
			00 1 & 1 1 & 1 0 & pi2 / 1 & pi2 / 1\tabularnewline
			\hline 
		\end{tabular}
		\par\end{centering}}
	\caption[Příklad pro testování.]{Výstupy z programu pro vstup z obr. \ref{fig:test_circuit2}. (d = výstup z AND hradla před větvením)}
	\label{tab:testing_example}
\end{table}




\section{Instalace}
Program je distribuován ve spustitelné binární formě i v podobě zdrojového kódu. Pro kompilaci je v prostředí OS Windows nutné otevřít řešení LogSynth ve Visual Studiu a zkompilovat projekt ATPG\_RAS, přičemž je automaticky vyřešena závislost na projektech Minisat+ a Kernel, které jsou kompilované jako statické knihovny, a na projektu ATPG, se kterým ATPG\_RAS sdílí kód. Pro platformu linux je k disposici makefile a program je zkompilován pomocí \verb|make ATPG_RAS|. Závislosti na Minisat+, ATPG a Kernel jsou vyřešeny v rámci makefile.

\chapter{Experimentální výsledky}
Vytvořený program jsem se pokusil aplikoval na obvody z balíku ISCAS\footnote{International Symposium on Circuits and Systems}. Program jsem spouštěl ve versi pro OS Windows na počítači s hardwarovými parametry CPU Intel i5-8250U, 8 GB RAM. Bohužel se ukázalo, že pro složitější obvody algoritmus běží poměrně dlouho (např. pro obvod ISCAS s13207 by byl potřeba přibližně týden) a v rozumném čase byl výpočet schopný doběhnout pouze na jednodušších obvodech. Do experimentálního vyhodnocení tedy zařazuji pouze výsledky z \uv{menších} obvodů.

V tab. \ref{tab:experiments} uvádím přehled informací o dvou testovaných obvodech a získané výsledky. Výpočet jsem prováděl nejprve algoritmem pro RAS a porovnávám ho s výpočtem s vypnutou minimalizací. Do délky bitstreamu započítávám počet měněných bitů z PI a počet měněných bitů z FF znásobený délkou adresy ($\left\lceil \log_{2}n_{\textrm{FF}}\right\rceil $) 


% Náhled zdrojového kódu pro odstavec 1

% Náhled zdrojového kódu pro odstavec 1

\begin{table}[htbp]
	\makebox[\textwidth][c]{
	\begin{centering}
		\begin{tabular}{|>{\centering}p{3cm}|c|c|c|c|c|>{\centering}p{3cm}||>{\centering}p{3cm}|}
			\hline 
			Obvod & PI& PO & FF & Poruch & Vektor\r{u} & Délka bitstreamu {[}bit\r{u}{]} & Délka výpočtů\tabularnewline
			\hline 
			\hline 
			ISCAS s991 & 65 & 17 & 19 & 908 & 132 & 386 & $\approx$ 10 min\tabularnewline
			\hline 
			ISCAS s991 bez PBO & 65 & 17 & 19 & 908 & 108 & 6713 & $\approx$ 3 min\tabularnewline
			\hline 
			\hline 
			ISCAS s1423 & 17 & 5 & 74 & 1495 & 207 & 2030 & $\approx$ 20 min\tabularnewline
			\hline 
			ISCAS s1423 bez PBO & 17 & 5 & 74 & 1495 & 88 & 20316 & $\approx$ 5 min\tabularnewline
			\hline 
			ISCAS s13207 & 30 & 116 & 669 & 9682 & 1385 & 36766 & $\approx$ 120 hod\tabularnewline
			\hline 
		\end{tabular}
		\par\end{centering}}
	\label{tab:experiments}
	\caption[Výsledky pro s991 a s1423.]{Přehled pro obvody s991 a s1423}
\end{table}

Pro změřené výsledky platí, že algoritmus sice zvýší počet nalezených testovacích vektorů, ale řádově sníží délku bitstreamu (V porovnání s výpočtem, kdy je vypnutá minimalizace). Co se týče výpočtu pro ISCAS s13207, tak se zdá, že získaná data jsou horší než v \cite{baikRAS}. Grafické průběhy z výpočtů jsou na obr. \ref{fig:exp1} až \ref{fig:exp5}. 




\begin{figure}[h]	
	\includegraphics[width=\textwidth]{includes/s991_ras}
	\centering
	\caption{ISCAS s991.}
	\label{fig:exp1}
\end{figure}

\begin{figure}[h]	
	\includegraphics[width=\textwidth]{includes/s991_atpg}
	\centering
	\caption{ISCAS s991 bez minimalizace (pouze SAT).}
\end{figure}

\begin{figure}[h]	
	\includegraphics[width=\textwidth]{includes/s1423_ras}
	\centering
	\caption{ISCAS s1429.}
\end{figure}

\begin{figure}[h]	
	\includegraphics[width=\textwidth]{includes/s1423_atpg}
	\centering
	\caption{ISCAS s1429 bez minimalizace (pouze SAT).}
		\label{fig:exp4}
\end{figure}

\begin{figure}[h]	
	\includegraphics[width=\textwidth]{includes/s13207_ras}
	\centering
	\caption{ISCAS s13207.}
	\label{fig:exp5}
\end{figure}

\chapter{Další vývoj}
Kvůli nedostatku času se mi bohužel nepodařilo zrealizovat vše, co jsem původně zamýšlel. Jako další nápady či návrhy pro rozvoj programu bych zmínil zejména:
\subsection*{Analýza vlivu parametrů PbSolveru}
Při vývoji programu bohužel nevyzbyl čas na zkoumání vlivu parametrů solveru, tj. vliv nastavení původních globálních proměnných \verb|opt_X| (přistupovaných pomocí statických metod třídy \verb|Params|). Takto jde např. omezit metoda převodu PB podmínek do SAT a též je možno nastavovat několik číselných parametrů. Pro toto by zřejmě bylo nutné důkladně nastudovat článek autorů solveru, neboť ze zdrojového kódu programu je význam proměnných zřejmý jen rámcově. Dále by bylo nutné se zamyslet nad způsobem vstupu těchto parametrů do programu, protože větší počet přepínačů ve vstupu by učinil program ještě více nepřehledným. 

\subsection*{Paralelizace}
Dalším vhodným kandidátem na další rozvoj programu by byl převod na paralelní výpočet. Výhody takového přístupu jsou jasné - v dnešní době je u většiny PC k disposici 4 či více jader procesoru a došlo by tak k (přibližně) stejnému urychlení běhu programu. Jádro algoritmu tvořené hledáním minima přes množinu poruch by bylo jednoduché upravit jako úlohu producent-konzument, globální datové struktury, které jsou v PbSolveru sdíleny, by však bylo nutné odstranit.

\begin{conclusion}
Cílem této práce bylo navrhnout a implementovat aplikaci pro generování komprimovaného testu pro číslicové obvody s RAS architekturou. Aplikace měla být založena na frameworku LogSynth a řešiči Minisat+. I přes nedostatek času mám za to, že se tento cíl z větší části naplnit podařilo, přestože se při vývoji aplikace objevila řada jevů, které by bylo dobré dále hlouběji zkoumat a věnovat jim pozornost, jako např. vliv doplňování DC hodnot do testovacích vektorů. Jako pozitivní bych hodnotil to, že se v rámci vývoje podařilo objevit a opravit i několik chyb v použitém frameworku a v Minisat+.

Další vývoj a práce s aplikací by mohly zahrnovat zkoumání na více rozsáhlejších obvodech, paralelizaci či optimalizaci simulace obvodů v LogSynthu, čímž by se výpočty mohly urychlit.
\end{conclusion}

\bibliographystyle{csn690}
\bibliography{bibliografie_BP_KP}

\appendix

\chapter{Seznam použitých zkratek}
% \printglossaries
\begin{description}
	\item[ATPG] Automatický generátor testovacích vektorů pro číslicové obvody  (\textit{Automatic Test Pattern Generator})
	\item[CNF, KNF] Konjunktivní normální forma
	\item[CUT, DUT] Testovaný obvod (\textit{chip under test, device under test, design under test})
	\item[DFF] Klopný obvod typu D, 1-bitová paměť
	\item[PBO] Pseudo-booleovská optimalizace
	\item[PI] Primární vstup či vstupy
	\item[PPI] Pseudo-primární vstup či vstupy
	\item[PO] Primární výstup či výstupy
	\item[PPO] Pseudo-primární výstup či výstupy
	\item[RAS] Random access scan
	\item[SAT] Problém splitelnosti booleovské formule
\end{description}


% % % % % % % % % % % % % % % % % % % % % % % % % % % % 
% % Tuto kapitolu z výsledné práce ODSTRAŇTE.
% % % % % % % % % % % % % % % % % % % % % % % % % % % % 
% 
% \chapter{Návod k~použití této šablony}
% 
% Tento dokument slouží jako základ pro napsání závěrečné práce na Fakultě informačních technologií ČVUT v~Praze.
% 
% \section{Výběr základu}
% 
% Vyberte si šablonu podle druhu práce (bakalářská, diplomová), jazyka (čeština, angličtina) a kódování (ASCII, \mbox{UTF-8}, \mbox{ISO-8859-2} neboli latin2 a nebo \mbox{Windows-1250}). 
% 
% V~české variantě naleznete šablony v~souborech pojmenovaných ve formátu práce\_kódování.tex. Typ může být:
% \begin{description}
% 	\item[BP] bakalářská práce,
% 	\item[DP] diplomová (magisterská) práce.
% \end{description}
% Kódování, ve kterém chcete psát, může být:
% \begin{description}
% 	\item[UTF-8] kódování Unicode,
% 	\item[ISO-8859-2] latin2,
% 	\item[Windows-1250] znaková sada 1250 Windows.
% \end{description}
% V~případě nejistoty ohledně kódování doporučujeme následující postup:
% \begin{enumerate}
% 	\item Otevřete šablony pro kódování UTF-8 v~editoru prostého textu, který chcete pro psaní práce použít -- pokud můžete texty s~diakritikou normálně přečíst, použijte tuto šablonu.
% 	\item V~opačném případě postupujte dále podle toho, jaký operační systém používáte:
% 	\begin{itemize}
% 		\item v~případě Windows použijte šablonu pro kódování \mbox{Windows-1250},
% 		\item jinak zkuste použít šablonu pro kódování \mbox{ISO-8859-2}.
% 	\end{itemize}
% \end{enumerate}
% 
% 
% V~anglické variantě jsou šablony pojmenované podle typu práce, možnosti jsou:
% \begin{description}
% 	\item[bachelors] bakalářská práce,
% 	\item[masters] diplomová (magisterská) práce.
% \end{description}
% 
% \section{Použití šablony}
% 
% Šablona je určena pro zpracování systémem \LaTeXe{}. Text je možné psát v~textovém editoru jako prostý text, lze však také využít specializovaný editor pro \LaTeX{}, např. Kile.
% 
% Pro získání tisknutelného výstupu z~takto vytvořeného souboru použijte příkaz \verb|pdflatex|, kterému předáte cestu k~souboru jako parametr. Vhodný editor pro \LaTeX{} toto udělá za Vás. \verb|pdfcslatex| ani \verb|cslatex| \emph{nebudou} s~těmito šablonami fungovat.
% 
% Více informací o~použití systému \LaTeX{} najdete např. v~\cite{wikilatex}.
% 
% \subsection{Typografie}
% 
% Při psaní dodržujte typografické konvence zvoleného jazyka. České \uv{uvozovky} zapisujte použitím příkazu \verb|\uv|, kterému v~parametru předáte text, jenž má být v~uvozovkách. Anglické otevírací uvozovky se v~\LaTeX{}u zadávají jako dva zpětné apostrofy, uzavírací uvozovky jako dva apostrofy. Často chybně uváděný symbol "{} (palce) nemá s~uvozovkami nic společného.
% 
% Dále je třeba zabránit zalomení řádky mezi některými slovy, v~češtině např. za jednopísmennými předložkami a spojkami (vyjma \uv{a}). To docílíte vložením pružné nezalomitelné mezery -- znakem \texttt{\textasciitilde}. V~tomto případě to není třeba dělat ručně, lze použít program \verb|vlna|.
% 
% Více o~typografii viz \cite{kobltypo}.
% 
% \subsection{Obrázky}
% 
% Pro umožnění vkládání obrázků je vhodné použít balíček \verb|graphicx|, samotné vložení se provede příkazem \verb|\includegraphics|. Takto je možné vkládat obrázky ve formátu PDF, PNG a JPEG jestliže používáte pdf\LaTeX{} nebo ve formátu EPS jestliže používáte \LaTeX{}. Doporučujeme preferovat vektorové obrázky před rastrovými (vyjma fotografií).
% 
% \subsubsection{Získání vhodného formátu}
% 
% Pro získání vektorových formátů PDF nebo EPS z~jiných lze použít některý z~vektorových grafických editorů. Pro převod rastrového obrázku na vektorový lze použít rasterizaci, kterou mnohé editory zvládají (např. Inkscape). Pro konverze lze použít též nástroje pro dávkové zpracování běžně dodávané s~\LaTeX{}em, např. \verb|epstopdf|.
% 
% \subsubsection{Plovoucí prostředí}
% 
% Příkazem \verb|\includegraphics| lze obrázky vkládat přímo, doporučujeme však použít plovoucí prostředí, konkrétně \verb|figure|. Například obrázek \ref{fig:float} byl vložen tímto způsobem. Vůbec přitom nevadí, když je obrázek umístěn jinde, než bylo původně zamýšleno -- je tomu tak hlavně kvůli dodržení typografických konvencí. Namísto vynucování konkrétní pozice obrázku doporučujeme používat odkazování z~textu (dvojice příkazů \verb|\label| a \verb|\ref|).
% 
% \begin{figure}\centering
% 	\includegraphics[width=0.5\textwidth, angle=30]{cvut-logo-bw}
% 	\caption[Příklad obrázku]{Ukázkový obrázek v~plovoucím prostředí}\label{fig:float}
% \end{figure}
% 
% \subsubsection{Verze obrázků}
% 
% % Gnuplot BW i barevně
% Může se hodit mít více verzí stejného obrázku, např. pro barevný či černobílý tisk a nebo pro prezentaci. S~pomocí některých nástrojů na generování grafiky je to snadné.
% 
% Máte-li například graf vytvořený v programu Gnuplot, můžete jeho černobílou variantu (viz obr. \ref{fig:gnuplot-bw}) vytvořit parametrem \verb|monochrome dashed| příkazu \verb|set term|. Barevnou variantu (viz obr. \ref{fig:gnuplot-col}) vhodnou na prezentace lze vytvořit parametrem \verb|colour solid|.
% 
% \begin{figure}\centering
% 	\includegraphics{gnuplot-bw}
% 	\caption{Černobílá varianta obrázku generovaného programem Gnuplot}\label{fig:gnuplot-bw}
% \end{figure}
% 
% \begin{figure}\centering
% 	\includegraphics{gnuplot-col}
% 	\caption{Barevná varianta obrázku generovaného programem Gnuplot}\label{fig:gnuplot-col}
% \end{figure}
% 
% 
% \subsection{Tabulky}
% 
% Tabulky lze zadávat různě, např. v~prostředí \verb|tabular|, avšak pro jejich vkládání platí to samé, co pro obrázky -- použijte plovoucí prostředí, v~tomto případě \verb|table|. Například tabulka \ref{tab:matematika} byla vložena tímto způsobem.
% 
% \begin{table}\centering
% 	\caption[Příklad tabulky]{Zadávání matematiky}\label{tab:matematika}
% 	\begin{tabular}{|l|l|c|c|}\hline
% 		Typ		& Prostředí		& \LaTeX{}ovská zkratka	& \TeX{}ovská zkratka	\tabularnewline \hline \hline
% 		Text		& \verb|math|		& \verb|\(...\)|	& \verb|$...$|		\tabularnewline \hline
% 		Displayed	& \verb|displaymath|	& \verb|\[...\]|	& \verb|$$...$$|	\tabularnewline \hline
% 	\end{tabular}
% \end{table}
% 
% % % % % % % % % % % % % % % % % % % % % % % % % % % % 

\chapter{Obsah přiloženého CD}

%upravte podle skutecnosti

\begin{figure}
	\dirtree{%
		.1 readme.txt\DTcomment{stručný popis obsahu CD}.
		.1 bin\DTcomment{adresář se spustitelnou formou implementace}.
		.1 src.
		.2 impl\DTcomment{zdrojové kódy implementace}.
		.2 thesis\DTcomment{zdrojová forma práce ve formátu \LaTeX{}}.
		.1 text\DTcomment{text práce}.
		.2 thesis.pdf\DTcomment{text práce ve formátu PDF}.	
	}
\end{figure}

\end{document}
