Publication Details

Hades: Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems

CHARVÁT, L.; SMRČKA, A.; VOJNAR, T. Hades: Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems. In Proceedings 11th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2016). Electronic Proceedings in Theoretical Computer Science, EPTCS. Electronic Proceedings in Theoretical Computer Science. Brno: Faculty of Informatics MU, 2016. p. 87-93. ISBN: 978-80-210-8362-2. ISSN: 2075-2180.
Czech title
Hades: analýza hazardů v mikroprocesorech s využitím formální verifikace parametrických systémů
Type
conference paper
Language
English
Authors
Charvát Lukáš, Ing., Ph.D.
Smrčka Aleš, Ing., Ph.D. (DITS)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS)
URL
Keywords

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

Abstract

Hades is a fully automated verification tool for pipeline-based microprocessors that aims at flaws caused by improperly handled data hazards. It focuses on single-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.

Published
2016
Pages
87–93
Journal
Electronic Proceedings in Theoretical Computer Science, EPTCS, vol. 2016, no. 233, ISSN 2075-2180
Proceedings
Proceedings 11th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2016)
Series
Electronic Proceedings in Theoretical Computer Science
Conference
MEMICS'16 Doctoral Workshop on Mathematical and Engineering Methods in Computer Science , Telč, CZ
ISBN
978-80-210-8362-2
Publisher
Faculty of Informatics MU
Place
Brno
DOI
10.4204/EPTCS.233.9
UT WoS
000390333200010
EID Scopus
2-s2.0-85018638270
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"
}
Files
Back to top