Microprocessor Hazard Analysis Via Formal Verification of Parameterized Systems

Type

conference paper

Language

English

Authors

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

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

URL

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

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

Conference

Fifteenth International Conference on Computer Aided Systems Theory

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

Projects

Automatic Formal Analysis and Verification of Programs with Complex Unbounded Data and Control Structures, GACR, Standardní projekty, GA14-11384S, start: 2014-01-01, end: 2016-12-31, completed
Centrum excelence IT4Innovations, MŠMT, Operační program Výzkum a vývoj pro inovace, ED1.1.00/02.0070, start: 2011-01-01, end: 2015-12-31, completed
Spolehlivost a bezpečnost v IT, BUT, Vnitřní projekty VUT, FIT-S-14-2486, start: 2014-01-01, end: 2016-12-31, completed

Research groups

Automated Analysis and Verification Research Group - VeriFIT (RG VERIFIT)

Departments

Department of Intelligent Systems (DITS)