Detail publikace

Utilizing parametric systems for detection of pipeline hazards

CHARVÁT, L. SMRČKA, A. VOJNAR, T.

Originální název

Utilizing parametric systems for detection of pipeline hazards

Typ

článek v časopise ve Web of Science, Jimp

Jazyk

angličtina

Originální abstrakt

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.

Klíčová slova

Microprocessor, Data hazard, Control hazard, Formal methods, Parametric systems

Autoři

CHARVÁT, L.; SMRČKA, A.; VOJNAR, T.

Vydáno

1. 2. 2022

ISSN

1433-2779

Periodikum

International Journal on Software Tools for Technology Transfer

Ročník

2020

Číslo

1

Stát

Spolková republika Německo

Strany od

1

Strany do

28

Strany počet

28

URL

https://link.springer.com/content/pdf/10.1007/s10009-020-00591-y.pdf

BibTex

@article{BUT168177,
  author="Lukáš {Charvát} and Aleš {Smrčka} and Tomáš {Vojnar}",
  title="Utilizing parametric systems for detection of pipeline hazards",
  journal="International Journal on Software Tools for Technology Transfer",
  year="2022",
  volume="2020",
  number="1",
  pages="1--28",
  doi="10.1007/s10009-020-00591-y",
  issn="1433-2779",
  url="https://link.springer.com/content/pdf/10.1007/s10009-020-00591-y.pdf"
}