Search

It has long been the practice to create models in C or C+ + for architectural studies, software prototyping and RTL verification in the design of systems-on-chip (SoC). It is often the case that by the end of a design project, multiple C models exist for different uses. Clearly, this leads to wasted effort on the part of model developers, and creates risk of functional divergence across models. In this paper we present some guidelines for system-level modeling and RTL design to allow for efficiently leveraging the system-level model for RTL verification via simulation based techniques, as well as via sequential equivalence checking. The paper presents the challenges of keeping system-level models and RTL synchronized from a functional perspective and presents some techniques for overcoming these challenges.

We introduce the notions of required precision and information content of datapath signals and use them to define functionally safe transformations on data flow graphs. These transformations reduce widths of datapath operators and enhance their mergeability. Using efficient algorithms to compute required precision and information content of signals, we define a new algorithm for partitioning a data flow graph consisting of datapath operators into mergeable clusters. Experimental results indicate that use of our clustering algorithm for operator merging based synthesis of datapath intensive designs, can lead to significant improvement in the delay and area of the implementation.

Finding the set of steady states of a machine has applications in formal verification, sequential synthesis and ATPG. Existing techniques assume the presence of a designated set of initial states which is impractical in a real design environment. The set of steady state of a design is defined by the terminally strongly connected components (tSCCs) of the underlying state transition graph (STG). We show that multiple tSCCs and non-terminal SCCs need to be handled in a real design environment especially for verification. We present a fully implicit algorithm to find the steady states of a machine without any knowledge of initial states. We demonstrate the utility of our algorithm by applying it to FSM equivalence checking.

The use of multiphase clocking scheme, aggressive pipelining and "sparse" encodings in high performance designs results in a tremendous increase in the state space. We show that automatically transforming such designs to ones that have more "dense" encodings can result in significant benefits in using implicit BDD based techniques for their verification. We formulate a relaxed retiming framework which is more powerful than traditional retiming in reducing the number of latches and show that it can be applied to the product machine model for checking sequential hardware equivalence (SHE) without altering the correctness of the SHE check. We combine retiming with phase abstraction (C. Pixley, 1992) (a technique to transform multi phase FSMs to single phase FSMs for equivalence checking). The two transformations enable the SHE check to be performed on high performance controllers with large state space (more than 100 latches) from an industrial setting.