Web Map
Location
News
Santander Info
|
| GIM>Research>Publication |
| PUBLICATION |
| |
| Full record |
| Title: | Assertion Checking of Control Dominated Systems with Nonlinear Solvers |
| Type: | International Conference |
| Where: | IEEE International Conference on Formal Methods and Models for Co-Design |
| Date: | 2006-07 |
| Authors: |
Iñigo Ugarte
Pablo Pedro Sánchez
|
| R&D Lines: |
|
| Projects: |
|
| ISBN: | 1-4244-0421-5 |
| PDF File: |
|
| Abstract: | Assertion-based verification (ABV) is a promising methodology to confront the growing problem of system design verification. 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. Some techniques allow the transformation of the behavioral level system description into a set of polynomial inequalities that efficiently model control dominated designs. Other techniques allow integer solutions of the polynomial inequality set to be found from the real solutions that the solver provides.
These techniques have been verified with several control dominated modules of an mpeg decoder. |
|
|
