Detail publikace

Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems

CHARVÁT Lukáš, SMRČKA Aleš a VOJNAR Tomáš. Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems. In: Proceedings of the 15th International Conference on Computer Aided Systems Theory (EUROCAST 2015). Las Palmas de Grand Canaria: Universidad de Las Palmas de Gran Canaria, 2015, s. 193-194. ISBN 978-84-606-5438-4.
Název česky
Analýza hazardů v mikroprocesorech pomocí formální analýzy parametrizovaných systémů
Typ
článek ve sborníku konference
Jazyk
angličtina
Autoři
Abstrakt

Implementace linky zřetězení v procesorech s aplikačně-specifickým využitím (angl., application-specific instruction set processors) je nachylná k chybám, z čehož plyne potřeba pro odpovídající verifikaci výsledných návrhů. Práce je součástí dlouhodobého záměru, který si klade za cíl vývoj verifikačních technik s formálními základy, kde se každá z technik zaměřuje na uřitý typ chyb vyskytujících se ve výše uvedených typech procesorů. Tímto přístupem může být dosaženo dobré škálovatelnosti a velkého stupně automatického zpracování, a to zejména z důvodu, že jsou verifikovány pouze části návrhu vázané k určitému typu chyby. Článek popisuje automatický přístup pro verikaci datavých hazardů typu WAW (write-after-write) a WAR (write-after-read) v mikroprocesorech s jednou linkou zřetězení. Navazuje tak na dřívejší práce, které se soustředily na oveření správnosti implementaci izolovaného zpracování instrukcí a verifikujících absenci hazardů typu RAW (read-after-write). 

Rok
2015
Strany
193-194
Sborník
Proceedings of the 15th International Conference on Computer Aided Systems Theory (EUROCAST 2015)
Konference
Fifteenth International Conference on Computer Aided Systems Theory , Las Palmas de Gran Canaria, ES
ISBN
978-84-606-5438-4
Vydavatel
Universidad de Las Palmas de Gran Canaria
Místo
Las Palmas de Grand Canaria, ES
BibTeX
@INPROCEEDINGS{FITPUB10767,
   author = "Luk\'{a}\v{s} Charv\'{a}t and Ale\v{s} Smr\v{c}ka and Tom\'{a}\v{s} Vojnar",
   title = "Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems",
   pages = "193--194",
   booktitle = "Proceedings of the 15th International Conference on Computer Aided Systems Theory (EUROCAST 2015)",
   year = 2015,
   location = "Las Palmas de Grand Canaria, ES",
   publisher = "The Universidad de Las Palmas de Gran Canaria",
   ISBN = "978-84-606-5438-4",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/10767"
}
Nahoru