Detail publikace
Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems
microprocessor analysis, pipelined execution, WAW hazard, WAR hazard, formal verification, parameterized systems
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).
@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"
}