Utilizing parametric systems for detection of pipeline hazards

Utilizing parametric systems for detection of pipeline hazards

Článek WoS

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.

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

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

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

2024

01.02.2022

International Journal on Software Tools for Technology Transfer

1433-2779

International Journal on Software Tools for Technology Transfer

2020

1

Spolková republika Německo

1

28

28

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