Formal analysis of synchronous circuits
Thomas R. Shiple, Alberto L. Sangiovanni-Vincentelli · 1996
This dissertation addresses three separate, but related problems concerning the formal analysis of synchronous circuits and their associated finite state machines. The first problem is the logical analysis of synchronous circuits containing combinational cycles. The presence of such cycles can cause unstable behavior at the outputs of a circuit, but this is not necessarily always the case. This work determines when cycles are harmless, and when they are not. In particular, three classes of circuits are defined that tradeoff time to decide the class, with the permissiveness of the class. For each class, the complexity of the corresponding decision problem is proven and a procedure to decide the class is given. In addition, if a circuit is determined to be within a given class, then a new circuit can be generated with the same input/output behavior, but without combinational cycles. This is an important utility, as many CAD tools do not accept circuits with combinational cycles. The second problem that is addressed is the CTL model checking of interacting FSMs. A state equivalence is presented that is defined with respect to a given CTL formula. Since it does not attempt to preserve all CTL formulas, like bisimulation does, we can expect to compute coarser equivalences. This equivalence is used to manage the size of the transition relations encountered when model checking a system of interacting FSMs. Specifically, the equivalence is used to reduce the size of each component FSM, so that their product will be smaller. We show how to apply the method, whether an explicit representation is used for the FSMs, or BDDs are used. Also, we show that in some cases this approach can detect if a formula passes or fails, without composing all the component machines. The method is exact and completely automatic, and handles full CTL. These two problems are PSPACE-hard (in the number of flip-flops) to decide; approximate methods may be useful to find a solution in affordable CPU time. To demonstrate the use of approximate methods in logical analysis, we address the the state reachability problem in FSMs, which is the problem of determining if one set of states can reach another. State reachability has broad applications in formal verification, synthesis, and testing of synchronous circuits. This work attacks this problem by making a series of under- and over-approximations to the state transition graph, using the over-approximations to guide the search in the under-approximations for a potential path from one state set to the other. Central to this method is an algorithm to approximate a Boolean function by another function having a smaller BDD.