# 36DP - Diplomová práce

## Automatický generátor testovacích vektorů (ATPG) založený na testu splnitelnosti booleovské formule

- Abstrakt
- CD struktura
- Instalační informace
- Manuál

# Abstrakt

Práce se zabývá implementací ATPG nástroje využívající řešení SAT problému open-source řešičem. Jako řešič je použit Minisat 2.0, dále jsou zkoumány možnosti generování neurčitých hodnot v testovacích vektorech. Vstupem aplikace jsou soubory ve formátu ISCAS 89, výsledné sady vektorů jsou porovnány s ATPG nástrojem Atalanta. Dále jsou analyzovány parametry instancí SAT řešených při generování vektorů. Nástroj může být použit jako generátor instancí SAT problémů ve formátu DIMACS.

### Abstract

In this thesis ATPG aplication based on solving SAT problem by open-source solver. SAT solver Minisat 2.0 is used, Ways of generating don´t cares in test patterns are explored. Files in format ISCAS 89 are input of aplication, resulted test patterns are compared with ATPG tool Atalanta. Parameters of SAT instances solved during ATPG are analyzed. ATPG tool can by used as generator of SAT instances in DIMACS format.

# CD struktura

    |-- bin
    |-- exe
    |-- src
    |   `-- sat_atpg
    |       |-- lib
    |       |   |-- minisat
    |       |   `-- minisat_dc
    |       `-- src
    `-- text
        `-- latex-src

# Instalační příručka

Program je na CD médiu dodán ve formě binárních souborů v adresářích bin/ a exe/ ve formě zdrojových kódů v adresáři src/. Pro snadný překlad zdrojových kódů je program spravován nástroji Autotools (Autoconf, Automake, Libtool). Pro překlad na platformě Linux použijte známou trojici příkazů:

$> ./configure
$> make
$> sudo make install

Skriptu `./configure` lze předat řadu parametrů, které lze zjistit pomocí:

$> ./configure --help

Překlad na platformě Windows je možný podobným způsobem za použití prostředí Cygwin.

Nahoru