Microelectronics Engineering Group

Microelectronics Engineering Group

Electronics Technology, Systems and Automation Engineering Department University of Cantabria
Home    Staff    Research    Teaching    Doctorate    Publications    Tools    versión en español Sun 17-Feb-19 . 11:42



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.
© Copyright GIM (TEISA-UC)    ¤    All rights reserved.    ¤    Legal TermsE-Mail Webmaster