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 Fri 29-Mar-24 . 10:29



Web Map


Location

News

Santander Info

GIM>Research>Publication
   PUBLICATION
 
   Full record
Title:Assertion Checking of Behavioral Descriptions with Non-linear Solver
Type:International Conference
Where:IEEE International Conference on Computer Design
Date:2005-10
Authors: Iñigo Ugarte
Pablo Pedro Sánchez
R&D Lines:
Projects:
ISBN:0-7695-2451-6
PDF File:
Abstract:Verification has become the mayor bottleneck of the
design process. According to the latest report of the
International Technology Roadmap for
Semiconductors, the challenge will be to develop new
design-for-verifiability techniques and verification
methods for higher levels of abstraction. Several
Design-for-Verifiability methodologies (DFV) have
been proposed and Assertion-based Verification (ABV)
is one of the most promising. In order to automatically
verify assertions at the higher abstraction levels, it is
necessary to improve the performances and
capabilities of current constraint solvers.
This paper presents a new technique based on nonlinear
solvers that automatically checks assertions in
behavioral descriptions of hardware systems. These
descriptions are modeled with a set of integer
polynomial inequalities. The technique provides better
results than SAT solvers and it is applied to real
designs, such as Viterbi decoders or vocoder digital
filters.
© Copyright GIM (TEISA-UC)    ¤    All rights reserved.    ¤    Legal TermsE-Mail Webmaster