Verification of properties (tasks) on a system P containing data paths may require too many resources (memory space and/or computation time) because such systems have very large and deep state spaces. As pointed out by Kurshan, what is needed is a reduced system P' which behaves exactly as P with respect to the properties that must be proved, but more compact than P, so that the verification can be easily performed. The process of finding P' from P is called reduction. P is specified by a network of interacting finite-state machines for data paths and controllers, and tasks are specified by finite-state automate. The verification of a task T on P is performed by the language containment check L(P)/spl sube/L(T), where L(P) is the language generated by P and L(T) is the language accepted by T. It has been shown that, under appropriate conditions, the system P can be reduced to P' and the task T to T' such that L(P')/spl sube/L(T')/spl hArr/L(P)/spl sube/L(T). The direct language containment check L(P)/spl sube/L(T) is no longer needed; it is replaced by L(P')/spl sube/L(T'), which is less expensive. More specifically, for the purpose of simplifying the verification of some properties, the system implementation is abstracted locally with respect to the behavior under observation (i.e., bottom-up reduction), in the context of an integrated top-down design/verification technique. The tasks that one may want to verify can express both safety and fairness constraints. In this paper, we prove that the reduction of some data paths to four-state, nondeterministic finite-state machines, and the redundancy removal performed on the controllers is a homomorphic transformation, so that the simplified language containment check can automatically be applied without testing the validity of the homomorphism. This homomorphism correctness verification, required when a formal proof is not available, can be executed using a tool like Cospan, but it may not be completed when the state space to be traversed is too large and deep. The redundancy removal performed on the controllers is important because it eliminates the spurious behaviors introduced in the system by the nondeterminism of the reduced data paths. Redundancy, in fact, may induce a failure in the verification of L(P')/spl sube/L(T'), while L(P)/spl sube/L(T) actually holds. In order to show the effectiveness of the proposed methodology, we verify properties on an extended version of the Mead-Conway Traffic Light Controller, on a modified IRQ communication protocol, and on a relatively prime integers checker and generator.

This paper presents algorithms for approximate finite state machine traversal based on state space decomposition. The original finite state machine is partitioned in component submachines, and each of them is traversed separately; the result of the computation is an over-estimation of the set of reachable states of the original machine. Different traversal strategies, which reduce the effects of the degrees of freedom introduced by the decomposition, are discussed. Efficient partitioning is a key point for the performance of the traversal techniques; a method to heuristically find a good decomposition of the overall finite state machine, based on the exploration of its state variable dependency graph, is proposed. Applications of the approximate traversal methods to logic optimization of sequential circuits and behavioral verification of finite state machines are described; experimental results for such applications, together with data concerning pure traversal, are reported.

Article Algorithms for approximate FSM traversal Share on Authors: Hyunwoo Cho View Profile , Gary D. Hachtel View Profile , Enrico Macii View Profile , Bernard Plessier View Profile , Fabio Somenzi View Profile Authors Info & Claims DAC '93: Proceedings of the 30th international Design Automation ConferenceJuly 1993 Pages 25–30https://doi.org/10.1145/157485.164555Online:01 July 1993Publication History 72citation370DownloadsMetricsTotal Citations72Total Downloads370Last 12 Months3Last 6 weeks0 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteGet Access

It is pointed out that systems containing counters have very large and deep state spaces, and the verification of properties on these systems can be very expensive in terms of memory space and computation time. A technique for automatically reducing the state space associated with the system on which some properties that can express both safeness and fairness constraints have to be proved is presented. In particular, a set of conditions upon which some counters can be reduced to three-state, nondeterministic machines is given. The controllers can be simplified by removing the redundancy induced by their interaction with the counter, so that the verification tasks can be more easily performed.>

The authors present an extension to binary decision diagrams (BDDs) that exploits the information contained in the structure of the circuit to produce a compact, semicanonical representation. The extended BDDs (XBDDs) retain many of the advantages of BDDs while at the same time allowing one to deal with larger circuits. Using XBDDs, it is possible to verify circuits for which the BDDs could not be built in the same amount of space. Results of the application of XBDDs to combinational multipliers are presented.>

The authors consider the problem of variable ordering in algorithms for verification of finite state machines (FSMs) for which the traversal is based on BDD (binary decision diagram) representation and image computation via implicit enumeration. They treat two separate BDD ordering problems: (1) minimization of the representation of the next state function and the representation of the set of reachable states, and (2) a selection heuristic to reduce the complexity of the image computation problem by dynamic selection of the implicit enumeration splitting variables. In both problems they present theoretical results based on the algebraic structure of the next state functions, heuristic ordering methods, and favorable experimental results for problems with significant algebraic structure.>

Algorithms are presented for finite state machine (FSM) verification and image computation which improve on the results of O. Coudert et al (1989), giving 1-4 orders of magnitude speedup. Novel features include primary input splitting-this PODEM feature enlarges the search space but shortens the search due to implications. Another new feature, identical subtree recombination, is shown to be effective for iterative networks (eg, serial multipliers). The free-variable recognition feature prevents unbalanced bipartitioning trees in tautological subspaces. Finally, reached set pruning is significant when the image contains large numbers of previously reached states.>