|
Published Articles >> Table of Contents >> Abstract
Design, Automation and Test in Europe Conference and Exhibition Volume I (DATE'04)
p. 10036
Enhanced Diameter Bounding via Structural
Jason Baumgartner, IBM Server Group
Andreas Kuehlmann, Cadence Berkeley Labs
Full Article Text:
  
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/DATE.2004.1268824
Send link to a friend
| Abstract |
|
Bounded model checking (BMC) has gained widespread industrial use due to its relative scalability. Its exhaustiveness over all valid input vectors allows it to expose arbitrarily complex design flaws. However, BMC is limited to analyzing only a specific time window, hence will only expose those flaws which manifest within that window and thus cannot readily prove correctness. The diameter of a design has thus become an important concept — a bounded check of depth equal to the diameter constitutes a complete proof. While the diameter of a design may be exponential in the number of its state elements, in practice it often ranges from tens to a few hundred regardless of design size. Therefore, a powerful diameter over-approximation technique may enable automatic proofs that otherwise would be infeasible. Unfortunately, exact diameter calculation requires exponential resources, and over-approximation techniques may yield exponentially loose bounds. In this paper, we provide a general approach for enabling the use of structural transformations, such as redundancy removal, retiming, and target enlargement, to tighten the bounds obtained by arbitrary diameter approximation techniques. Numerous experiments demonstrate that this approach may significantly increase the set of designs for which practically useful diameter bounds may be obtained.
|
 Additional Information
|
Citation:
Jason Baumgartner, Andreas Kuehlmann,
"Enhanced Diameter Bounding via Structural,"
date,
p. 10036,
Design, Automation and Test in Europe Conference and Exhibition Volume I (DATE'04),
2004
|
|
