Publication detail

Utilizing parametric systems for detection of pipeline hazards

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

Original Title

Utilizing parametric systems for detection of pipeline hazards

Type

journal article in Web of Science

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

Keywords

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

Authors

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

Released

1. 2. 2022

ISBN

1433-2779

Periodical

International Journal on Software Tools for Technology Transfer

Year of study

2020

Number

1

State

Federal Republic of Germany

Pages from

1

Pages to

28

Pages count

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