Utilizing parametric systems for detection of pipeline hazards
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F22%3APU138668" target="_blank" >RIV/00216305:26230/22:PU138668 - isvavai.cz</a>
Result on the web
<a href="https://link.springer.com/content/pdf/10.1007/s10009-020-00591-y.pdf" target="_blank" >https://link.springer.com/content/pdf/10.1007/s10009-020-00591-y.pdf</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/s10009-020-00591-y" target="_blank" >10.1007/s10009-020-00591-y</a>
Alternative languages
Result language
angličtina
Original language name
Utilizing parametric systems for detection of pipeline hazards
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 approach that combines static analysis of data paths, SMT solving, and formal verification of parametric systems in order to discover flaws caused by improperly handled data and control hazards between pairs of instructions. In particular, we concentrate on synchronous, single-pipelined microprocessors with in-order execution of instructions. The paper unifies and better formalizes our previous works on read-after-write, write-after-read, and write-after-write hazards and extends them to be able to handle control hazards in microprocessors with a single pipeline too. The approach has been implemented in a tool called Hades, and we present promising experimental results obtained using the tool on multiple pipelined microprocessors.
Czech name
—
Czech description
—
Classification
Type
J<sub>imp</sub> - Article in a specialist periodical, which is included in the Web of Science database
CEP classification
—
OECD FORD branch
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Result continuities
Project
<a href="/en/project/GA20-07487S" target="_blank" >GA20-07487S: Scalable Techniques for Analysis of Complex Properties of Computer Systems</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)
Others
Publication year
2022
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Name of the periodical
International Journal on Software Tools for Technology Transfer
ISSN
1433-2779
e-ISSN
1433-2787
Volume of the periodical
2020
Issue of the periodical within the volume
1
Country of publishing house
DE - GERMANY
Number of pages
28
Pages from-to
1-28
UT code for WoS article
000574070100001
EID of the result in the Scopus database
2-s2.0-85091726965