Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems

Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F15%3APU117129" target="_blank" >RIV/00216305:26230/15:PU117129 - isvavai.cz</a>
Result on the web
<a href="http://link.springer.com/content/pdf/10.1007%2F978-3-319-27340-2_75.pdf" target="_blank" >http://link.springer.com/content/pdf/10.1007%2F978-3-319-27340-2_75.pdf</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/978-3-319-27340-2_75" target="_blank" >10.1007/978-3-319-27340-2_75</a>

Result language
angličtina
Original language name
Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems
Original language description
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.
Czech name
—
Czech description
—

Project
Result was created during the realization of more than one project. More information in the Projects tab.
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Publication year
2015
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Similar results(10)