Current approaches to compute and exploit the flexibility of a component in an FSM network are all at the symbolic level. Conventionally, exploitation of this flexibility relies on state minimizers for incompletely specified FSMs (ISFSMs) or pseudo non-deterministic FSMs (PNDFSM's). However, state-of-the art state minimizers cannot handle large ISFSMs or PNDFSMs. In addition, these exploitation techniques are at the symbolic level, not directly at the net-list logic level. We present a general approach to exploit exact or approximate flexibility directly at the net-list logic level, and we demonstrate that many sequential logic optimization techniques can be applied in exploitation. Moreover, we propose a new procedure for input don't care sequences. As a result, both computation and exploitation of input don't care sequences in larger FSM networks can be made efficient and effective. Finally, we give preliminary results on some artificially constructed FSM networks. Preliminary results indicate that our approach can be effective in reducing the size of a component of an FSM network.

Article Free Access Share on HSIS: a BDD-based environment for formal verification Authors: A. Aziz Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , F. Balarin Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , S.-T. Cheng Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , R. Hojati Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , T. Kam Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , S. C. Krishnan Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , R. K. Ranjan Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , T. R. Shiple Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , V. Singhal Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , S. Tasiran Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , H.-Y. Wang Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , R. K. Brayton Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile , A. L. Sangiovanni-Vincentelli Department of EECS, University of California at Berkeley, Berkeley, CA Department of EECS, University of California at Berkeley, Berkeley, CAView Profile Authors Info & Claims DAC '94: Proceedings of the 31st annual Design Automation ConferenceJune 1994 Pages 454–459https://doi.org/10.1145/196244.196467Published:06 June 1994Publication History 39citation325DownloadsMetricsTotal Citations39Total Downloads325Last 12 Months36Last 6 weeks17 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 SiteeReaderPDF

Previous attempts to capture the phenomenon of output don't care sequences for a component in an FSM network have been incomplete.We demonstrate that output don't care sequences for a component can be expressed using a set of observability relations given that its state transition function is kept unchanged.Each observability relation is permissible in the sense that any implementation compatible with one of them is feasible.The representation for a set of permissible observability relations is not unique.We provide a method to find a set with the minimum number of permissible relations.We briefly discuss the exploitation of permissible observability relations in state minimization, circuit implementation and signal encoding.We have implemented these methods and present some preliminary results on a few small artificially constructed examples.

We present an approach to compute all input don't care sequences for a component in an FSM network with an arbitrary topology. In a cascade FSM network, Kim and Newborn's (K-N) procedure exactly computes all input don't care sequences for the driven machine. However, for a component in a general FSM network the problem of computing and exploiting input don't care sequences is unsolved. We demonstrate that this problem can be reduced to one for a cascade circuit. This reduction uses the notion of an abstract driving machine. In some cases, the exact computation and exploitation of these sequences may be too expensive. We propose methods to compute subsets of input don't care sequences. We discuss the implementation of these algorithms using implicit methods. We also present approximate methods for managing the complexity of large FSM networks. Finally, we give some preliminary results on small networks.