Equivalence checking between SLM and TLM using coverage directed simulation

The increasing complexity of digital systems makes designers begin to design using abstract system level modeling （SLM）. However, SLM brings new challenges for verification engineers to guarantee the functional equivalence between SLM specifications and lower-level implementa- tions such as those of transaction level modeling （TLM）. This paper proposes a novel method for equivalence checking be- tween SLM and TLM based on coverage directed simulation. Our method randomly simulates an SLM model and uses an satisfiability modulo theories （SMT） solver to generate stimuli for the uncovered area with the direction of a com- posite coverage metric （code coverage and functional cover- age）. Then we run all the generated stimuli （random stimuli and direct stimuli） on both SLM and TLM designs. At the same time, the selected observation variables are compared to evaluate the equivalence between SLM and TLM. Promising experimental results show that our equivalence checking method is more efficient with lower simulation cost.

Arithmetic Operand Ordering for Equivalence Checking

An information extraction-based technique is proposed for RTL-to-gate equivalence checking. Distances are calculated on directed acyclic graph (AIG). Multiplier and multiplicand are distinguished on multiplications with different coding methods, with which the operand ordering/grouping information could be extracted from a given implementation gate netlist, helping the RTL synthesis engine generate a gate netlist with great similarity. This technique has been implemented in an internal equivalence checking tool, ZDIS. Compared with the simple equivalence checking, the speed is accelerated by at least 40% in its application to a class of arithmetic designs, addition and multiplication trees. The method can be easily incorporated into existing RTL-to-gate equivalence checking frameworks, increasing the robustness of equivalence checking for arithmetic circuits.

The parametric complexity of bisimulation equivalence of normed pushdown automata

Deciding bisimulation equivalence of two normed pushdown automata is one of the most fundamental problems in formal verification.The problem is proven to be ACKER-MANN-complete recently.Both the upper bound and the lower bound results indicate that the number of control states is an important parameter.In this paper,we study the parametric complexity of this problem.We refine previous results in two aspects.First,we prove that the bisimulation equivalence of normed PDA with two states is EXPTIME-hard.Second,we prove that the bisimulation equivalence of normed PDA with d states is in F_(d+3),which improves the best known upper bound F_(d+4) of this problem.