|
| |
|
|
FPGA Platform with .NET Micro Framework Support
Matyáš, Jan ; Minařík, Miloš (referee) ; Vašíček, Zdeněk (advisor)
The goal of the thesis is to design a development board that may be used for embedded systems prototyping. The board's key parts are an ARM-Cortex-based microcontroller and a FPGA programmable circuit. The platform is designed with .NET Micro Framework support in mind. The thesis contains specifications of the development board, describes the design process as well as the task of .NET Micro Framework porting and the establishment of communication bus between the FPGA and microcontroller circuits. The thesis is concluded by a set of demonstration examples which outline how to develop new applications for the designed platform.
|
|
|
GPU-Accelerated Synthesis of Probabilistic Programs
Marcin, Vladimír ; Matyáš, Jiří (referee) ; Češka, Milan (advisor)
V tejto práci sa zoberáme problémom automatizovanej syntézy pravdepodobnostných programov: majme konečnú rodinu kandidátnych programov, v ktorej chceme efektívne identifikovať program spĺňajúci danú špecifikáciu. Aj riešenie tých najjednoduchších syntéznych problémov v praxi predstavuje NP-ťažký problém. Pokrok v tejto oblasti prináša nástroj Paynt, ktorý na riešenie tohto problému používa novú integrovanú metódu syntézy pravdepodobnostných programov. Aj keď sa tento prístup dokáže efektívne vysporiadať s exponenciálnym rastom rodín kandidátnych riešení, stále tu existuje problém spôsobený exponenciálnym rastom jednotlivých členov týchto rodín. S cieľom vysporiadať sa aj s týmto problémom, sme implementovali GPU orientované algoritmy slúžiace na overovanie kandidátnych programov (modelov), ktoré danú úlohu paralelizujú na stavovej úrovni pravdepodobnostých modelov. Celkové zrýchlenie doshiahnuté týmto prístupom za určitých podmienok potom prinieslo takmer teoretický limit možného zrýchlenia syntézneho procesu.
|
|
|
Wireless Security System
Matyáš, Jan ; Kočí, Radek (referee) ; Hanáček, Petr (advisor)
This thesis describes the design and implementation of portable wireless security device for monitoring object. The device consists of a control module allowing user to set and monitor current state of the measuring module which communicates with the control module wireless using the ISM band. The device is battery powered and highest possible battery life per charge is required.
|
|
|
Improving Robustness of Neural Networks against Adversarial Examples
Gaňo, Martin ; Matyáš, Jiří (referee) ; Češka, Milan (advisor)
Tato práce pojednává o kontradiktorních útocích na klasifikační modely neuronových sítí. Naším cílem je shrnout a demonstrovat kontradiktorní metody a ukázat, že představují vážný problém v strojovém učení. Důležitým přínosem této práce je implementace nástroje pro trénink robustního modelu na základě kontradiktorních příkladů. Náš přístup spočívá v minimalizaci maximalizace chybové funkce cílového modelu. Související práce a naše vlastní experimenty nás vedou k použití Projektovaného gradientního sestupu jako cílového útoku, proto trénujeme proti datům generovaným Projektovaným gradientním sestupem. Výsledkem použití nástroje je, že můžeme dosáhnout přesnosti více než 90% proti sofistikovaným nepřátelským útokům.
|
|
|
Employing Approximate Equivalence for Design of Approximate Circuits
Matyáš, Jiří ; Lengál, Ondřej (referee) ; Češka, Milan (advisor)
This thesis is concerned with the utilization of formal verification techniques in the design of the functional approximations of combinational circuits. We thoroughly study the existing formal approaches for the approximate equivalence checking and their utilization in the approximate circuit development. We present a new method that integrates the formal techniques into the Cartesian Genetic Programming. The key idea of our approach is to employ a new search strategy that drives the evolution towards promptly verifiable candidate solutions. The proposed method was implemented within ABC synthesis tool. Various parameters of the search strategy were examined and the algorithm's performance was evaluated on the functional approximations of multipliers and adders with operand widths up to 32 and 128 bits respectively. Achieved results show an unprecedented scalability of our approach.
|
|
|
Optimal Scheduling Systems for Outdoor Activity
Rykala, Kryštof ; Matyáš, Jiří (referee) ; Češka, Milan (advisor)
The thesis discusses technologies and approaches for implementation of information system. Its part and motivation is automatic scheduling of activities. A model for resource-contraint project scheduling is defined using mixed-integer linear programming. Part of this thesis are client, server and planning programs that form a system for management of an outdoor center with automatic scheduling of activities.
|
|
|
RONJA TWISTER Based on FPGA
Matyáš, Jan ; Kaštil, Jan (referee) ; Vašíček, Zdeněk (advisor)
RONJA is an open-source hardware project for an optical data-link device which utilizes a visible-light beam for wireless data transmission. This thesis focuses on a single electronic module called RONJA Twister, which forms an interface between metallic Ethernet and the optical transmission itself. The purpose of this project is to reimplement the original Twister module design in a backward-compatible manner using FPGA technology. Furthermore, the proposed and implemented solution enhances the module by incorporating the Auto-Negotiation capability which mitigates several issues of the original Twister module.
|
|
|
Counter-Example Generation in the Analysis of Markov Models
Molek, Martin ; Matyáš, Jiří (referee) ; Češka, Milan (advisor)
This thesis deals with generating counterexamples in context of probabilistic models. Counterexamples are generated for Markov models (specifically DTMC). Definitions of model properties are given by logic PCTL. Two algorithms (Best-first search and Recursive Enumration Algorithm) are used to generate these counterexamples. Thesis describes implementation of algorithms into verification tool STORM. The results of experiments show that REA is capable of handling models containg millions of states.
|
|
|
A VHDL Parser for Formal Verification
Matyáš, Jiří ; Smrčka, Aleš (referee) ; Charvát, Lukáš (advisor)
The principal goal of this bachelor thesis is to design and implement a parser of VHDL language into graph representation in VAM (Variable Assignment Language). The application is developed for formal verification purposes of VeriFIT research group of the Faculty of Information Technology, Brno University of Technology. The development of the compiler described in this thesis should provide the opportunity to use formal verification techniques to verify hardware designs described in high level design languages, such as VHDL.
|
guest ::
RSS feed.