Detail publikace

Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems

CHARVÁT, L.; SMRČKA, A.; VOJNAR, T. Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems. Proceedings of the 15th International Conference on Computer Aided Systems Theory (EUROCAST 2015). Las Palmas de Grand Canaria: The Universidad de Las Palmas de Gran Canaria, 2015. p. 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
anglicky
Autoři
Charvát Lukáš, Ing., Ph.D.
Smrčka Aleš, Ing., Ph.D. (UITS)
Vojnar Tomáš, prof. Ing., Ph.D. (UITS)
Klíčová slova

microprocessor analysis, pipelined execution, WAW hazard, WAR hazard, formal verification, parameterized systems

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)
ISBN
978-84-606-5438-4
Vydavatel
The Universidad de Las Palmas de Gran Canaria
Místo
Las Palmas de Grand Canaria
BibTeX
@inproceedings{BUT119797,
  author="Lukáš {Charvát} and Aleš {Smrčka} and Tomáš {Vojnar}",
  title="Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems",
  booktitle="Proceedings of the 15th International Conference on Computer Aided Systems Theory (EUROCAST 2015)",
  year="2015",
  pages="193--194",
  publisher="The Universidad de Las Palmas de Gran Canaria",
  address="Las Palmas de Grand Canaria",
  isbn="978-84-606-5438-4"
}
Nahoru