Detail publikace
Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems
Smrčka Aleš, Ing., Ph.D. (UITS FIT VUT)
Vojnar Tomáš, prof. Ing., Ph.D. (UITS FIT VUT)
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{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" }