Publication detail

Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems

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

Original Title

Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems

Type

conference paper

Language

English

Original Abstract

The current stress on having a rapid development cycle for microprocessors featuring pipeline-based execution leads to a high demand of automated techniques supporting the design, including a support for its verification. We present an automated technique exploiting static analysis of data paths and formal verification of parameterized systems in order to discover flaws caused by improperly handled data hazards. In particular, as a complement of our previous work on read-after-write hazards, we focus on write-after-write and write-after-read hazards in microprocessors with a single pipeline.

Keywords

microprocessor analysis, pipelined execution, WAW hazard, WAR hazard, formal verification, parameterized systems

Authors

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

RIV year

2015

Released

17. 12. 2015

Publisher

Springer International Publishing

Location

Zurich

ISBN

978-3-319-27340-2

Book

Computer Aided Systems Theory - EUROCAST 2015

Edition

Lecture Notes in Computer Science

ISBN

0302-9743

Periodical

Lecture Notes in Computer Science

Year of study

9520

Number

1

State

Federal Republic of Germany

Pages from

605

Pages to

614

Pages count

10

URL

http://link.springer.com/content/pdf/10.1007%2F978-3-319-27340-2_75.pdf

BibTex

@inproceedings{BUT120023,
  author="Lukáš {Charvát} and Aleš {Smrčka} and Tomáš {Vojnar}",
  title="Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems",
  booktitle="Computer Aided Systems Theory - EUROCAST 2015",
  year="2015",
  series="Lecture Notes in Computer Science",
  journal="Lecture Notes in Computer Science",
  volume="9520",
  number="1",
  pages="605--614",
  publisher="Springer International Publishing",
  address="Zurich",
  doi="10.1007/978-3-319-27340-2\{_}75",
  isbn="978-3-319-27340-2",
  issn="0302-9743",
  url="http://link.springer.com/content/pdf/10.1007%2F978-3-319-27340-2_75.pdf"
}