Alexander Fedotov: Automatic Generation of Hardware Checkers from Formal Micro-architectural Specifications

Event Details

To manage design complexity, high-level models are used to evaluate the functionality and performance of design solutions. There is a significant gap between these high-level models and the Register Transfer Level (RTL) implementations actually produced by designers. We address the challenge of bridging this gap, namely, relating abstract specifications to RTL implementations. An important feature of our proposed approach is to support non-deterministic specifications. From such a non-deterministic model, we automatically compute a representation of its observable behaviour. We then turn this representation into a System Verilog checker. The checker is connected to the input and output interfaces of the RTL implementation. The resulting combination is given to a commercial EDA tool to prove that the specification simulates the implementation. Our method is implemented for the formal micro-architectural description language (MaDL) ¨C an extension of the xMAS formalism originally proposed by Intel ¨C and exemplified on several examples.