Detail výsledku

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.
Typ
článek ve sborníku konference
Jazyk
anglicky
Autoři
Charvát Lukáš, Ing., Ph.D., UITS (FIT)
Smrčka Aleš, Ing., Ph.D., UITS (FIT)
Vojnar Tomáš, prof. Ing., Ph.D., UITS (FIT)
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.

Klíčová slova

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

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
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"
}
Projekty
Automatizovaná formální analýza a verifikace programů se složitými datovými a řídicími strukturami s předem neomezenou velikostí, GAČR, Standardní projekty, GA14-11384S, zahájení: 2014-01-01, ukončení: 2016-12-31, ukončen
Centrum excelence IT4Innovations, MŠMT, Operační program Výzkum a vývoj pro inovace, ED1.1.00/02.0070, zahájení: 2011-01-01, ukončení: 2015-12-31, ukončen
Spolehlivost a bezpečnost v IT, VUT, Vnitřní projekty VUT, FIT-S-14-2486, zahájení: 2014-01-01, ukončení: 2016-12-31, ukončen
Výzkumné skupiny
Pracoviště
Nahoru