Publication Details
Utilizing parametric systems for detection of pipeline hazards
Microprocessor, Data hazard, Control hazard, Formal methods, Parametric systems
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.
@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"
}