Detail publikace

Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems

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

Originální název

Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems

Typ

článek ve sborníku ve WoS nebo Scopus

Jazyk

angličtina

Originální abstrakt

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.

Klíčová slova

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

Autoři

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

Rok RIV

2015

Vydáno

17. 12. 2015

Nakladatel

Springer International Publishing

Místo

Zurich

ISBN

978-3-319-27340-2

Kniha

Computer Aided Systems Theory - EUROCAST 2015

Edice

Lecture Notes in Computer Science

ISSN

0302-9743

Periodikum

Lecture Notes in Computer Science

Ročník

9520

Číslo

1

Stát

Spolková republika Německo

Strany od

605

Strany do

614

Strany počet

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"
}