HADES: Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems
Luk\'a\v{s} Charv\'at (Faculty of Information Technology, Brno, University of Technology), Ale\v{s} Smr\v{c}ka (IT4Innovations Centre of, Excellence, FIT, Brno University of Technology), Tom\'a\v{s} Vojnar, (IT4Innovations Centre of Excellence, FIT, Brno University of Technology)
TL;DR
HADES is an automated verification tool that detects data hazards in pipeline microprocessors at the RTL level using formal methods, improving microprocessor reliability.
Contribution
The paper introduces HADES, a novel tool combining multiple formal verification techniques to automatically identify data hazards in pipeline microprocessors.
Findings
Successfully tested on embedded microprocessors
Detects read-after-write, write-after-write, and write-after-read hazards
Automates hazard detection process
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsEmbedded Systems Design Techniques · Radiation Effects in Electronics · Formal Methods in Verification