Článek ve sborníku konference

CHARVÁT Lukáš, SMRČKA Aleš a VOJNAR Tomáš. Using Formal Verification of Parameterized Systems in RAW Hazard Analysis in Microprocessors. In: Proceedings of 15th International Workshop on Microprocessor Test and Verification (MTV 2014). Austin, TX: IEEE Computer Society, 2014, s. 83-89. ISBN 978-1-4673-6858-2. Dostupné z: http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=7087240
Jazyk publikace:angličtina
Název publikace:Using Formal Verification of Parameterized Systems in RAW Hazard Analysis in Microprocessors
Název (cs):Analýza RAW hazardů v mikroprocesorech pomocí formální verifikace parametrizovaných systémů
Strany:83-89
Sborník:Proceedings of 15th International Workshop on Microprocessor Test and Verification (MTV 2014)
Konference:Microprocessor Test and Verification 2014
Místo vydání:Austin, TX, US
Rok:2014
URL:http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=7087240
ISBN:978-1-4673-6858-2
DOI:10.1109/MTV.2014.21
Vydavatel:IEEE Computer Society
Klíčová slova
automatic formal verification, microprocessor, register transfer level description, parameterised system, RAW hazard
Anotace
Implementace linky zřetězení v procesorech s aplikačně-specifickým využitím je nachylná k chybám, z čehož plyne potřeba pro odpovídající verifikaci výsledných návrhů. Pro tento účel byla navržena řada technik, znichž ovšem většina vyžaduje výrazné manuální zapojení ze strany vývojáře. Článek představuje nový automatizovaný přístup pro detekci hazardů typu RAW (read-after-write) v linkách s zřetězení, které zpracovávají instrukce ve vstupním pořadí. Přístup je založen na statické analýze datových cest použité k nalezení potenciálních zdrojů hazardů, která je následována převodem nalezených problémových částí do podoby parametrizovaného systému. Tento systém je poté formálně verifikován pro ověření, zda jsou veškeré nalezené poteciální hazardy správně ošetřeny. Přístup byl také úspěšně aplikován na několika netriviálních modelech mikroprocesorů.
BibTeX:
@INPROCEEDINGS{
   author = {Luk{\'{a}}{\v{s}} Charv{\'{a}}t and Ale{\v{s}}
	Smr{\v{c}}ka and Tom{\'{a}}{\v{s}} Vojnar},
   title = {Using Formal Verification of Parameterized Systems
	in RAW Hazard Analysis in Microprocessors},
   pages = {83--89},
   booktitle = {Proceedings of 15th International Workshop on Microprocessor
	Test and Verification (MTV 2014)},
   year = 2014,
   location = {Austin, TX, US},
   publisher = {IEEE Computer Society},
   ISBN = {978-1-4673-6858-2},
   doi = {10.1109/MTV.2014.21},
   language = {english},
   url = {http://www.fit.vutbr.cz/research/view_pub.php.cs?id=10742}
}

Vaše IPv4 adresa: 100.24.209.47