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. |
ArXived at: https://dx.doi.org/10.4204/EPTCS.233.9 | bibtex | |
Comments and questions to: eptcs@eptcs.org |
For website issues: webmaster@eptcs.org |