Přístupnostní navigace
E-application
Search Search Close
Publication detail
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
0302-9743
Periodical
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" }