Detail publikace

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

CHARVÁT, L.; SMRČKA, A.; VOJNAR, T. 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. p. 83-89. ISBN: 978-1-4673-6858-2.
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
anglicky
Autoři
Charvát Lukáš, Ing., Ph.D.
Smrčka Aleš, Ing., Ph.D. (UITS)
Vojnar Tomáš, prof. Ing., Ph.D. (UITS)
URL
Klíčová slova

automatic formal verification, microprocessor, register transfer level description, parameterised system, RAW hazard

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)
ISBN
978-1-4673-6858-2
Vydavatel
IEEE Computer Society
Místo
Austin, TX
DOI
10.1109/MTV.2014.21
UT WoS
000380373200017
EID Scopus
2-s2.0-84945181643
BibTeX 
@inproceedings{BUT119794,
  author="Lukáš {Charvát} and Aleš {Smrčka} and Tomáš {Vojnar}",
  title="Using Formal Verification of Parameterized Systems in RAW Hazard Analysis in Microprocessors",
  booktitle="Proceedings of 15th International Workshop on Microprocessor Test and Verification (MTV 2014)",
  year="2014",
  pages="83--89",
  publisher="IEEE Computer Society",
  address="Austin, TX",
  doi="10.1109/MTV.2014.21",
  isbn="978-1-4673-6858-2",
  url="http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=7087240"
}
Nahoru