We present a novel technique for Sequential Equivalence Checking (SEC) between non-cycle-accurate designs. The problem is routinely encountered in verifying the correctness of a system-level model versus an RTL design which has been derived from the former either manually or through high-level synthesis. The existing state-of-the-art in formal verification/SEC does not provide an efficient mechanism to perform such an equivalence check. Our technique reduces the SEC problem to a cycle-accurate equivalence-checking problem by constructing a pair of normalized cycle-accurate designs from the original designs, on which standard equivalence-checking techniques can then be deployed. We report the results of deploying our techniques on several industrial examples.

Binary Decision Diagrams (BDDs) often fail to exploit sharing between Boolean functions that differ only in their support variables. In a memory circuit, for example, the functions for the different bits of a word differ only in the data bit while the address decoding part of the function is identical. We present a symbolic representation approach using ordered function templates to exploit such regularity.Templates specify functionality without being bound to a specific set of variables. Functions are obtained by instantiating templates with a list of variables. We ensure canonicity of the representation by requiring that templates are normalized and argument lists are ordered. We also present algorithms for performing Boolean operations using this representation. Experiments with a prototype implementation built on top of CUDD indicate that function templates can dramatically reduce memory requirements for symbolic simulation of regular circuits.

In this paper, we present approaches and algorithms for parallelization of compiled event driven VHDL simulations on shared-memory multiprocessors (SMP). An efficient single-threaded algorithm for simulation of VHDL descriptions is first presented. This algorithm is shown to be competitive with a commercial VHDL simulator. Schemes for multithreaded execution of this algorithm are then described. These have been implemented on top of the POSIX pthreads library and experimental results have been shown on a Sun SparcServer 1000E. Speedups of up to four on eight processors have been achieved for some benchmarks.

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 multi-phase clocking scheme, aggressive pipelining and #sparse" encodings in high performance designs results in a tremendous increase in the state space. In this paper, we show that automatically transforming such designs to ones that have more #dense" encodings can result in signi#cant bene#ts in using implicit BDD-based techniques for their veri#cation. 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 #4# #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. 1 Introduction Due to aggressive t...

Optimization of large sequential circuits has become unmanageable in CAD of VLSI due to time and memory requirements. We report a parallel algorithm for the state assignment problem for finite state machines. Our algorithm has three significant contributions: it is an asynchronous parallel algorithm portable across different MIMD machines; time and memory requirements reduce linearly with the number of processors, enabling the parallel implementation to handle large problem sizes; and the quality of the results for multiprocessor runs remains comparable to the serial algorithm on which it is based due to an implicit backtrack correction mechanism built into the parallel implementation.

Equivalence checking of finite state machines (FSMs) traditionally assumes single phase machines where a single clock (implicit or explicit) synchronizes the state of the FSM. We extend the equivalence checking paradignm to FSMs with multi-phase clocks. Such designs are becoming increasingly popular in high performance microprocessors since they result in lower synchronization overhead. In addition, aggressive pipelining and the use of “sparse” encodings results in designs where the ratio of steady states to the total state space is very low. In this paper, 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 explore two such techniques: phase abstraction and retiming and demonstrate their utility in the context of FSM equivalence checking. The main contributions of our work are: —We show that a multi-phase FSM can be transformed to a functionally equivalent one phase FSM and this phase abstraction leads to significant improvement in the size of FSMs that can be checked for equivalence. —We show that min-latch retiming preserves equivalence and can be performed efficiently in multi-phase designs, even when latch borrowing and discarding is allowed at the primary inputs and outputs. —We demonstrate the utility of our approach on several controller FSMs from the industry.

Formally verifying properties of signals in a circuit hasseveral applications in an equivalence checking based formalverification flow.In a hierarchical design, functionalityis divided across blocks.This necessitates the useof constraints on input signals of a block to avoid falsenegatives.Validating such input constraints requires assertionchecking at the outputs of modules generatingthe constrained signals.In this paper, we present anefficient assertion checker for combinational propertieswhich avoids the BDD explosion problem by finding anoptimal intermediate correlation free frontier.It hasbeen successfully used in an industrial setting to uncovera number of bugs.

In this paper, we propose a unique problem in the assignment of overlapping tasks to processors on a parallel machine, with the twin objectives of minimizing workloads while maintaining good load balance. This problem arises in some applications in VLSI CAD, e.g. parallel compiled VHDL simulation. We assume that the parallel application can be decomposed into a set of tasks, each in turn comprising a finite number of subtasks. Overlapped computations arise as a result of replication of subtasks across tasks in order to reduce the amount of communication performed in fine grained parallel applications. The uniqueness of the problem stems from the fact that overlapping computation on tasks assigned to the same processor is only performed once. Theoretical results on NP-hardness and bounds on the utilization of overlap are provided. A heuristic solution is also proposed. An important application area in VLSI-CAD, parallel compiled event driven VHDL simulation is introduced. Results of the application of our heuristics to this problem are reported on a SUN Sparcserver 1000 multiprocessor.

This paper presents a detailed evaluation of parallel mesaagedriven pmgmms on both message-passing and shared memory pamllel architectures.Four large pomllel appiications from the domain of VLSI computer aided design are evaluated, namely: parallel test pattern genemtion, pamllel cell placement, logic qnthesis, and event dn'ven VHDL kmulalion.The parallelism structure, the communication characterktics, locality chamcterirrtics, gmin sizes of wmputationa, and detailed measurement8 of system time, idle time, and uaer time are meaaunzd for theae applicationa.Resulta are presented for an Intel Pamgon distributed-memory measagepassing multicomputer and compared to a Sun SPARCcenter 1 OOOE symmetric multiprocessor.