HADES: Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems

Lukáš Charvát
(Faculty of Information Technology, Brno University of Technology)
Aleš Smrčka
(IT4Innovations Centre of Excellence, FIT, Brno University of Technology)
Tomáš Vojnar
(IT4Innovations Centre of Excellence, FIT, Brno University of Technology)

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.

In Jan Bouda, Lukáš Holík, Jan Kofroň, Jan Strejček and Adam Rambousek: Proceedings 11th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2016), Telč, Czech Republic, 21st-23rd October 2016, Electronic Proceedings in Theoretical Computer Science 233, pp. 87–93.
Published: 13th December 2016.

ArXived at: https://dx.doi.org/10.4204/EPTCS.233.9 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org