Detail publikace

Using Formal Verification of Parameterized Systems in RAW Hazard Analysis in Microprocessors

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
Název česky
Analýza RAW hazardů v mikroprocesorech pomocí formální verifikace parametrizovaných systémů
Typ
článek ve sborníku konference
Jazyk
angličtina
Autoři
URL
Abstrakt

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ů.

Rok
2014
Strany
83-89
Sborník
Proceedings of 15th International Workshop on Microprocessor Test and Verification (MTV 2014)
Konference
Microprocessor Test and Verification 2014, Austin, TX, US
ISBN
978-1-4673-6858-2
Vydavatel
IEEE Computer Society
Místo
Austin, TX, US
DOI
UT WoS
000380373200017
EID Scopus
BibTeX
@INPROCEEDINGS{FITPUB10742,
   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 = "https://www.fit.vut.cz/research/publication/10742"
}
Nahoru