2016/12/15 by Lukáš Charvát, Aleš Smrčka, Tomáš Vojnar
Computer Science · #cs.AR
paper · pdf · doi:10.4204/eptcs.233.9
published as EPTCS 233, 2016, pp. 87-93 · In Proceedings MEMICS 2016, arXiv:1612.04037
arxiv created 2016/12/15 · arxiv updated 2016/12/16
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.