Přístupnostní navigace
E-application
Search Search Close
Publication detail
CHARVÁT, L. SMRČKA, A. VOJNAR, T.
Original Title
Hades: Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems
Type
conference paper
Language
English
Original 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.
Keywords
automated tool, formal verification, pipeline-based microprocessors, data hazards
Authors
CHARVÁT, L.; SMRČKA, A.; VOJNAR, T.
Released
13. 12. 2016
Publisher
Faculty of Informatics MU
Location
Brno
ISBN
978-80-210-8362-2
Book
Proceedings 11th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2016)
Edition
Electronic Proceedings in Theoretical Computer Science
2075-2180
Periodical
Electronic Proceedings in Theoretical Computer Science, EPTCS
Year of study
2016
Number
233
State
unknown
Pages from
87
Pages to
93
Pages count
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" }