Publication Details

Hades: Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems

CHARVÁT Lukáš, SMRČKA Aleš and VOJNAR Tomáš. 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, vol. 2016. Brno: Faculty of Informatics MU, 2016, pp. 87-93. ISBN 978-80-210-8362-2. ISSN 2075-2180. Available from: http://eptcs.web.cse.unsw.edu.au/paper.cgi?MEMICS2016.9
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. (DITS FIT BUT)
Smrčka Aleš, Ing., Ph.D. (DITS FIT BUT)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT)
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, 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 - 11th 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, CZ
DOI
10.4204/EPTCS.233.9
UT WoS
000390333200010
EID Scopus
2-s2.0-85018638270
BibTeX 
@INPROCEEDINGS{FITPUB11312,
   author = "Luk\'{a}\v{s} Charv\'{a}t and Ale\v{s} Smr\v{c}ka and Tom\'{a}\v{s} Vojnar",
   title = "Hades: Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems",
   pages = "87--93",
   booktitle = "Proceedings 11th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2016)",
   series = "Electronic Proceedings in Theoretical Computer Science",
   journal = "Electronic Proceedings in Theoretical Computer Science",
   volume = 2016,
   number = 233,
   year = 2016,
   location = "Brno, CZ",
   publisher = "Faculty of Informatics MU",
   ISBN = "978-80-210-8362-2",
   ISSN = "2075-2180",
   doi = "10.4204/EPTCS.233.9",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/11312"
}
Back to top