Verification of Basic Block Schedules Using RTL Transformations

  • Rajesh Radhakrishnan
  • Elena Teica
  • Ranga Vemuri
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2144)


We present an approach to aid in debugging/development of scheduling algorithm implementations. Our technique makes use of a sequence of a correctness-preserving RTL transformation called Register Transfer Split (RTS), to collectively perform the same task as that of a scheduler. Violation of the transformation precondition signals an error and the sequence of RTS transformations applied so far forms a trace which can be used for debugging purposes.


Schedule Algorithm Discrete Cosine Transform Data Path Register Transfer High Level Synthesis 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. [1]
    T. Lock, M. Mendler, and M. Mutz. Combined Formal Post-and Presynthesis Verification in High Level Synthesis. In Formal Methods in Computer-Aided Design, pages 222–236, 1998.Google Scholar
  2. [2]
    P. Ashar, A. Raghunathan, A. Gupta, and S. Bhattacharya. Verification of scheduling in the presence of loops using uninterpreted symbolic simulation. In International Conference on Computer Design (ICCD), 1999.Google Scholar
  3. [3]
    H. Eveking, H. Hinrichsen, and G. Ritter. Automatic Verification of Scheduling Results in High Level Synthesis. In Design, Automation and Test in Europe (DATE), 1999.Google Scholar
  4. [4]
    N. Narasimhan, E. Teica, R. Radhakrishnan, S. Govindarajan, and R. Vemuri. Theorem Proving Guided Development of Formal Assertions in a Resource-Constrained Scheduler for High Level Synthesis. In Andreas Kuehlmann, editor, International Conference on Computer Design (ICCD), Austin, TX, October 1998. IEEE Computer Society.Google Scholar
  5. [5]
    R. Walker and S. Chaudhuri. Introduction to the scheduling problem. IEEE Design and Test, 12(2):60–69, 1995.CrossRefGoogle Scholar
  6. [6]
    E. Teica and R. Vemuri. A Mechanical Proof of Completeness for a Set of Register-level transformations. Technical Report 257/05/01/ECECS, University of Cincinnati, 2001.Google Scholar
  7. [7]
    J. Roy, N. Kumar, R. Dutta, and R. Vemuri. DSS: A Distributed High Level Synthesis System. In IEEE Design and Test of Computers, volume 9, pages 18–32, 1992.CrossRefGoogle Scholar
  8. [8]
    M. Wolfe. High Performance Compilers for Parallel Computing. Addison-Wesley Publishers, 1996.Google Scholar
  9. [9]
    N. Dutt. High Level Synthesis Workshop Benchmarks’92.Google Scholar
  10. [10]
    G. De Micheli. Synthesis and Optimization of Digital Circuits. McGraw-Hill, 1994.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Rajesh Radhakrishnan
    • 1
  • Elena Teica
    • 1
  • Ranga Vemuri
    • 1
  1. 1.ECECS DepartmentUniversity of CincinnatiCincinnati

Personalised recommendations