Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems

Czech title

Analýza hazardů v mikroprocesorech pomocí formální analýzy parametrizovaných systémů

Type

conference paper

Language

English

Authors

Charvát Lukáš, Ing., Ph.D.
Smrčka Aleš, Ing., Ph.D. (DITS)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS)

URL

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

Keywords

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

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.

Annotation

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.

Published

2015

Pages

605–614

Journal

Lecture Notes in Computer Science, vol. 9520, no. 1, ISSN 0302-9743

Proceedings

Computer Aided Systems Theory - EUROCAST 2015

Series

Lecture Notes in Computer Science

ISBN

978-3-319-27340-2

Publisher

Springer International Publishing

Place

Zurich

DOI

10.1007/978-3-319-27340-2_75

UT WoS

000376687100075

EID Scopus

2-s2.0-84952306064

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