Publication Details

Microprocessor Hazard Analysis Via Formal Verification of Parameterized Systems

CHARVÁT Lukáš, SMRČKA Aleš and VOJNAR Tomáš. Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems. In: Computer Aided Systems Theory - EUROCAST 2015. Lecture Notes in Computer Science, vol. 9520. Zurich: Springer International Publishing, 2015, pp. 605-614. ISBN 978-3-319-27340-2. ISSN 0302-9743. Available from: http://link.springer.com/content/pdf/10.1007%2F978-3-319-27340-2_75.pdf
Type
conference paper
Language
english
Authors
URL
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
Conference
Fifteenth International Conference on Computer Aided Systems Theory , Las Palmas de Gran Canaria, ES
ISBN
978-3-319-27340-2
Publisher
Springer International Publishing
Place
Zurich, CH
DOI
UT WoS
000376687100075
EID Scopus
BibTeX
@INPROCEEDINGS{FITPUB11064,
   author = "Luk\'{a}\v{s} Charv\'{a}t and Ale\v{s} Smr\v{c}ka and Tom\'{a}\v{s} Vojnar",
   title = "Microprocessor Hazard Analysis Via Formal Verification of Parameterized Systems",
   pages = "605--614",
   booktitle = "Computer Aided Systems Theory - EUROCAST 2015",
   series = "Lecture Notes in Computer Science",
   journal = "Lecture Notes in Computer Science",
   volume = 9520,
   number = 1,
   year = 2015,
   location = "Zurich, CH",
   publisher = "Springer International Publishing",
   ISBN = "978-3-319-27340-2",
   ISSN = "0302-9743",
   doi = "10.1007/978-3-319-27340-2\_75",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/11064"
}
Back to top