Efficient Approximate Symbolic Reachability of Discrete-timed Digital Circuits

Timed reachability analysis of gate-level circuits is important in several applications. In this paper, we present techniques for efficient approxi- mate symbolic reachability of circuits assuming dis- crete delays of gates. We exploit local interactions among gates to develop a highly scalable algorithm for over-approximating the set of timed reachable states. We present a scheme of successive over- approximations and provide a probabilistic analysis to prove that these approximations converge quickly on an average. We argue that this scheme corresponds to successively extracting trees in the underlying factor graph representing the interaction of gates. We report experimental results on a set of benchmarks that demonstrate the effectiveness of our approach.