|
|
Memory System Management for Colibri XScale PXA270 Platform
Mačišák, Lukáš ; Straka, Martin (referee) ; Šimek, Václav (advisor)
This Bachelor's Thesis describes platform Colibri XScale PXA270, analyses potential usage of DMA transfers on this platform and describes principles of work with flash and SDRAM memories. Thesis includes design and implementation of firmware for servicing memory systems on this platform. One part of this thesis is also the description and implementation of tests for semiconductor memories with random access. The demonstrative application is implemented to show usage and functionality of this firmware.
|
|
|
RAM-Tester Design in VHDL
Charvát, Jiří ; Straka, Martin (referee) ; Strnadel, Josef (advisor)
This paper describes various approaches to hardware testing semiconductor memory. We describe the priciple of basic memory types, the way which each of them stores information and their comunication protocol. Following part deals with common failures which may occur in the memory. The section also describes the implementation of memory model and tester designed in VHDL language. It is possible to inject some errors into memory, which are later detected by the tester. The final section shows the response of tester to various error types according to used error detection method. The paper is especially focused on failure detection by variants of march test.
|
|
|
Program Loop Unwinding in the 2LS Framework
Nečas, František ; Vojnar, Tomáš (referee) ; Malík, Viktor (advisor)
Cílem této práce je navrhnout vylepšený mechanismus rozbalování smyček pro analyzátor 2LS. 2LS je nástroj pro statickou analýzu C programů založený na usuzování o programech pomocí SMT solveru. Kombinuje několik běžných verifikačních technik do algoritmu zvaného k I k I. Jednou z klíčových součástí tohoto algoritmu je rozbalování smyček programu. Současné řešení bohužel neumožňuje správně rozbalovat smyčky obsahující operace s dynamicky alokovanou pamětí. Námi navrhované řešení je založeno na rozbalování smyček v GOTO programu namísto SSA formy, díky čemuž je možné správně pracovat s dynamickými objekty a operacemi s nimi. Navržené řešení bylo implementováno v nástroji 2LS a naše experimenty na sadě testů z mezinárodní soutěže ve verifikaci software (SV-COMP) ukazují, že zvyšuje korektnost analýzy programů pracujících s dynamickými objekty.
|
|
|
Program Loop Unwinding in the 2LS Framework
Nečas, František ; Vojnar, Tomáš (referee) ; Malík, Viktor (advisor)
Cílem této práce je navrhnout vylepšený mechanismus rozbalování smyček pro analyzátor 2LS. 2LS je nástroj pro statickou analýzu C programů založený na usuzování o programech pomocí SMT solveru. Kombinuje několik běžných verifikačních technik do algoritmu zvaného k I k I. Jednou z klíčových součástí tohoto algoritmu je rozbalování smyček programu. Současné řešení bohužel neumožňuje správně rozbalovat smyčky obsahující operace s dynamicky alokovanou pamětí. Námi navrhované řešení je založeno na rozbalování smyček v GOTO programu namísto SSA formy, díky čemuž je možné správně pracovat s dynamickými objekty a operacemi s nimi. Navržené řešení bylo implementováno v nástroji 2LS a naše experimenty na sadě testů z mezinárodní soutěže ve verifikaci software (SV-COMP) ukazují, že zvyšuje korektnost analýzy programů pracujících s dynamickými objekty.
|
|
|
Memory System Management for Colibri XScale PXA270 Platform
Mačišák, Lukáš ; Straka, Martin (referee) ; Šimek, Václav (advisor)
This Bachelor's Thesis describes platform Colibri XScale PXA270, analyses potential usage of DMA transfers on this platform and describes principles of work with flash and SDRAM memories. Thesis includes design and implementation of firmware for servicing memory systems on this platform. One part of this thesis is also the description and implementation of tests for semiconductor memories with random access. The demonstrative application is implemented to show usage and functionality of this firmware.
|
|
|
RAM-Tester Design in VHDL
Charvát, Jiří ; Straka, Martin (referee) ; Strnadel, Josef (advisor)
This paper describes various approaches to hardware testing semiconductor memory. We describe the priciple of basic memory types, the way which each of them stores information and their comunication protocol. Following part deals with common failures which may occur in the memory. The section also describes the implementation of memory model and tester designed in VHDL language. It is possible to inject some errors into memory, which are later detected by the tester. The final section shows the response of tester to various error types according to used error detection method. The paper is especially focused on failure detection by variants of march test.
|
guest ::
