On Ensuring Correctness of Cold Scheduler

摘要

Cold scheduling is one widely used transformation technique that reorders the instruction sequence in such a way bit switching between two successive instructions will be minimum and thus reduces power consumption. To make the system reliable, ensuring correctness of cold scheduling is important. In this paper, a method for verification of cold scheduler is presented. Our method first extracts finite state machines with data paths (FSMDs) from the input and the output of a cold scheduler and then applies an FSMD-based equivalence checking method to ensure the correctness of the cold scheduler. We have implemented our method and tested on some examples. The results show the effectiveness of our method.