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.
KeywordsCold scheduling Verification Equivalence checking FSMD
- 1.Graphviz - graph visualization software. https://graphviz.gitlab.io/
- 6.S. Microsystems, Ksparc assembly language - clemson university. https://people.cs.clemson.edu/~mark/sparc/control_structures.txt
- 7.C.L. Su, A.M. Despain, Cold scheduling. Tech. rep. (1993)Google Scholar
- 9.T.H. Weng, C.H. Lin, J.J.J. Shann, C.P. Chung, Power reduction by register relabeling for crosstalk-toggling free instruction bus coding, in 2010 International Computer Symposium (ICS2010), pp. 676–681 (2010)Google Scholar