Assertion checking of control dominated systems with nonlinear solvers

Nowadays, the verification of systems has grown to dominate the cost of electronic system design, often with limited success, as designs continue to be released with latent bugs. The International Technology Roadmap for Semiconductors (ITRS) affirms in the report of 2005 that for the most complex designs, verification engineers outnumber designers with this ratio reaching two or three to one. Assertion-based verification (ABV) is a promising methodology to confront the growing problem of system design verification (Yeung and Larsen, 2005). Key aspects in increasing the scalability of formal and semi-formal verification techniques are the role of the solver and the level of abstraction of the system description. Several assertion checking techniques based on nonlinear solvers have been proposed to verify assertions in behavioral level system descriptions. These techniques are very efficient with data dominated designs (for example digital filters) but they have a lot of problems with control dominated designs in which the variables have a small set of possible values (typically two, 0 and 1). This paper presents several techniques that allow the use of a commercial nonlinear solver to check assertions in control dominated design. And it studies in depth some techniques that allow the transformation of the behavioral level system description into a set of polynomial inequalities that efficiently model control dominated designs. The goal of the verification methodology is maximizing a nonlinear equation (the assertion equation in this paper) while satisfying a set of non-linear constraints (polynomial inequalities) that model conditional statements and discontinuous functions in this work. The commercial solver LINDO is an example of a global non-linear solver and it has been used in this work. In order to validate the proposed technique, the example \´MPEG system decoder\´ used by (Mitchel et al., 1997) for HW verification is selected. The system decoder is composed o- - f several modules, completely decoupled behaviorally amongst themselves. The verification can be done individually for each module. The property "EF (stop = "1") (LTL nomenclature) has to be verified to guarantee that the composite design will work. The table shows the results. These components are control dominated designs with very few data operations. The second column (non-linear) shows the CPU time of the proposed technique, while the third column presents the time of a commercial integer solver. It can be shown that the proposed technique provides similar results to an integer solver with pure control descriptions