Utilizing parametric systems for detection of pipeline hazards
| Autor: | Lukáš Charvát, Aleš Smrčka, Tomáš Vojnar |
|---|---|
| Rok vydání: | 2020 |
| Předmět: |
Computer science
business.industry Pipeline (computing) 020207 software engineering 02 engineering and technology Static analysis Parametric system Embedded system Theory of computation 0202 electrical engineering electronic engineering information engineering business Formal verification Software Information Systems |
| Zdroj: | International Journal on Software Tools for Technology Transfer. 24:1-28 |
| ISSN: | 1433-2787 1433-2779 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full text from SpringerLink