Formal Semantics of Hardware Compilation Framework

From bibtex.

Abstract

Static worst-case timing analyses are used to ensure the timing deadlines required for safety-critical systems. In order to derive accurate bounds, these timing analyses require precise (micro-)architecture considerations. Usually, such micro-architecture models are constructed by hand from processor manuals.However, with the open-source hardware initiatives and high-level Hardware Description Languages (HCLs), the automatic generation of these micro-architecture models and, more specifically, the pipeline models are promoted. We propose a workflow that aims to automatically construct pipeline datapath models from processor designs described in HCLs. Our workflow is based on the Chisel/FIRRTL Hardware Compiler Framework. We build at the intermediate representation level the datapath pipeline models. Our work intends to prove the timing properties, such as the timing predictability-related properties. We rely on the formal verification as our method. The generated models are then translated into formal models and integrated into an existing model checking-based procedure for detecting timing anomalies. We use TLA+ modeling and verification language and experiment with our analysis with several open-source RISC-V processors. Finally, we advance the studies by evaluating the impact of automatic generation through a series of synthetic benchmarks.