|
|
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.
|
|
|
Testing of generated C compilers for processors in embedded systems
Dolíhal, Luděk ; Kubátová, Hana (oponent) ; Vojnar, Tomáš (oponent) ; Hruška, Tomáš (vedoucí práce)
The embedded systems have become essential for our everyday lives. They are usually highly specialized and optimized single purpose devices. The cores of this devices are usually composed of one or more application specific instruction-set processors. This dissertation thesis is focused on testing of tools for design of application specific instruction set processors (ASIP) and ASIPs itself. The aim is to create a system, that allows testing of the tools such as compiler, assembler, disassembler or debugger. Nevertheless, there is also need for more complex tests, for example integration tests, that ensure there is no incompatibility between the tools. Author created with support of continuous integration server an environment, that helps to reveal and fix errors during the design of the application specific processors and moreover this environment is automatized up to certain point.
|
|
|
Optimalizace testu digitálního obvodu multifunkčními prvky
Stareček, Lukáš ; Gramatová, Elena (oponent) ; Kubátová, Hana (oponent) ; Kotásek, Zdeněk (vedoucí práce)
Tato práce se zabývá možností optimalizace testu číslicových obvodů pomocí multifunkčních logických hradel. Nejdůležitější částí práce je vysvětlení samotného principu optimalizace, který je popsán také formálními matematickými prostředky. Na základě tohoto popisu je v práci prezentováno několik možností využití. Ukázána je optimalizace testovatelnosti obdobná metodě vkládání testovacích bodů a jednoduchá metodika založena na základě SCOAP. Těžištěm práce je však metodika, která byla vytvořena pro optimalizaci testu obvodu. Ta byla implementována v podobě softwarových nástrojů. V práci jsou následně prezentovány výsledky použití těchto nástrojů na úloze snížení počtu testovacích vektorů se zachováním pokrytí poruch pro různé obvody včetně testovací sady ISCAS 85. Část práce je věnována také různým principům a technologiím tvorby multifunkčních logických hradel. Některá vybraná hradla z těchto technologií jsou podrobena simulacím elektronických vlastností ve SPICE. Na základě principů prezentované metodiky a výsledků simulací multifunkčních hradel je také provedena analýza a rozbor různých problémů jako je platnost testu modifikovaného obvodu a vhodnost jednotlivých technologií multifunkčních hradel pro danou metodiku. Výsledky analýz a provedených experimentů je potvrzeno, že pomocí multifunkčních hradel lze optimalizovat diagnostické vlastnosti obvodu takovým způsobem, aby došlo k požadovaným úpravám parametrů výsledných testů obvodů při minimálních dopadech na kvalitu a věrohodnost těchto testů.
|
|
|
Semi - analytické výpočty a spojitá simulace
Kopřiva, Jan ; Kubátová, Hana (oponent) ; Novitzká,, Valerie (oponent) ; Kunovský, Jiří (vedoucí práce)
Práce se zabývá urychlením a zpřesněním numerických výpočtů, především pak úloh z oblasti diferenciálního počtu. Zmíněné vlastnosti jsou charakteristické pro skupinu výpočtů nazývaných semi-analytické. Jednou z možností urychlení výpočtu obyčejných diferenciálních rovnic je paralelizace. Předkládaná paralelizace je založena na transformaci numerického řešení do aritmetiky zbytkových tříd, která je rozšířena o výpočty s pohyblivou čárkou. Součástí práce je i nový algoritmus pro součin celých čísel a jeho následnou redukci zvoleným modulem. Vzhledem k aplikacím v diferenciálním počtu jsou v práci popsány upravené integrační metody - Eulerova, Runge - Kutta a Taylorova s využitím aritmetiky zbytkových tříd. V závěru jsou také nástíněny další možnosti rozšíření a urychlení popsané aritmetiky.
|
|
|
Paralelní výpočetní architektury založené na numerické integraci
Kraus, Michal ; Kubátová, Hana (oponent) ; Kollár,, Ján (oponent) ; Kunovský, Jiří (vedoucí práce)
Předkládaná práce se zabývá simulací spojitých systémů popsaných soustavou diferenciálních rovnic nebo blokového diagramu. Zcela běžné je numerické řešení diferenciálních rovnic a používání simulačních programových celků (Matlab, Maple, TKSL). Pro řešení diferenciálních rovnic je použita metoda Taylorovy řady. Bylo dokázáno, že metoda dosahuje velké přesnosti a rychlosti a nabízí možnost paralelního provádění a tím další urychlení výpočtu. Hlavní část práce obsahuje popis návrhu a realizace specializovaného paralelního systému provádějící výpočet numerické integrace v~několika variantách a jejich porovnání.
|
|
| |
|
| |
|
|
Political Apologies and Conservatism
Mussenden, William James Silveira ; Kubátová, Hana (vedoucí práce) ; Halamka, Tomáš (oponent)
Conservatism and political apologies share a paradoxical relationship, commonly viewed as contradictory, yet upon closer inspection reveal more similarities than expected. This apparent contradiction stems primarily from the varying interpretations and applications of these concepts across different academic disciplines and areas of discourse. Existing interpretations, such as Michael Cunningham's claim that conservatism is more compatible with political apologies than other major western ideologies, are based on broad assumptions. This thesis expands on Cunningham's findings by adopting an intersectional approach to scrutinize the concepts of conservatism and political apologies, in particular within the context of Canadian parliamentary speeches. The thesis answers: are we or are we not able to conceptually locate political apologies within conservatism? Whatever the answer might be to this first question, can we find empirical evidence of that conceptual relationship in a real world context? Guided by the dual enquiries of the conceptual placement of political apologies within conservatism and empirical evidence of this relationship, the research draws upon the morphological analysis of ideologies as proposed by Michel Freeden. The study commences with the exploration of the conservative concept...
|
|
|
Protivládní protesty v ČR a na Slovensku během pandemie COVID-19
Klemš, Jan ; Guasti, Petra (vedoucí práce) ; Kubátová, Hana (oponent)
Bakala0r0ska0 pra0ce se zaby0va0 vy0vojem obc0anske0 a neobc0anske0 spolec0nosti v C0eske0 republice a na Slovensku be0hem pandemie COVID-19 zkouma0ni0m protestu0 v obou zemi0ch. Ci0lem pra0ce je zjistit, do jake0 mi0ry byly protesty v obou zemi0ch manifestaci0 obc0anske0 nebo neobc0anske0 spolec0nosti a zda jsou protesty du0kazem odolnosti nebo kr0ehkosti demokracie. Pra0ce take0 srovna0va0 protivla0dni0 protesty v C0eske0 republice a na Slovensku a zkouma0, zda existuji0 specificke0 faktory ovlivn0uji0ci0 jejich vy0voj a si0lu. Vy0zkum je proveden pomoci0 analy0zy dat z ACLED a na za0klade0 deskriptivni0ho komparativni0ho pr0i0stupu. Za0ve0r pra0ce navrhuje moz0ne0 du0vody pro rozdi0lny0 vy0voj protestu0 v obou zemi0ch a nabi0zi0 moz0ne0 r0es0eni0 pro budouci0 vy0zkum tohoto te0matu.
|
|
| |
host ::
RSS.