Detail výsledku
Utilizing parametric systems for detection of pipeline hazards
Smrčka Aleš, Ing., Ph.D., UITS (FIT)
Vojnar Tomáš, prof. Ing., Ph.D., UITS (FIT)
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.
Microprocessor, Data hazard, Control hazard, Formal methods, Parametric systems
@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"
}