Detail publikace

Hades: Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems

CHARVÁT, L. SMRČKA, A. VOJNAR, T.

Originální název

Hades: Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems

Typ

článek ve sborníku ve WoS nebo Scopus

Jazyk

angličtina

Originální abstrakt

Hades is a fully automated verification tool for pipeline-based microprocessors that aims at flaws caused by improperly handled data hazards. It focuses onsingle-pipeline microprocessors designed at the register transfer level (RTL)and deals with read-after-write, write-after-write, and write-after-read hazards. Hades combines several techniques, including data-flow analysis, error pattern matching, SMT solving, and abstract regular model checking. It has been successfully tested on several microprocessors for embedded applications.

Klíčová slova

automated tool, formal verification, pipeline-based microprocessors, data hazards

Autoři

CHARVÁT, L.; SMRČKA, A.; VOJNAR, T.

Vydáno

13. 12. 2016

Nakladatel

Faculty of Informatics MU

Místo

Brno

ISBN

978-80-210-8362-2

Kniha

Proceedings 11th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2016)

Edice

Electronic Proceedings in Theoretical Computer Science

ISSN

2075-2180

Periodikum

Electronic Proceedings in Theoretical Computer Science, EPTCS

Ročník

2016

Číslo

233

Stát

neuvedeno

Strany od

87

Strany do

93

Strany počet

7

URL

http://eptcs.web.cse.unsw.edu.au/paper.cgi?MEMICS2016.9

BibTex

@inproceedings{BUT132606,
  author="Lukáš {Charvát} and Aleš {Smrčka} and Tomáš {Vojnar}",
  title="Hades: Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems",
  booktitle="Proceedings 11th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2016)",
  year="2016",
  series="Electronic Proceedings in Theoretical Computer Science",
  journal="Electronic Proceedings in Theoretical Computer Science, EPTCS",
  volume="2016",
  number="233",
  pages="87--93",
  publisher="Faculty of Informatics MU",
  address="Brno",
  doi="10.4204/EPTCS.233.9",
  isbn="978-80-210-8362-2",
  issn="2075-2180",
  url="http://eptcs.web.cse.unsw.edu.au/paper.cgi?MEMICS2016.9"
}

Dokumenty

1612.04986.pdf