Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Graphviz - graph visualization software. https://graphviz.gitlab.io/
D. Gajski, L. Ramachandran, Introduction to high-level synthesis. IEEE Trans. Des. Test Comput. pp. 44–54 (1994)
D. Grune, K.V. Reeuwijk, H.E. Bal, C.J. Jacobs, K. Langendoen, Modern Compiler Design (Springer, Berlin, 2012)
C.A.R. Hoare, An axiomatic basis for computer programming. Commun. ACM 12, 576–580 (1969). https://doi.org/10.1145/363235.363259
C. Karfa, D. Sarkar, C. Mandal, P. Kumar, An equivalence-checking method for scheduling verification in high-level synthesis. IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst. 27(3), 556–569 (2008)
S. Microsystems, Ksparc assembly language - clemson university. https://people.cs.clemson.edu/~mark/sparc/control_structures.txt
C.L. Su, A.M. Despain, Cold scheduling. Tech. rep. (1993)
J.B. Tristan, X. Leroy, Verified validation of lazy code motion. SIGPLAN Not. 44(6), 316–326 (2009)
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)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2020 Springer Nature Singapore Pte Ltd.
About this paper
Cite this paper
Barik, A., Deb, N., Biswas, S. (2020). On Ensuring Correctness of Cold Scheduler. In: Elçi, A., Sa, P., Modi, C., Olague, G., Sahoo, M., Bakshi, S. (eds) Smart Computing Paradigms: New Progresses and Challenges. Advances in Intelligent Systems and Computing, vol 767. Springer, Singapore. https://doi.org/10.1007/978-981-13-9680-9_15
Download citation
DOI: https://doi.org/10.1007/978-981-13-9680-9_15
Published:
Publisher Name: Springer, Singapore
Print ISBN: 978-981-13-9679-3
Online ISBN: 978-981-13-9680-9
eBook Packages: Intelligent Technologies and RoboticsIntelligent Technologies and Robotics (R0)