HADES: Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems

Autor:	Charvát, Lukáš, Smrčka, Aleš, Vojnar, Tomáš
Rok vydání:	2016
Předmět:	Computer Science - Hardware Architecture
Zdroj:	EPTCS 233, 2016, pp. 87-93
Druh dokumentu:	Working Paper
DOI:	10.4204/EPTCS.233.9
Popis:	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. Comment: In Proceedings MEMICS 2016, arXiv:1612.04037
Databáze:	arXiv
Externí odkaz:	http://arxiv.org/abs/1612.04986 Zobrazit plný text záznamu View this record from Arxiv