A concolic approach, called Slec-Cf, to check sequential equivalence between a high-level (e.g., C++/SystemC) hardware description and an RTL (e.g., Verilog) is presented. Slec-Cf searches for counterexamples over the possible values of a set of "control signals" in a depth-first lexicographic manner, avoiding values that are unrealizable by any concrete input. In addition, Slec-Cf respects user-specified design constraints during search, thus only producing stimuli that are of relevance to users. It is a superior alternative to random simulations, which produce an overwhelming number of irrelevant stimuli for user-constrained designs, and are therefore of limited effectiveness. To handle complex designs, we present an incremental version of Slec-Cf, which iteratively increases the search depth, and set of control signals, and uses a cache to reuse prior results. We implemented Slec-Cf on top an existing industrial tool for sequential equivalence checking. Experimental results indicate that Slec-Cf clearly outperforms random simulation in terms of coverage achieved. On complex designs, incremental Slec-Cf demonstrates superior ability to achieve good coverage in almost all cases, compared to non-incremental Slec-Cf.

Methods for word-level model checking based on purely bit-level techniques have difficulties with heavy arithmetic logic. Word-level and SMT approaches often are limited by relying on (incomplete) bounded model checking. UFAR, a hybrid word- and bit-level approach, addresses these issues, taking advantage of modern bit-level sequential techniques while heavy arithmetic logic is addressed by word-level abstraction and the use of uninterpreted function (UF) constraints. The methods and efficiency improvements developed for UFAR enabled it to prove 2422 of a set of 2492 industrial sequential model checking problems within a 1-hour limit, while a bit-level model checker super prove completed only 2115 of these within the same limit.

In numerous EDA flows, time-consuming computations are repeatedly applied to sequential circuits. This motivates developing methods to determine what circuits have been processed already by a tool. This paper proposes an algorithm for semi-canonical labeling of nodes in a sequential AIG, allowing problems or sub-problems solved by an EDA tool to be cached with their computed results. This can speed up the tool when applied to designs with isomorphic components or design suites exhibiting substantial structural similarity.

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.

Parametric representations used for symbolic simulation of circuits usually use BDDs. After a few steps of symbolic simulation, state set representation is converted from one parametric representation to another smaller representation, in a process called reparameterization. For large circuits, the reparametrization step often results in a blowup of BDDs and is expensive due to a large number of quantifications of input variables involved. Efficient SAT solvers have been applied successfully for many verification problems. This paper presents a novel SAT-based reparameterization algorithm that is largely immune to the large number of input variables that need to be quantified. We show experimental results on large industrial circuits and compare our new algorithm to both SAT-based Bounded Model Checking and BDD based symbolic simulation. We were able to achieve on average 3x improvement in time and space over BMC and able to complete many examples that BDD based approach could not even finish.

Computing the set of states reachable in one step from a given set of states, i.e. image computation, is a crucial step in several symbolic verification algorithms, including model checking and reachability analysis. So far, the best methods for quantification scheduling in image computation, with a conjunctively partitioned transition relation, have been restricted to a linear schedule. This results in a loss of flexibility during image computation. We view image computation as a problem of constructing an optimal parse tree for the image set. The optimality of a parse tree is defined by the largest BDD that is encountered during the computation of the tree. We present dynamic and static versions of a new algorithm, VarScore, which exploits the flexibility offered by the parse tree approach to the image computation. We show by extensive experimentation that our techniques outperform the best known techniques so far.