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. Varioustransformations 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 transformationsperformed 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 workis 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 aviable automated equivalence checking technique for such examples, we improve on the state of the art.
展开▼
