Detail publikačního výsledku

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

Anglický název

Hades: Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems

Druh

Stať ve sborníku v databázi WoS či Scopus

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.

Anglický 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

Klíčová slova v angličtině

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

Autoři

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

Rok RIV

2017

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

Svazek

2016

Číslo

233

Stát

Australské společenství

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",
  url="http://eptcs.web.cse.unsw.edu.au/paper.cgi?MEMICS2016.9"
}

Dokumenty

1612.04986