Verification and Synthesis of Counters based on Symbolic Techniques

Binary Decision Diagrams and Symbolic Techniques have undergone major improvements in the last few years but extending the applicability of the reachability analysis to new fields is still a key issue. A great limitation on standard Symbolic Traversal is represented by Finite State Machines with a very high sequential depth. A typical example of this behaviour are counters. On the other hand systems containing counters, e.g. embedded systems, are of great practical importance in several fields. Among the techniques introduced to better deal with "pure" counters, iterative squaring plays an important role, because it can produce solutions with a logarithmic execution time with respect to the sequential depth. Some drawbacks usually limit the application of such a technique to more general circuits but we successfully tailored iterative squaring to allow its application for symbolic verification and synthesis of circuits containing counters. Experiments on large and complex home--made and industrials circuits containing counters show the feasibility of the approach.