|
|
Automated Verification in HW/SW Co-design
Charvát, Lukáš ; Kubátová, Hana (referee) ; Řehák, Vojtěch (referee) ; Vojnar, Tomáš (advisor)
Předmětem dizertační práce je návrh nových technik pro verifikaci hardwaru, které jsou optimalizovány pro použití v procesu souběžného vývoje hardwaru a softwaru. V rámci tohoto typu vývoje je hardware spolu se software vyvíjen paralelně s cílem urychlit vývoj nových systémů. Současné nástroje pro tvorbu mikroprocesorů stavějící na tomto stylu vývoje obvykle umožňují vývojářům ověřit jejich návrh využitím různých simulačních technik a/nebo za pomoci tzv. funkční verifikace. Společnou nevýhodou těchto přístupů je, že se zaměřují pouze na hledání chyb. Výsledný produkt tedy může stále obsahovat nenalezené netriviální defekty. Z tohoto důvodu se v posledních letech stává stále více žádané nasazení formálních metod. Na rozdíl od výše uvedených přístupů založených na hledání chyb, se formální verifikace zaměřuje na dodání rigorózního důkazu, že daný systém skutečně splňuje požadované vlastnosti. I když bylo v uplynulých letech v této oblasti dosaženo značného pokroku, tak aktuální formální přístupy nemají zdaleka schopnost plně automaticky prověřit všechny relevantní vlastnosti verifikovaného návrhu bez výrazného a často nákladného zapojení lidí v rámci verifikačního procesu. Tato práce se snaží řešit problém s automatizací verifikačního procesu jejím zaměřením na verifikační techniky, ve kterých je záměrně kladen menší důraz na jejich přesnost a obecnost, za cenu dosažení plné automatizace (např. vyloučením potřeby ručně vytvářet modely prostředí). Dále se práce také zaměřuje na efektivitu navrhovaných technik a jejich schopnost poskytovat nepřetržitou zpětnou vazbu o verifikačním procesu (např. v podobě podání informace o aktuálním stavu pokrytí). Zvláštní pozornost je pak věnována vývoji formálních metod ověřujících ekvivalenci návrhů mikroprocesorů na různých úrovních abstrakce. Tyto návrhy se mohou lišit ve způsobu, jakým jsou vnitřně zpracovány programové instrukce, nicméně z vnějšího pohledu (daného např. obsahem registrů viditelných z pozice programátora) musí být jejich chování při provádění stejného vstupního programu shodné. Kromě těchto témat se práce také zabývá problematikou návrhu metod pro verifikaci správnosti mechanismů zabraňujících výskytu datových a řídících hazardů v rámci linky zřetězeného zpracování instrukcí. Veškeré metody popsané v této práci byly implementovány ve formě několika nástrojů. Aplikací těchto nástrojů pro verifikaci návrhů netriviálních procesorů bylo dosaženo slibných experimentálních výsledků.
|
|
|
Testing of generated C compilers for processors in embedded systems
Dolíhal, Luděk ; Kubátová, Hana (referee) ; Vojnar, Tomáš (referee) ; Hruška, Tomáš (advisor)
Vestavěné systémy se staly nepostradatelnými pro náš každodenní život. Jsou to obvykle úzce zaměřená, vysoce optimalizovaná, jednoúčelová zařízení. Jádro vestavěných zařízení obvykle tvoří jeden nebo více aplikačně specifických instrukčních procesorů. Tato disertační práce se zaměřuje na problematiku testování nástrojú pro návrh aplikačně specifických procesorů a následně i samotných aplikačne specifických procesorů. Snahou bylo vytvořit systém, ve kterém bude možné otestovat jednotlivé nástroje, jako například překladač, assembler, disassembler, debugger. Nicméně vyvstává také potřeba provádět složitější testy, například integrační, které zaručí, že mezi jednotlivými nástroji nevzniká nekompatibilita. Autor vytvořil s podporou přůběžně integračního serveru prostředí, které napomáhá odhalování a odstraňování chyb při návrhu aplikačně specifických procesorů a které je navíc do značné míry automatizované.
|
|
|
Digital circuits test optimization by multifunctional components
Stareček, Lukáš ; Gramatová, Elena (referee) ; Kubátová, Hana (referee) ; Kotásek, Zdeněk (advisor)
This thesis deals with the possibilities of digital circuit test optimization using multifunctional logic gates. The most important part of this thesis is the explanation of the optimization principle, which is also described by a formal mathematical apparatus. Based on this apparatus, the work presents several options. The optimization of testability analogous to inserting test points and simple methodology based on SCOAP is shown. The focus of work is a methodology created to optimize circuit tests. It was implemented in the form of software tools. Presented in this work are the results of using these tools to reduce the test vectors volume while maintaining fault coverage on various circuits, including circuits from the ISCAS 85 test set. Part of the work is devoted to the various principles and technology of creating multifunctional logic gates. Some selected gates of these technologies are subject to simulations of electronic properties in SPICE. Based on the principles of presented methodology and results of multifunctional gates simulations, analysis of various problems such as validity of the modified circuit test and the suitability of each multifunctional gate technology for the methodology was also made. The results of analysis and experiments confirm it is possible for the multifunctional logic gate to optimize circuit diagnostic properties in such a way that has achieved the required circuit test parameter modification with minimum impact on the quality and credibility of these tests.
|
|
|
Semi - analytical computations and continuous systems simulation
Kopřiva, Jan ; Kubátová, Hana (referee) ; Novitzká,, Valerie (referee) ; Kunovský, Jiří (advisor)
The thesis deals with speedup and accuracy of numerical computation, especially when differential equations are solved. Algorithms, which are fulling these conditions are named semi-analytical. One posibility how to accelerate computation of differential equation is paralelization. Presented paralelization is based on transformation numerical solution into residue number system, which is extended to floating point computation. A new algorithm for modulo multiplication is also proposed. As application applications in solution of differential calculus are the main goal it is discussed numeric integration with modified Euler, Runge - Kutta and Taylor series method in residue number system. Next possibilities and extension for implemented residue number system are mentioned at the end.
|
|
|
Parallel Computer Systems Based on Numerical Integrations
Kraus, Michal ; Kubátová, Hana (referee) ; Kollár,, Ján (referee) ; Kunovský, Jiří (advisor)
This thesis deals with continuous system simulation. The systems can be described by system of differential equations or block diagram. Differential equations are usually solved by numerical methods that are integrated into simulation software such as Matlab, Maple or TKSL. Taylor series method has been used for numerical solutions of differential equations. The presented method has been proved to be both very accurate and fast and also procesed in parallel systems. The aim of the thesis is to design, implement and compare a few versions of the parallel system.
|
|
| |
|
| |
|
|
Political Apologies and Conservatism
Mussenden, William James Silveira ; Kubátová, Hana (advisor) ; Halamka, Tomáš (referee)
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...
|
|
|
Anti-governmental protests in the Czech Republic and Slovakia during Covid-19 pandemic
Klemš, Jan ; Guasti, Petra (advisor) ; Kubátová, Hana (referee)
This bachelor's thesis examines the development of civil and uncivil society in the Czech Republic and Slovakia during the COVID-19 pandemic by examining protests in both countries. The aim of the thesis is to determine to what extent the protests in both countries were manifestations of civil or uncivil society and whether protests are a sign of resilience or fragility of democracy. The thesis also compares anti-government protests in the Czech Republic and Slovakia and examines whether there are specific factors influencing their development and strength. The research is conducted using analysis of data z ACLED and descriptive comparative approach. The conclusion of the thesis proposes possible reasons for the different development of protests in both countries and offers possible solutions for future research on this topic.
|
|
| |
guest ::
RSS feed.