Grupo de Ingeniería Microelectrónica

Grupo de Ingeniería Microelectrónica

Departamento de Tecnología Electrónica, Ingeniería de Sistemas y Automática Universidad de Cantabria
Home   Personas   Investigación   Docencia   Doctorado   Publicaciones   Herramientas   Bolsa de Empleo   english version Sun 20-Sep-20 . 19:35

Mapa Web



Info Santander

Gestión BD

   Ficha completa
Título:Assertion Checking of Control Dominated Systems with Nonlinear Solvers
Tipo:Publicacion en Proceedings o Actas internacionales
Lugar:IEEE International Conference on Formal Methods and Models for Co-Design
Autores: Iñigo Ugarte
Pablo Pedro Sánchez
Resumen: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.
© Copyright GIM (TEISA-UC)    ¤    Todos los derechos Reservados.    ¤    Términos LegalesE-Mail Webmaster