Advertisement

On Ensuring Correctness of Cold Scheduler

  • Aparna BarikEmail author
  • Nabamita Deb
  • Santosh Biswas
Conference paper
Part of the Advances in Intelligent Systems and Computing book series (AISC, volume 767)

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.

Keywords

Cold scheduling Verification Equivalence checking FSMD 

References

  1. 1.
    Graphviz - graph visualization software. https://graphviz.gitlab.io/
  2. 2.
    D. Gajski, L. Ramachandran, Introduction to high-level synthesis. IEEE Trans. Des. Test Comput. pp. 44–54 (1994)CrossRefGoogle Scholar
  3. 3.
    D. Grune, K.V. Reeuwijk, H.E. Bal, C.J. Jacobs, K. Langendoen, Modern Compiler Design (Springer, Berlin, 2012)CrossRefGoogle Scholar
  4. 4.
    C.A.R. Hoare, An axiomatic basis for computer programming. Commun. ACM 12, 576–580 (1969).  https://doi.org/10.1145/363235.363259CrossRefzbMATHGoogle Scholar
  5. 5.
    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)CrossRefGoogle Scholar
  6. 6.
    S. Microsystems, Ksparc assembly language - clemson university. https://people.cs.clemson.edu/~mark/sparc/control_structures.txt
  7. 7.
    C.L. Su, A.M. Despain, Cold scheduling. Tech. rep. (1993)Google Scholar
  8. 8.
    J.B. Tristan, X. Leroy, Verified validation of lazy code motion. SIGPLAN Not. 44(6), 316–326 (2009)CrossRefGoogle Scholar
  9. 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

Copyright information

© Springer Nature Singapore Pte Ltd. 2020

Authors and Affiliations

  1. 1.Gauhati UniversityGauhatiIndia
  2. 2.IIT GuwahatiGuwahatiIndia

Personalised recommendations