Utilizing parametric systems for detection of pipeline hazards
- PDF / 1,606,449 Bytes
- 28 Pages / 595.276 x 790.866 pts Page_size
- 53 Downloads / 175 Views
GENERAL Regular Paper
Utilizing parametric systems for detection of pipeline hazards Lukáš Charvát1 · Aleš Smrˇcka1 · Tomáš Vojnar1 Accepted: 14 September 2020 © Springer-Verlag GmbH Germany, part of Springer Nature 2020
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
1 Introduction As the complexity of hardware designs is growing over the last decades and microprocessor development cycles are facing pressure on fast and low design costs, automation of hardware development has become a crucial need. This trend was further boosted by the recent rise of the so-called Internet of Things (IoT) interconnecting embedded devices, which often require specialized, power-efficient designs to be used. To facilitate the automation, specialized processor description languages [14,25] are used increasingly during the design process. Various tool chains, such as Synopsys ASIP Designer [26], Cadence Tensilica SDK [8], or Codasip Studio [15], can then take advantage of the availability of such microprocessor descriptions and provide automatic generation of HDL designs, simulators, assemblers, disassemblers, and compilers.
B
Lukáš Charvát [email protected] Aleš Smrˇcka [email protected] Tomáš Vojnar [email protected]
1
Faculty of Information Technology, Brno University of Technology, Božetˇechova 2, 612 66 Brno, Czech Republic
Nowadays, microprocessor design tool chains typically allow designers to verify designs by simulation and/or functional verification. Simulation is commonly used to obtain some initial understanding about the design (e.g. to check whether an instruction set contains sufficient instructions). Functional verification usually compares results of large numbers of computations performed by the newly designed microprocessor against a golden specification, which must be provided manually by the developers. However, even extensive functional verification can miss some non-trivial bugs. Therefore, usage of formal verification becomes more and more desirable in the recent years. As o
Data Loading...
