Enhanced Diameter Bounding via Structural

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 overapproximation technique may enable automatic proofs that otherwise would be infeasible. Unfortunately, exact diameter calculation requires exponential resources, and overapproximation techniques may yield exponentially loose bounds. In this paper, we provide a general appro...

• Type: Conference
• Year: 2004
• Where: DATE
• Authors: Jason Baumgartner, Andreas Kuehlmann
• Keywords: DATE 2004, Exact Diameter Calculation, Hardware, Powerful Diameter Overapproximation, Useful Diameter Bounds