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. In Computer Aided Systems Theory - EUROCAST 2015. Lecture Notes in Computer Science. Lecture Notes in Computer Science. Zurich: Springer International Publishing, 2015. p. 605-614. ISBN: 978-3-319-27340-2. ISSN: 0302-9743.
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)
URL
Klíčová slova

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

Abstrakt

Současný tlak na rapidní vývojový cyklus mikroprocesorů zahrnující linku zřetězení vede k vysokým požadavkům na použití automatizovaných technik při návrhu i při verikaci. V článku je prezetována automatizovaná technika využívající statickou analýzu datových cest a formální verifikaci parametrizovaných systémů za účelem odhalení chyb způsobených nevhodným řešením datových hazardů. Zvláštně se jako doplněk k read-after-write hazardům článek zaměruje na write-after-write a write-after-read hazardy v mikroprocesorech s jednou linkou zřetězení.

Rok
2015
Strany
605–614
Časopis
Lecture Notes in Computer Science, roč. 9520, č. 1, ISSN 0302-9743
Sborník
Computer Aided Systems Theory - EUROCAST 2015
Řada
Lecture Notes in Computer Science
ISBN
978-3-319-27340-2
Vydavatel
Springer International Publishing
Místo
Zurich
DOI
10.1007/978-3-319-27340-2_75
UT WoS
000376687100075
EID Scopus
2-s2.0-84952306064
BibTeX 
@inproceedings{BUT120023,
  author="Lukáš {Charvát} and Aleš {Smrčka} and Tomáš {Vojnar}",
  title="Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems",
  booktitle="Computer Aided Systems Theory - EUROCAST 2015",
  year="2015",
  series="Lecture Notes in Computer Science",
  journal="Lecture Notes in Computer Science",
  volume="9520",
  number="1",
  pages="605--614",
  publisher="Springer International Publishing",
  address="Zurich",
  doi="10.1007/978-3-319-27340-2\{_}75",
  isbn="978-3-319-27340-2",
  issn="0302-9743",
  url="http://link.springer.com/content/pdf/10.1007%2F978-3-319-27340-2_75.pdf"
}
Nahoru