|
|
Automated Verification in HW/SW Co-design
Charvát, Lukáš ; Kubátová, Hana (oponent) ; Řehák, Vojtěch (oponent) ; Vojnar, Tomáš (vedoucí práce)
The subject of the thesis is to design new hardware verification techniques optimized for a process of HW/SW co-design in which hardware and software are developed in parallel to speed up the development of new embedded systems. Currently, microprocessor co-design tools typically allow to verify designs by simulation and/or functional verification. However, even extensive functional verification can miss some non-trivial bugs. Therefore, formal verification has become more and more desirable in recent years. As opposed to testing and bug-hunting techniques that only aim at detecting flaws, the goal of formal verification is to rigorously prove that the system is indeed correct. Formal verification is, however, a very demanding task, and even though a lot of progress has been achieved in this area, formal verification is far from being able to fully automatically check all relevant properties of complex designs without a significant and costly human involvement in the verification process. The thesis deals with these challenges by focusing on verification techniques based on formal approaches, but possibly relaxing or limiting their precision and generality to achieve full automation. Further, the thesis also focuses on the efficiency of the proposed techniques and their ability to deliver continuous feedback about the verification process. Special attention is devoted to the development of formal methods for checking the equivalence of microprocessor designs on various levels of abstraction. Although these designs cannot be behaviorally equivalent, they are required to give mutually corresponding results when executing the same input program, which is a property difficult to achieve. As another considered topic, the thesis proposes methods for checking correctness of mechanisms preventing data and control hazards in single-pipelined implementations of microprocessors. The approaches described in this thesis has been implemented in the form of several tools which, after examining designs of multiple pipelined microprocessors, were able to deliver promising experimental results.
|
|
|
Formy spolupráce neziskové organizace Sue Ryder s firemními partnery
Řehák, Vojtěch ; Legnerová, Kateřina (vedoucí práce) ; Dohnalová, Marie (oponent)
Spolupráce mezi tržními společnostmi a organizacemi občanské společnosti je v moderní společnosti fenoménem. Stran firem tato spolupráce splňuje koncept společensky odpovědného podnikání, pro jehož zavedení můžou mít firmy různé motivace. Pro podporované organizace je tato spolupráce jedním z možných zdrojů, jak rozvíjet svou činnost. Na základě studia dokumentů a také vedení polostrukturovaných rozhovorů s respondenty zjišťuji formy spolupráce organizace Sue Ryder s tržními partnery. Rozhovory navíc poskytují zhodnocení různých druhů partnerství z pohledu organizace Sue Ryder. Práce poskytuje přehled nejvýznamnějších forem spolupráce Sue Ryder s firmami a ukazuje, že tato mezisektorová spolupráce může s sebou přinášet benefity, ale i negativa pro podporovanou organizaci.
|
|
|
Zkušenosti s distanční výukou na vybrané konzervatoři a základní škole
Řehák, Vojtěch ; Svobodová, Zuzana (vedoucí práce) ; Dvořáková, Danuše (oponent)
Bakalářská práce je zaměřená na zkušenosti s distančním vzděláváním v pokročilé době pandemie COVID-19. Popisuje, jak se vyvíjelo distanční vzdělávání na dvou vzdělávacích institucích - na konzervatoři a na základní škole. Teoretická část bakalářské práce bude zaměřena na vytvoření vhodného konceptuálního rámce a bude se zabývat základní terminologií vztahující se k formám vzdělávání, popisem distančního vzdělávání, platforem a analýzou České školní inspekce i MŠMT k distančnímu vzdělávání. V teoretické části bude dále periodizace průběhu školního roku 2020/2021 s uvedenými výsledky vzdělávání. Cílem bakalářské práce je popsat průběh distančního vzdělávání a vybrat příklady pozitivní zkušenosti během distanční výuky na vybrané ZŠ a konzervatoři a identifikovat jejich možné využití v tradiční výuce. Výsledková část definuje pět různých kategorií popisující průběh distančního vzdělávání. Detailně popisuje zkušenosti s distanční výukou z hlediska organizace, z hlediska absence, výsledků vzdělávání, technologického zázemí a osobnosti pedagoga jako člověka. Dále charakterizuje základní kladné zkušenosti, které dotazovaní respondenti vyhodnotili jako využitelné v běžné výuce. Mezi takové kladné zkušenosti patří aktivní využívání kombinace prezenčního i distančního vzdělávání, stálé využívání platforem...
|
|
| |
|
|
Automated Verification in HW/SW Co-design
Charvát, Lukáš ; Kubátová, Hana (oponent) ; Řehák, Vojtěch (oponent) ; Vojnar, Tomáš (vedoucí práce)
The subject of the thesis is to design new hardware verification techniques optimized for a process of HW/SW co-design in which hardware and software are developed in parallel to speed up the development of new embedded systems. Currently, microprocessor co-design tools typically allow to verify designs by simulation and/or functional verification. However, even extensive functional verification can miss some non-trivial bugs. Therefore, formal verification has become more and more desirable in recent years. As opposed to testing and bug-hunting techniques that only aim at detecting flaws, the goal of formal verification is to rigorously prove that the system is indeed correct. Formal verification is, however, a very demanding task, and even though a lot of progress has been achieved in this area, formal verification is far from being able to fully automatically check all relevant properties of complex designs without a significant and costly human involvement in the verification process. The thesis deals with these challenges by focusing on verification techniques based on formal approaches, but possibly relaxing or limiting their precision and generality to achieve full automation. Further, the thesis also focuses on the efficiency of the proposed techniques and their ability to deliver continuous feedback about the verification process. Special attention is devoted to the development of formal methods for checking the equivalence of microprocessor designs on various levels of abstraction. Although these designs cannot be behaviorally equivalent, they are required to give mutually corresponding results when executing the same input program, which is a property difficult to achieve. As another considered topic, the thesis proposes methods for checking correctness of mechanisms preventing data and control hazards in single-pipelined implementations of microprocessors. The approaches described in this thesis has been implemented in the form of several tools which, after examining designs of multiple pipelined microprocessors, were able to deliver promising experimental results.
|
|
|
Olympijské parky v ČR,využití v marketingu vybraných firem
Řehák, Vojtěch ; Mikeš, Jiří (vedoucí práce) ; Kindová, Alena (oponent)
Tato diplomová práce se zabývá problematikou pořádání olympijských parků v České republice a jejich využitím v marketingových strategiích vybraných firem. Hlavním cílem je zhodnocení analýzy marketingové strategie tří hlavních partnerů. Šlo o společnosti Škoda Auto, Skupina ČEZ a Pilsner Urquell. První kapitola se zaměřuje na teorii obecného marketingu. Druhá kapitola pojednává o teorii sportovního marketingu a soustředí se především na marketingový a komunikační mix ve sportu. V další části jsou popsány jednotlivé olympijské parky. Zároveň zde proběhne analýza komunikace hlavních partnerů v průběhu provozu hlavního parku Rio-Lipno. Poslední kapitola obsahuje zhodnocení přínosu olympijských parků a partnerských marketingových aktivit a návrhy pro příští dvě olympiády.
|
|
|
Marketingová analýza hotelu Louis Leger
Řehák, Vojtěch ; Sedláček, Jiří (vedoucí práce) ; Soudková, Hana (oponent)
Tato bakalářská práce se zabývá analýzou marketingové strategie hotelu Louis Leger. Hlavním cílem práce je zhodnotit tuto strategii a případně navrhnout určité změny. První část práce je zaměřena na teorii internetového marketingu, marketingového mixu a SWOT analýzy. Ve druhé části jsou informace o společnosti Czech Inn Hotels a hotelu Louis Leger. V další části je již samotná analýza, která proběhla hlavně na základě dat z interního hotelového systému a vlastních zkušeností s prací v tomto hotelu. Součástí analýzy je marketingový mix a SWOT analýza. Poslední část obsahuje zhodnocení strategie a návrhy na zlepšení.
|
host ::
RSS.