In this paper we outline a theory for the environment-modeling problem , the problem of abstracting component finite state machines (FSMs)bordering a particular FSM of interest within a network of interacting FSMs. The goal is to lay a theoretical foundation for the automatic state reduction of large FSM networks. We feel this is a prerequisite for the efficient use of many verification techniques. We focus on computing conditions for the safe removal of a component FSM in a FSM network, where removal is safe if it preserves a certain well-defined trace equivalence. We present an optimized algorithm for determining language universality of a FSM, as well as determining independence of a FSM from those of its inputs connected to outputs of neighboring FSMs. These two properties, input independence and language universality, provide the necessary and sufficient conditions for safe removal. In addition, we show how simulation relations can be utilized, both to reduce the cost of computing safe removal and to create an appropriate abstract FSM when safe removal is not possible.

Hardware systems are generally specified as a set of interacting finite state machines (FSMs). An important problem in formal verification using Binary Decision Diagrams (BDDs) is forming the transition relation of the product machine. This problem reduces to conjuncting (or multiplying) the BDDs representing the transition relations of the individual machines, and then existentially quantifying out the set of input and output variables. The resulting graph is called the product graph. Computing the set of reachable states of the product graph is the central verification problem. In this paper, we discuss two related problems. The early quantification problem is the problem of interleaving multiplication of a set of BDDs with the quantification of a set of variables so that the size of the largest BDD encountered is minimized. We show that an abstraction of this problem is NP-complete, and provide heuristic solutions for it. In some cases, the size of the BDD representing the transition relation of the product graph is too large. The partitioned transition relations problem deals with partially combining the BDD's and quantifying as many variables as possible, so that the time for computing the set of reachable states of the product graph is minimized. We offer heuristic solutions to this problem based on our algorithms for early quantification. The algorithms have been implemented and good experimental results have been achieved.

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

We present heuristic algorithms for finding a minimum BDD size cover of an incompletely specified function, assuming the variable ordering is fixed.In some algorithms based on BDDs, incompletely specified functions arise for which any cover of the function will suffice.Choosing a cover that has a small BDD representation may yield significant performance gains.We present a systematic study of this problem, establishing a unified framework for heuristic algorithms, proving optimality in some cases,and presenting experimental results.

Article A unified approach to language containment and fair CTL model checking Share on Authors: Ramin Hojati View Profile , Thomas R. Shiple View Profile , Robert K. Brayton View Profile , Robert P. Kurshan View Profile Authors Info & Claims DAC '93: Proceedings of the 30th international Design Automation ConferenceJuly 1993 Pages 475–481https://doi.org/10.1145/157485.164985Online:01 July 1993Publication History 7citation260DownloadsMetricsTotal Citations7Total Downloads260Last 12 Months1Last 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

This paper introduces a new and practical approach to several layout optimization problems. A novel two-dimensional pattern generator, in connection with a set of routing and placement transformations, is employed to efficiently solve problems ranging from Wire Crossing Minimization and Topological Via Minimization to Minimum Steiner Tree Optimization and IO Alignment. The expected running time is O(nlogn) and the space requirement is O(n), where n is the number of layout objects. The system is fully coded and tested, and excellent results in both laboratory and real-life examples have been achieved.