Ing. Lukáš Charvát

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.
Jazyk publikace:angličtina
Název publikace:Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems
Název (cs):Analýza hazardů v mikroprocesorech pomocí formální analýzy parametrizovaných systémů
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
Místo vydání:Las Palmas de Grand Canaria, ES
Rok:2015
ISBN:978-84-606-5438-4
Vydavatel:Universidad de Las Palmas de Gran Canaria
Klíčová slova
microprocessor analysis, pipelined execution, WAW hazard, WAR hazard, formal verification, parameterized systems
Anotace
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). 
Abstrakt
Implementation of pipeline-based execution of instructions in purpose-specific microprocessors is an error prone task, which implies a need of proper verification of the resulting designs. Our long-term goal is to develop a set of verification techniques with formal roots, each of them specialised in checking absence of a certain kind of errors in purpose-specific microprocessors. The main idea is that, this way, a high degree of automation and scalability can be achieved since only parts of a design related to a specific error are to be investigated. In our previous works, we proposed, with the above goal in mind, fully automated approaches for checking correctness of the implementation of individual instructions and for verifying absence of read-after-write (RAW) hazards. In this paper, we extend our approach by aiming at write-after-write (WAW) and write-after-read (WAR) in microprocessors with a single pipeline.
BibTeX:
@INPROCEEDINGS{
   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 = {http://www.fit.vutbr.cz/research/view_pub.php.cs?id=10767}
}

Vaše IPv4 adresa: 52.200.130.163
Přepnout na https