Current courses - rozvrh ZS2011
------
Courses - 2010/2011
BI-CAO - Číslicové a analogové obvody
BI-SAP - Struktura a architektura počítačů
Courses - 2009/2010
X36PJC - Programovací jazyk C++
Y36ALG - Algoritmizace
Nabízené bakalářské a diplomové práce
- Prozkoumejte možnosti rozšíření ATPG (Automatic Test Patterns Generator) SAT-Solveru (MiniSat, zChaff, ...) o techniku "aktivace klauzulí", "preprocessing" a "postprocessing" ke zvýšení počtu DC (Don't Care) bitů. Proveďte srovnání původní a rozšířené verze SAT-Solveru pro různé typy instancí SAT problému (umělé instance vs. instance generované v ATPG).
-> Programovací jazyk C, C++
-> SAT-Solver=nástroj řešící splnitelnost booleovské formule
SP, BP, DP
- Prozkoumejte možnosti vnitřní reprezentace klauzulí SAT-Solveru (MiniSat, zChaff, ...). Upravte vnitřní reprezentaci zvoleného SAT-Solveru a prohledávácí heuristiku na reprezentaci klauzulí pomocí ZDD (Zero-Suppressed Decision Diagram). Zjistěte možnosti komprese instance SAT problému pomocí ZDD a vliv vnitřní reprezentace na rychlost řešení. Měření proveďte pro umělé a ATPG (Automatic Test Patterns Generator) SAT instance.
-> Programovací jazyk C, C++
-> SAT instance=problém splnitelnosti zadán jako booleovská formule v konjunktivní normální formě; SAT-Solver=nástroj řešící splnitelnost booleovské formule
DP (SP, BP)
- Prozkoumejte možnosti vnitřní reprezentace klauzulí SAT-Solveru (MiniSat, zChaff, ...). Upravte vnitřní reprezentaci zvoleného SAT-Solveru a prohledávácí heuristiku na reprezentaci klauzulí pomocí BDD (Binary Decision Diagram). Porovnejte vliv vnitřní reprezentace na rychlost řešení. Měření proveďte pro umělé a ATPG (Automatic Test Patterns Generator) SAT instance.
-> Programovací jazyk C, C++
-> SAT instance=problém splnitelnosti zadán jako booleovská formule v konjunktivní normální formě; SAT-Solver=nástroj řešící splnitelnost booleovské formule
DP (SP, BP)
- Prozkoumejte možnosti SSMIBDDs (Structurally Synthesized Multiple Input BDDs) v simulaci digitálních obvodů a implementujte simulátor poruch využívající tuto reprezentaci. Vaše řešení porovnejte se stávajícími simulátory a výsledky zhodnoťe.
-> Programovací jazyk C, C++
SP, BP, DP
- Prostudujte možnosti generování SAT instance v CNF (Conjunctive Normal Form) reprezentující množinu testovacích vektorů pro poruchu v digitálním obvodu. Implementujte několik způsobů a proveďte jejich srovnání (velikost, doba generování, rychlost řešení SAT-solvery).
-> Programovací jazyk C, C++
-> SAT instance=problém splnitelnosti zadán jako booleovská formule v konjunktivní normální formě; SAT-Solver=nástroj řešící splnitelnost booleovské formule
SP, BP (DP)
- Nastudujte problematiku SSMIBDDs (Structurally Synthesized Multiple Input BDDs) a implementujte knihovnu funkcí pro práci s touto strukturou. Funkčnost řešení demonstrujte na jednoduchých příkladech.
-> Programovací jazyk C, C++ SP, BP, DP
|