|
|
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ů.
|
|
|
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ů.
|
|
| |
|
|
Combined linear and non-linear time heteronymous damping in internal dynamics of non-linear parametric systems
Hortel, Milan ; Škuderová, Alena
In the process of the design of high speed planetary gear systems with minimum dimensions and masses are not sufficiently in advance known many of the functional dependencies of parameters such as constant or time heteronomous damping in gear mesh of kinematic pairs, etc. Therefore, it is necessary due to the safety and reliability of these systems that the basic research in this field dealt with this problem deeper both qualitatively and quantitatively, analytically and numerically. The values and functional dependencies, for example of damping parameters of solved systems, are often only estimated. Effects of variations in the size of the estimated parameters from their true values is solved in a wider variation expected ranges, including the impact on the internal dynamics of these systems. In this study are analyzed bifurcation resonance characteristics of relative motion in the gear mesh of system with combined linear and non-linear - quadratic time heteronymous damping on the model of one branch of power flow of pseudoplanetary weakly and strongly non-linear system with six degrees of freedom.
|
|
| |
|
|
Bifurcation characteristics in parametric systems with combined linear and non-linear damping
Hortel, Milan ; Škuderová, Alena
The damping or the damping forces represent certain speciality in the investigation of the internal dynamics of the transmission systems. The special significance has this damping parameter especially in the areas of impact effects in the high-speed light aircraft and mobile transmission constructions. On the example of gear mesh in one branch of forces-flow in the pseudoplanetary reducer deals the paper with some partial results of the analysis of the influence of combination damping, i.e. linear and non-linear damping, on the gear mesh dynamics.
|
|
|
K numerické analýze singularit v rezonančních charakteristikách nelineárních parametrických systémů s rázovými jevy v záběru ozubení
Hortel, Milan ; Škuderová, Alena
The impact effects in gear mesh represent specific phenomena in the dynamic investigation of highspeed light transmission systems with kinematic couplings. They are caused of greater dynamic than static-elastic deformations in meshing gear profiles. In term of internal dynamics they are influenced among others by time heteronomous stiffness functions in gear mesh and resonance tuning of stiffness level. The damping in gear mesh and in gear system is concerned significantly in the amplitude progress, greatness and phase shift of relative motion towards stiffness function alternatively towards its modify form in gear mesh. In consequence of these and another actions rise above resonance characteristics certain singular locations with jump amplitude course.
|
|
|
To some dynamic properties of parametric - heteronomous systems with internal kinematic couplings and split power flow
Hortel, Milan ; Škuderová, Alena
The contribution deals partly with the problems of influence of material damping of gearing by normal and inverse mesh and the effect of viscous damping of lubricant surrounding, i.e. the influence of oil during cog contact bounce in the gap - technological backlash and partly with the analysis of issue causation of sharp discontinuity locality in the resonance characteristics, which is associated with the cog contact bounce with the impact effects in dependence with given resonance tuning, the gear mesh duration term on stiffness level of the parametric stiffness function or the modify stiffness function, inclusive the time phase shifts of relative motion towards these stiffness function.
|
|
|
To influence of damping on impact effects in gear mesh
Hortel, Milan ; Škuderová, Alena
The motion equations of nonlinear parametric system of kinematic pair with elastic supported cog wheels were assembled on the basis of analytical Lagrange’s theory of mechanics, principle of virtual work, d’Alembert’s principle of conversion of kinetics problem onto statics and Lagrange’s release principle and analytical solved by means of equivalent nonlinear integrodifferential equations with solved kernels in the form of split Green’s resolvent. The influence of linear and nonlinear damping in the several phasis of gear engagement onto impact effects in gear mesh is solved in the contribution by means of numerical simulation in MATLAB/Simulink.
|
|
| |
guest ::
