Publication result detail

Hades: Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems

CHARVÁT, L.; SMRČKA, A.; VOJNAR, T.

Original Title

Hades: Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems

English Title

Hades: Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems

Type

Paper in proceedings (conference paper)

Original Abstract

Hades is a fully automated verification tool for pipeline-based microprocessors that aims at flaws caused by improperly handled data hazards. It focuses onsingle-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.

English abstract

Hades is a fully automated verification tool for pipeline-based microprocessors that aims at flaws caused by improperly handled data hazards. It focuses onsingle-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.

Keywords

automated tool, formal verification, pipeline-based microprocessors, data hazards

Key words in English

automated tool, formal verification, pipeline-based microprocessors, data hazards

Authors

CHARVÁT, L.; SMRČKA, A.; VOJNAR, T.

RIV year

2017

Released

13.12.2016

Publisher

Faculty of Informatics MU

Location

Brno

ISBN

978-80-210-8362-2

Book

Proceedings 11th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2016)

Edition

Electronic Proceedings in Theoretical Computer Science

ISBN

2075-2180

Periodical

Electronic Proceedings in Theoretical Computer Science, EPTCS

Volume

2016

Number

233

State

unknown

Pages from

87

Pages to

93

Pages count

7

URL

http://eptcs.web.cse.unsw.edu.au/paper.cgi?MEMICS2016.9

BibTex

@inproceedings{BUT132606,
  author="Lukáš {Charvát} and Aleš {Smrčka} and Tomáš {Vojnar}",
  title="Hades: Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems",
  booktitle="Proceedings 11th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2016)",
  year="2016",
  series="Electronic Proceedings in Theoretical Computer Science",
  journal="Electronic Proceedings in Theoretical Computer Science, EPTCS",
  volume="2016",
  number="233",
  pages="87--93",
  publisher="Faculty of Informatics MU",
  address="Brno",
  doi="10.4204/EPTCS.233.9",
  isbn="978-80-210-8362-2",
  issn="2075-2180",
  url="http://eptcs.web.cse.unsw.edu.au/paper.cgi?MEMICS2016.9"
}

Documents

1612.04986