Conference paperCHARVÁ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). Brno: Faculty of Informatics MU, 2016, pp. 8793. ISBN 9788021083622. ISSN 20752180. Available from: http://eptcs.web.cse.unsw.edu.au/paper.cgi?MEMICS2016.9  Publication language:  english 

Original title:  Hades: Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems 

Title (cs):  Hades: analýza hazardů v mikroprocesorech s využitím formální verifikace parametrických systémů 

Pages:  8793 

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

Conference:  MEMICS'16  11th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science 

Series:  Electronic Proceedings in Theoretical Computer Science 

Place:  Brno, CZ 

Year:  2016 

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

ISBN:  9788021083622 

Journal:  Electronic Proceedings in Theoretical Computer Science, Vol. 2016, No. 233, Sydney, AU 

ISSN:  20752180 

DOI:  10.4204/EPTCS.233.9 

Publisher:  Faculty of Informatics MU 

Keywords 

automated tool, formal verification, pipelinebased microprocessors, data hazards 
Annotation 

Hades is a fully automated verification tool for pipelinebased microprocessors that aims at flaws caused by improperly handled data hazards. It focuses on
singlepipeline microprocessors designed at the register transfer level (RTL)
and deals with readafterwrite, writeafterwrite, and writeafterread hazards. Hades combines several techniques, including dataflow analysis, error pattern matching, SMT solving, and abstract regular model checking. It has been successfully tested on several microprocessors for embedded applications. 
BibTeX: 

@INPROCEEDINGS{
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 = {8793},
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 = {9788021083622},
ISSN = {20752180},
doi = {10.4204/EPTCS.233.9},
language = {english},
url = {http://www.fit.vutbr.cz/research/view_pub.php?id=11312}
} 
