Using Formal Verification of Parameterized Systems in RAW Hazard Analysis in Microprocessors

Implementation of a pipeline-based execution of instructions in purpose-specific microprocessors is an error prone task, which implies a need of proper verification of the resulting design. Various techniques were proposed for this purpose, but they usually require a significant manual intervention of the developers. In this work, we propose a novel, highly automated approach for discovering RAW hazards in in-order pipelined instruction execution. Our approach combines static analysis of data paths to detect anomalies and possible hazards, followed by a transformation of detected problematic paths to a parameterised system (PS), and a subsequent formal verification to check the possibility of unhandled hazards using techniques for formal verification of PSs. We have implemented our approach and successfully applied it on multiple non-trivial microprocessors.