HADES: Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems
Hardware Architecture
2016-12-16 v1
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.
Cite
@article{arxiv.1612.04986,
title = {HADES: Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems},
author = {Lukáš Charvát and Aleš Smrčka and Tomáš Vojnar},
journal= {arXiv preprint arXiv:1612.04986},
year = {2016}
}
Comments
In Proceedings MEMICS 2016, arXiv:1612.04037