Verification of scheduling in the presence of loops using uninterpreted symbolic simulation

Pranav Ashar, Anand Raghunathan, Aarti Gupta, Subhrajit Bhattacharya

Research output: Contribution to conferencePaperpeer-review

4 Scopus citations


We propose a novel procedure based on uninterpreted symbolic simulation for checking the scheduling step in high-level synthesis. The primary task in scheduling is the assignment of time steps or, equivalently, states to operations. Various transformations like operation reordering and loop unrolling may be performed in the process to meet the optimization criteria. The contribution of our proposal lies in its ability to efficiently handle loops and a wide range of loop transformations performed during scheduling. Our algorithm is based on loop invariant extraction using a combination of uninterpreted symbolic simulation and induction techniques. In spite of its wide scope, our procedure is relatively complete and practical. This work is a part of our effort to provide a suite of techniques for verifying the various steps involved in the high-level synthesis process. It is being implemented in an in-house verification system for checking equivalence of designs generated from high-level specifications through successive refinements. We present case studies to demonstrate the applicability of our approach. These case studies consist of examples where equivalence cannot be established using conventional FSM-based methods. By providing a viable automated equivalence checking technique for such examples, we improve on the state of the art.

Original languageEnglish (US)
Number of pages9
StatePublished - 1999
Externally publishedYes
EventInternational Conference on Computer Design (ICCD'99) - Austin, TX, USA
Duration: Oct 10 1999Oct 13 1999


ConferenceInternational Conference on Computer Design (ICCD'99)
CityAustin, TX, USA

All Science Journal Classification (ASJC) codes

  • Hardware and Architecture
  • Electrical and Electronic Engineering


Dive into the research topics of 'Verification of scheduling in the presence of loops using uninterpreted symbolic simulation'. Together they form a unique fingerprint.

Cite this