Utilizing parametric systems for detection of pipeline hazards

Kód výsledku v 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>

Výsledek na webu

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

Jazyk výsledku

angličtina

Název v původním jazyce

Utilizing parametric systems for detection of pipeline hazards

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Utilizing parametric systems for detection of pipeline hazards

Popis výsledku anglicky

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.

Druh

J_imp - Článek v periodiku v databázi Web of Science

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

<a href="/cs/project/GA20-07487S" target="_blank" >GA20-07487S: Škálovatelné techniky pro analýzu komplexních vlastností počítačových systémů</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2022

Kód důvěrnosti údajů

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

Název periodika

International Journal on Software Tools for Technology Transfer

ISSN

1433-2779

e-ISSN

1433-2787

Svazek periodika

2020

Číslo periodika v rámci svazku

1

Stát vydavatele periodika

DE - Spolková republika Německo

Počet stran výsledku

28

Strana od-do

1-28

Kód UT WoS článku

000574070100001

EID výsledku v databázi Scopus

2-s2.0-85091726965