HADES: Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems

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-afte...

Full description

Bibliographic Details
Published in:Electronic Proceedings in Theoretical Computer Science
Main Authors: Lukáš Charvát, Aleš Smrčka, Tomáš Vojnar
Format: Article
Language:English
Published: Open Publishing Association 2016-12-01
Online Access:http://arxiv.org/pdf/1612.04986v1