Recent advances in reinforcement learning (RL) have renewed focus on the design of reward functions that shape agent behavior. Manually crafting such functions is often tedious and error-prone. A more principled alternative is to specify behavioral requirements using a formal, unambiguous language that can be automatically translated into a reward function. Omega-regular languages are a natural choice for this purpose, given their established role in formal verification and synthesis. However, existing approaches using omega-regular specifications typically rely on discounted reward RL in an episodic setting, where the environment is periodically reset to an initial state during learning. This setup is misaligned with the semantics of omega-regular specifications, which describe properties over infinite behavior traces. In such cases, the average reward criterion and the continuing setting—where the agent interacts with the environment over a single, uninterrupted lifetime—are more appropriate. To address the challenges of infinite-horizon, continuing tasks, we restrict our focus to the subclass of omega-regular languages known as absolute liveness specifications. These specifications cannot be violated by any finite prefix of the agent’s behavior, aligning naturally with the continuing setting. We present the first model-free RL framework that translates absolute liveness specifications to average-reward objectives. In contrast to prior work, our approach enables learning in communicating Markov Decision Processes without episodic resetting. We further introduce a reward structure for lexicographic multi-objective optimization, where the goal is to maximize an external average-reward objective among the policies that also maximize the satisfaction probability of a given absolute liveness omega-regular specification. Our method guarantees convergence in unknown communicating MDPs and supports on-the-fly reductions that do not require full knowledge of the environment, thus enabling model-free RL. Empirical results across various benchmarks demonstrate that our average-reward approach in the continuing setting is more effective than competing methods based on discounting.

Regular decision processes (RDPs) are a subclass of non-Markovian decision processes where the transition and reward functions are guarded by some regular property of the past (a lookback). While RDPs enable intuitive and succinct representation of non-Markovian decision processes, their expressive power coincides with finite-state Markov decision processes (MDPs). We introduce omega-regular decision processes (ODPs) where the non-Markovian aspect of the transition and reward functions are extended to an omega-regular lookahead over the system evolution. Semantically, these lookaheads can be considered as promises made by the decision maker or the learning agent about her future behavior. In particular, we assume that, if the promised lookaheads are not met, then the payoff to the decision maker is falsum (least desirable payoff), overriding any rewards collected by the decision maker. We enable optimization and learning for ODPs under the discounted-reward objective by reducing them to lexicographic optimization and learning over finite MDPs. We present experimental results demonstrating the effectiveness of the proposed reduction.

We present a modular approach to reinforcement learning (RL) in environments consisting of simpler components evolving in parallel. A monolithic view of such modular environments may be prohibitively large to learn, or may require unrealizable communication between the components in the form of a centralized controller. Our proposed approach is based on the assume-guarantee paradigm where the optimal control for the individual components is synthesized in isolation by making assumptions about the behaviors of neighboring components, and providing guarantees about their own behavior. We express these assume-guarantee contracts as regular languages and provide automatic translations to scalar rewards to be used in RL. By combining local probabilities of satisfaction for each component, we provide a lower bound on the probability of satisfaction of the complete system. By solving a Markov game for each component, RL can produce a controller for each component that maximizes this lower bound. The controller utilizes the information it receives through communication, observations, and any knowledge of a coarse model of other agents. We experimentally demonstrate the efficiency of the proposed approach on a variety of case studies.

Linear temporal logic (LTL) and omega-regular objectives---a superset of LTL---have seen recent use as a way to express non-Markovian objectives in reinforcement learning. We introduce a model-based probably approximately correct (PAC) learning algorithm for omega-regular objectives in Markov decision processes (MDPs). As part of the development of our algorithm, we introduce the epsilon-recurrence time: a measure of the speed at which a policy converges to the satisfaction of the omega-regular objective in the limit. We prove that our algorithm only requires a polynomial number of samples in the relevant parameters, and perform experiments which confirm our theory.

Abstract In reinforcement learning, an agent incrementally refines a behavioral policy through a series of episodic interactions with its environment. This process can be characterized as explicit reinforcement learning, as it deals with explicit states and concrete transitions. Building upon the concept of symbolic model checking, we propose a symbolic variant of reinforcement learning, in which sets of states are represented through predicates and transitions are represented by predicate transformers. Drawing inspiration from regular model checking, we choose regular languages over the states as our predicates, and rational transductions as predicate transformations. We refer to this framework as regular reinforcement learning , and study its utility as a symbolic approach to reinforcement learning. Theoretically, we establish results around decidability, approximability, and efficient learnability in the context of regular reinforcement learning. Towards practical applications, we develop a deep regular reinforcement learning algorithm, enabled by the use of graph neural networks. We showcase the applicability and effectiveness of (deep) regular reinforcement learning through empirical evaluation on a diverse set of case studies.

Alternating-time temporal logic (ATL) extends branching time logic by enabling quantification over paths that result from the strategic choices made by multiple agents in various coalitions within the system. While classical temporal logics express properties of “closed” systems, ATL can express properties of “open” systems resulting from interactions among several agents. Reinforcement learning (RL) is a sampling-based approach to decision-making where learning agents, guided by a scalar reward function, discover optimal policies through repeated interactions with the environment. The challenge of translating high-level objectives into scalar rewards for RL has garnered increased interest, particularly following the success of model-free RL algorithms. This paper presents an approach for deploying model-free RL to verify multi-agent systems against ATL specifications. The key contribution of this paper is a verification procedure for model-free RL of quantitative and non-nested classic ATL properties, based on Q-learning, demonstrated on a natural subclass of non-nested ATL formulas.

Abstract The difficulty of manually specifying reward functions has led to an interest in using linear temporal logic (LTL) to express objectives for reinforcement learning (RL). However, LTL has the downside that it is sensitive to small perturbations in the transition probabilities, which prevents probably approximately correct (PAC) learning without additional assumptions. Time discounting provides a way of removing this sensitivity, while retaining the high expressivity of the logic. We study the use of discounted LTL for policy synthesis in Markov decision processes with unknown transition probabilities, and show how to reduce discounted LTL to discounted-sum reward via a reward machine when all discount factors are identical.

Reinforcement learning (RL) is a powerful approach for training agents to perform tasks, but designing an appropriate reward mechanism is critical to its success. However, in many cases, the complexity of the learning objectives goes beyond the capabilities of the Markovian assumption, necessitating a more sophisticated reward mechanism. Reward machines and ω-regular languages are two formalisms used to express non-Markovian rewards for quantitative and qualitative objectives, respectively. This paper introduces ω-regular reward machines, which integrate reward machines with ω-regular languages to enable an expressive and effective reward mechanism for RL. We present a model-free RL algorithm to compute ε-optimal strategies against ω-regular reward machines and evaluate the effectiveness of the proposed algorithm through experiments.

Abstract Mungojerrie is an extensible tool that provides a framework to translate linear-time objectives into reward for reinforcement learning (RL). The tool provides convergent RL algorithms for stochastic games, reference implementations of existing reward translations for $$\omega $$ ω -regular objectives, and an internal probabilistic model checker for $$\omega $$ ω -regular objectives. This functionality is modular and operates on shared data structures, which enables fast development of new translation techniques. Mungojerrie supports finite models specified in PRISM and $$\omega $$ ω -automata specified in the HOA format, with an integrated command line interface to external linear temporal logic translators. Mungojerrie is distributed with a set of benchmarks for $$\omega $$ ω -regular objectives in RL.

The expanding role of reinforcement learning (RL) in safety-critical system design has promoted ω-automata as a way to express learning requirements—often non-Markovian—with greater ease of expression and interpretation than scalar reward signals. However, real-world sequential decision making situations often involve multiple, potentially conflicting, objectives. Two dominant approaches to express relative preferences over multiple objectives are: (1) weighted preference , where the decision maker provides scalar weights for various objectives, and (2) lexicographic preference , where the decision maker provides an order over the objectives such that any amount of satisfaction of a higher-ordered objective is preferable to any amount of a lower-ordered one. In this article, we study and develop RL algorithms to compute optimal strategies in Markov decision processes against multiple ω-regular objectives under weighted and lexicographic preferences. We provide a translation from multiple ω-regular objectives to a scalar reward signal that is both faithful (maximising reward means maximising probability of achieving the objectives under the corresponding preference) and effective (RL quickly converges to optimal strategies). We have implemented the translations in a formal reinforcement learning tool, Mungojerrie , and we present an experimental evaluation of our technique on benchmark learning problems.

Recursion is the fundamental paradigm to finitely describe potentially infinite objects. As state-of-the-art reinforcement learning (RL) algorithms cannot directly reason about recursion, they must rely on the practitioner's ingenuity in designing a suitable "flat" representation of the environment. The resulting manual feature constructions and approximations are cumbersome and error-prone; their lack of transparency hampers scalability. To overcome these challenges, we develop RL algorithms capable of computing optimal policies in environments described as a collection of Markov decision processes (MDPs) that can recursively invoke one another. Each constituent MDP is characterized by several entry and exit points that correspond to input and output values of these invocations. These recursive MDPs (or RMDPs) are expressively equivalent to probabilistic pushdown systems (with call-stack playing the role of the pushdown stack), and can model probabilistic programs with recursive procedural calls. We introduce Recursive Q-learning---a model-free RL algorithm for RMDPs---and prove that it converges for finite, single-exit and deterministic multi-exit RMDPs under mild assumptions.

Abstract We study reinforcement learning for the optimal control of Branching Markov Decision Processes (BMDPs), a natural extension of (multitype) Branching Markov Chains (BMCs). The state of a (discrete-time) BMCs is a collection of entities of various types that, while spawning other entities, generate a payoff. In comparison with BMCs, where the evolution of a each entity of the same type follows the same probabilistic pattern, BMDPs allow an external controller to pick from a range of options. This permits us to study the best/worst behaviour of the system. We generalise model-free reinforcement learning techniques to compute an optimal control strategy of an unknown BMDP in the limit. We present results of an implementation that demonstrate the practicality of the approach.

The ever increasing number of connected devices has lead to a metoric rise in the amount data to be processed. This has caused computation to be moved to the edge of the cloud increasing the importance of efficiency in the whole of cloud. The use of this fog computing for time-critical control applications is on the rise and requires robust guarantees on transmission times of the packets in the network while reducing total transmission times of the various packets. We consider networks in which the transmission times that may vary due to mobility of devices, congestion and similar artifacts. We assume knowledge of the worst case tranmssion times over each link and evaluate the typical tranmssion times through exploration. We present the use of reinforcement learning to find optimal paths through the network while never violating preset deadlines. We show that with appropriate domain knowledge, using popular reinforcement learning techniques is a promising prospect even in time-critical applications.

We characterize the class of nondeterministic $$\omega $$ -automata that can be used for the analysis of finite Markov decision processes (MDPs). We call these automata ‘good-for-MDPs’ (GFM). We show that GFM automata are closed under classic simulation as well as under more powerful simulation relations that leverage properties of optimal control strategies for MDPs. This closure enables us to exploit state-space reduction techniques, such as those based on direct and delayed simulation, that guarantee simulation equivalence. We demonstrate the promise of GFM automata by defining a new class of automata with favorable properties—they are Büchi automata with low branching degree obtained through a simple construction—and show that going beyond limit-deterministic automata may significantly benefit reinforcement learning.

We provide the first solution for model-free reinforcement learning of $$\omega $$ -regular objectives for Markov decision processes (MDPs). We present a constructive reduction from the almost-sure satisfaction of $$\omega $$ -regular objectives to an almost-sure reachability problem, and extend this technique to learning how to control an unknown model so that the chance of satisfying the objective is maximized. We compile $$\omega $$ -regular properties into limit-deterministic Büchi automata instead of the traditional Rabin automata; this choice sidesteps difficulties that have marred previous proposals. Our approach allows us to apply model-free, off-the-shelf reinforcement learning algorithms to compute optimal strategies from the observations of the MDP. We present an experimental evaluation of our technique on benchmark learning problems.

A constant-rate multi-mode system is a hybrid system that can switch freely among a finite set of modes, and whose dynamics is specified by a finite number of real-valued variables with mode-dependent constant rates. We introduce and study a stochastic extension of a constant-rate multi-mode system where the dynamics is specified by mode-dependent compactly supported probability distributions over a set of constant rate vectors. The almost-sure reachability problem for stochastic multi-mode systems is to decide whether for all ε > 0 and for all pairs of start and target states in a path-connected and bounded safety set there exists a control strategy that almost-surely steers the system from the start state to the ε-neighborhood of the target state without leaving the safety set. We prove a necessary and sufficient condition to decide almost-sure reachability and, using this condition, we show that almost-sure reachability can be decided in polynomial time. Our algorithm can be used as a path-following algorithm in combination with off-the-shelf path-planning algorithms to make a robot with noisy low-level controllers follow a path with arbitrary precision.

In this paper, we address the problem of performance modeling for transistor-level circuits under process variations. A sparse regression technique is introduced to characterize the relationship between the process parameters and the output responses. This approach relies on repeated simulations to find polynomial approximations of response surfaces. It employs a heuristic to construct sparse polynomial expansions and a stepwise regression algorithm based on LASSO to find low degree polynomial approximations. The proposed technique is able to handle many tens of process parameters with a small number of simulations when compared to an earlier approach using ordinary least squares. We present our approach in the context of statistical model inference (SMI), a recently proposed statistical verification framework for transistor-level circuits. Our experimental evaluation compares percentage yields predicted by our approach with Monte-Carlo simulations and SMI using ordinary least squares on benchmarks with up to 30 process parameters. The sparse-SMI approach is shown to require significantly fewer simulations, achieving orders of magnitude improvement in the run times with small differences in the resulting yield estimates.

This paper studies the effect of parameter variation on the behavior of analog circuits at the transistor (netlist) level. It is well known that variation in key circuit parameters can often adversely impact the correctness and performance of analog circuits during fabrication. An important problem lies in characterizing a safe subset of the parameter space for which the circuit can be guaranteed to satisfy the design specification. Due to the sheer size and complexity of analog circuits, a formal approach to the problem remains out of reach, especially at the transistor level. Therefore, we present a statistical model inference approach that exploits recent advances in statistical verification techniques. Our approach uses extensive circuit simulations to infer polynomials that approximate the behavior of a circuit. A procedure inspired by statistical model checking is then introduced to produce “statistically sound” models that extend the polynomial approximation. The resulting model can be viewed as a statistically guaranteed over-approximation of the circuit behavior. The proposed technique is demonstrated with two case studies in which it identifies subsets of parameters that satisfy the design specifications.

Model checking is a formal method for verifying whether the system satisfies a user-defined specification. Compared to simulation, model checking is restricted in capacity. On the other hand, simulation is weak in detecting bugs that require long and complex sequences of events to be exposed. This paper combines model checking and simulation in an abstraction-refinement scheme to mitigate the problems of both methods. Abstraction refinement iteratively constructs a simplified model to verify the original model. While a simplified model mitigates the weakness of model checking, the set of simplified error traces model helps guide simulation toward deep bugs. In abstraction refinement, concretization-a process of deriving an error trace in the original model from the abstract ones-is used to invalidate spurious abstract error traces or to refute a property. In this paper, we describe a novel concretization algorithm that combines simulation with satisfiability to efficiently refute properties with very long error traces.

Satisfiability (SAT) solvers often benefit from clauses learned by the DPLL procedure, even though they are by definition redundant. In addition to those derived from conflicts, the clauses learned by dominator analysis during the deduction procedure tend to produce smaller implication graphs and sometimes increase the deductive power of the input CNF formula. We extend dominator analysis with an efficient self-subsumption check. We also show how the information collected by dominator analysis can be used to detect redundancies in the satisfied clauses and, more importantly, how it can be used to produce supplemental conflict clauses. We characterize these transformations in terms of deductive power and proof conciseness. Experiments show that the main advantage of dominator analysis and its extensions lies in improving proof conciseness.

Satisfiability (SAT) solvers often benefit from transformations of the formula to be decided that allow them to do more through deduction and decrease their reliance on enumeration. For formulae in conjunctive normal form, subsumed clauses may be removed or partial resolution may be applied. The objectives of simplifying the formula and speeding up the solver are sometimes competing. We characterize existing transformations in terms of their impact on the deductive power of the formula and their effects on the sizes of the implication graphs. For example, we show that variable elimination works by improving implication graphs. We also present two new techniques that try to increase deductive power. The first is a check performed during the computation of resolvents. The second is a new preprocessing algorithm based on distillation that combines simplification and increase of deductive power. Most current SAT solvers apply resolution at various stages to derive new clauses or simplify existing ones. The former happens during conflict analysis, while the latter is usually done during preprocessing. We show how subsumption of the operands by the resolvent can be inexpensively detected during resolution; we then discuss how this detection is used to improve three stages of the SAT solver: variable elimination, clause distillation, and conflict analysis. The “on-the-fly” subsumption check is easily integrated in a SAT solver. In particular, it is compatible with strong conflict analysis and the generation of unsatisfiability proofs. Experiments show the effectiveness of the new techniques.

In one-to-many concretization for model checking based on abstraction refinement, constraints on input vectors that are pseudo-randomly generated are often essential to the success of the procedure. These constraints have to do with both primary inputs and invisible state variables. We discuss algorithms that address both types and we show their effectiveness through experiments.

In the game theoretic approach to the synthesis of reactive systems, specifications are often given as a conjunction of linear time properties. An implementation can be obtained from a winning strategy derived from a suitable generalized parity game in which each property produces a parity acceptance condition. Safety and persistence properties usually make up the majority of the specification. We show how this can be exploited to play the game in two stages and substantially speed up synthesis without sacrificing generality and conciseness of specification.

We present an improved algorithm for concretization of abstract error traces in abstraction refinement-based invariant checking. The proposed algorithm maps each transition of the abstract error trace to one or more transitions in the concrete model by using a combination of simulation and satisfiability checking. Prior simulation- based approaches were hindered by limited visibility, which often resulted in excessive backtracking or refinements. The proposed technique addresses this issue in three ways: By identifying variables whose addition to the abstract trace significantly improves its predictive power at a low computational cost; by combining SAT checks with pseudo-random simulation in the construction of the concrete trace; and by a more flexible budgeting of simulation vectors that accounts for the progress made in concretization.

Satisfiability (SAT) solvers often benefit from a preprocessing of the formula to be decided. For formulae in conjunctive normal form (CNF), subsumed clauses may be removed or partial resolution may be applied. Preprocessing aims at simplifying the formula and at increasing the deductive power of the solver. These two objectives are sometimes competing. We present a new algorithm that combines simplification and increase of deductive power and we show its effectiveness in speeding up SAT solvers.

In this paper, we present a method that helps improve the performance of Bounded Model Checking by automatically strengthening invariants so that the termination proof may be obtained by analyzing shorter paths. The strengthening technique identifies sets of states as byproducts of the termination checks. It then uses SAT-based preimage computations to extend those sets. Our approach may substantially speed up the verification of both failing and passing properties. We present experimental results showing that our new method improves the performance of BMC significantly.

We combine abstraction refinement and simulation to provide a more efficient approach to checking invariant properties whose only counterexamples are very long traces. We allow each transition of an abstract error trace to map to multiple transitions of the concrete error trace and simulate pseudorandom vectors to build segments of the concrete trace. This approach addresses the capacity limitation of the formal verification engine as well as the short-sightedness of the simulator, thus providing a more effective technique for deep, subtle bugs.

We present a new approach to conflict analysis for propositional satisfiability solvers based on the DPLL procedure and clause recording. When conditions warrant it, we generate a supplemental clause from a conflict. This clause does not contain a unique implication point, and therefore cannot replace the standard conflict clause. However, it is very effective at reducing excessive depth in the implication graphs and at preventing repeated conflicts on the same clause. Experimental results show consistent improvements over state-of-the-art solvers and confirm our analysis of why the new technique works.

The last few years have seen the advent of a new breed of decision procedures for various fragments of first-order logic based on propositional abstraction. A lazy satisfiability checker for a given fragment of first-order logic invokes a theory-specific decision procedure (a theory solver) on (partial) satisfying assignments for the abstraction. If the assignment is found to be consistent in the given theory, then a model for the original formula has been found. Otherwise, a refinement of the propositional abstraction is extracted from the proof of inconsistency and the search is resumed. We describe a theory solver for integer difference logic that is effective when the formula to be decided contains equality and disequality (negated equality) constraints so that the decision problem partakes of the nature of the pigeonhole problem. We propose a reduction of the problem to propositional satisfiability by computing bounds on a sufficient subset of solutions, and present experimental evidence for the efficiency of this approach

The main challenge in BDD-based symbolic reachability analysis is represented by the sizes of the intermediate decision diagrams obtained during image computations. Methods proposed to mitigate this problem fall broadly into two categories: Search strategies that depart from breadth-first search, and efficient techniques for image computation. In this paper we present an algorithm that belongs to the latter category. It exploits define-use information along executable paths extracted from the control-flow graph of the model being analyzed; this information enables an effective constraining of the transition relation and a decomposition of the image computation process that often leads to much smaller intermediate BDDs. Our experiments confirm that this reduction in the size of the representation of state sets translates in significant decreases in CPU and memory requirements.

The authors propose a scalable abstraction-refinement method for model checking invariant properties on large sequential circuits, which is based on fine-grain abstraction and simultaneous analysis of all abstract counterexamples of the shortest length. Abstraction efficiency is introduced to measure for a given abstraction-refinement algorithm how much of the concrete model is required to make the decision. The fully automatic techniques presented in this paper can efficiently reach or come near to the maximal abstraction efficiency. First, a fine-grain abstraction approach is given to keep the abstraction granularity small by breaking down large combinational logic cones with Boolean network variables (BNVs) and then treating both state variables and BNVs as atoms in abstraction. Second, a refinement algorithm is proposed based on an improved Ariadne's bundle In the legend of Theseus, Ariadne's bundle contained one ball of thread to help Theseus navigate the labyrinth. In this paper, we work with multiple threads-hence, the "improved." of synchronous onion rings on the abstract model, through which the transitions contain all shortest abstract counterexamples. The synchronous onion rings are exploited in two distinct ways to provide global guidance to the abstraction refinement process. The scalability of our algorithm is ensured in the sense that all the analysis and computation required in our refinement algorithm are conducted on the abstract model. Finally, we derive sequential don't cares from the invisible variables and use them to constrain the behavior of the abstract model. We conducted experimental comparisons of our new method with various existing techniques. The results show that our method outperforms other counterexample-guided methods in terms of both run time and abstraction efficiency

Finding all satisfying assignments of a propositional formula has many applications in the design of hardware and software. An approach to this problem augments a clause-recording propositional satisfiability solver with the ability to add blocking clauses, which prevent the solver from visiting the same solution more than once. One generates a blocking clause from a satisfying assignment by taking its complement. In this paper, we present an improved algorithm for finding all satisfying assignments for a generic Boolean circuit. An optimization based on lifting-which generates minimal satisfying assignments-yields prime blocking clauses. Thanks to the primality of the blocking clauses, the derived conflict clauses usually prune both satisfiable and unsatisfiable points at once. The efficiency of our new algorithm is demonstrated by our preliminary results on SAT-based unbounded model checking.

Bounded Model Checking (BMC) relies on solving a sequence of highly correlated Boolean satisfiability (SAT) problems, each of which checks for the existence of counter-examples of a bounded length. The performance of SAT search depends heavily on the variable decision ordering. We propose an algorithm to exploit the correlation among different SAT problems in BMC, by predicting and successively refining a partial variable ordering. This ordering is based on the analysis of all previous unsatisfiable instances, and is combined with the SAT solver's existing decision heuristic to determine the final variable decision ordering. Experiments on real designs from industry show that our new method improves the performance of SAT-based BMC significantly.

In the abstraction refinement approach to model checking, the discovery of spurious counterexamples in the current abstract model triggers its refinement. The proof - produced by a SAT solver - that the abstract counterexamples cannot be concretized can be used to identify the circuit elements or predicates that should be added to the model. It is common, however, for the refinements thus computed to be highly redundant. A costly minimization phase is therefore often needed to prevent excessive growth of the abstract model. In This work we show how to modify the search strategy of a SAT solver so that it generates refinements that are close to minimal, thus greatly reducing the time required for their minimization.

Abstraction refinement is a key technique for applying model checking to the verification of real-world digital systems. In previous work, the abstraction granularity is often limited at the state variable level, which is too coarse for verifying industrial-scale designs. In this paper, we propose a finer grain abstraction in which intermediate variables are selectively inserted to partition large combinational logic cones into smaller pieces; these intermediate variables, together with the state variables, are then treated as "atoms" in abstraction refinement. With this fine-grain approach, refinement is conducted in two different directions, sequential and Boolean. We propose a SAT-based method for predicting the appropriate refinement direction, and apply greedy minimization in both directions to keep the refinement set small. We also explore the use of approximate reachable states of the remaining submodules to help verifying the abstract model. Experimental studies show that the proposed techniques significantly improve the performance of abstraction refinement, and therefore increase the model checker's ability to handle large designs.

Despite a number of solid advances in simulation and verification techniques over the last twenty years, semiconductor chip designs continue to see large increases in the cost of verification - both in terms of human resources and time. Most of these increases are due to the growing size and complexity of the chip designs. Many of these designs are complete systems in their own right thus enlarging the scope of the verification problem. Formal verification has held out the most promise for reducing the magnitude of the verification task. Indeed, most major microprocessor teams - at IBM, Intel and Motorola - have routinely hosted formal verification experts since the early '90s. ASIC vendors and their tool providers have been closely following these developments into a number of initiatives and new startup companies driven by that very promise of formal verification. Despite these developments, simulation continues to be the final source of signoff - if not confidence - in chip tapeouts. Why is this so? Formal verification is an important technology to be left at the margins of the validation task. Will formal verification eliminate or limit unit level verification and provide the necessary glue for a realistic validation flow? Will the testbenches be replaced by constraints and assertions? Can validation effort be reused? This panel will explore the issues related to building practical validation flows, and the technologies that the designer community can realistically look forward to materializing in their lifetimes.

Coverage estimation for model checking quantifies the completeness of a set of properties. We present an improved version of the algorithm of Hoskote et al. [7] that applies to a larger subset of CTL; we prove properties of the algorithm and apply it to three case studies. From these case studies we derive recommendations for an effective use of coverage estimation.

We propose an abstraction refinement method for invariant checking, which is based on the simultaneous analysis of all abstract counter examples of shortest length in the current abstraction. The algorithm is focused on an improved Ariadne's Bundle/sup 1/ of SORs (Synchronous Onion Rings) of the abstract model; the transitions through these SORs contain all shortest ACEs (Abstract Counter Examples) and no other ACEs. The SORs are exploited in two distinct ways to provide global guidance to the abstraction refinement process: (1) Refinement variable selection is based on the entirety of transitions connecting the SORs, and (2) a SAT-based concretization test is formulated to test all ACEs in the SORs at once. We call this test multi-thread concretization. The scalability of our refinement algorithm is ensured in the sense that all the analysis and computation required in our refinement algorithm are conducted on the abstract model. The abstraction efficiency of a given abstraction refinement algorithm measures how much of the concrete model is required to make the decision. We include experimental comparisons of our new method with recently published techniques. The results show that our scalable method, based on global guidance from the entire bundle of shortest ACEs, outperforms these other methods in terms of both run time and abstraction efficiency.

Ordered binary decision diagrams (BDDs) are a data structure for the representation and manipulation of Boolean functions, often applied in very large scale integration (VLSI) computer-aided design (CAD). The choice of variable ordering largely influences the size of the BDD; its size may vary from linear to exponential. The most successful methods to find good orderings are based on dynamic variable reordering, i.e., exchanging neighboring variables. This basic operation has been used in various variants, like sifting and window permutation. In this paper, we show that lower bounds computed during the minimization process can speed up the computation significantly. First, lower bounds are studied from a theoretical point of view. Then these techniques are incorporated in dynamic minimization algorithms. By the computation of good lower bounds, large parts of the search space can be pruned, resulting in very fast computations. Experimental results are given to demonstrate the efficiency of the approach.

CTL model checking of complex systems often suffers from the state-explosion problem. We propose using Symbolic Guided Search to avoid difficult-to-represent sections of the state space and prevent state explosion from occurring.

Sequential verification methods based on reachability analysis are still limited by the size of the BDDs involved in computations. Extending their applicability to larger and real circuits is still a key issue. Within this framework, we explore a new way to improve symbolic traversal performance, working on the representation of state sets. We exploit retiming to reduce the number of latches of a FSM, and to relocate them in order to obtain a simplified state set representation. We consider retiming as a temporary state space transformation to increase the efficiency of sequential verification. We discuss it as a state space transformation and we formally analyze the conditions under which such a transformation is equivalence preserving for a given property under verification. We lower image computation cost, and we reduce the size of BDDs representing intermediate results and state sets. Experimental results show considerable memory and time improvements on some benchmark and home made circuits. 1

Image computation is the key step in fixpoint computations that are extensively used in model checking. Two techniques have been used for this step: one based on conjunction of the terms of the transition relation, and the other based on recursive case splitting. We discuss when one technique outperforms the other, and consequently formulate a hybrid approach to image computation. Experimental results show that the hybrid algorithm is much more robust than the “pure” algorithms and outperforms both of them in most cases. Our findings also shed light on the remark of several researchers that splitting is especially effective in approximate reachability analysis.

Traditional FPGA design flows have treated logic synthesis and physical design as separate steps. With the recent advances in technology the lack of information on the physical implementation during logic synthesis has caused mismatches between the final circuit characteristics (delay, power and area) and those predicted by logic synthesis. In this paper, we present a technique that tightly links the logic and physical domains-we combine logic and placement optimization in a single step. The combined algorithm is based on simulation annealing and hence, very amenable to new optimization goals or constraints. Two types of moves, directed towards global reduction in the cost function (linear congestion), are accepted by the simulated annealing algorithm: (1) logic optimization steps consisting of removing or replacing redundant wires in a circuit using functional flexibilities derived from SPFDs and (2) the placement optimization steps consisting of swapping a pair of blocks in the FPGA. Feedback from placement is very valuable in making an informed choice of a target wire during logic optimization moves. Experimental results demonstrate the efficacy of our approach over the placement independent approach.

Computer-aided design (CAD) tools are now making it possible to automate many aspects of the design process. This has mainly been made possible by the use of effective and efficient algorithms and corresponding software structures. The very large scale integration (VLSI) design process is extremely complex, and even after breaking the entire process into several conceptually easier steps, it has been shown that each step is still computationally hard. To researchers, the goal of understanding the fundamental structure of the problem is often as important as producing a solution of immediate applicability. Despite this emphasis, it turns out that results that might first appear to be only of theoretical value are sometimes of profound relevance to practical problems, VLSI CAD is a dynamic area where problem definitions are continually changing due to complexity, technology and design methodology. In this paper, we focus on several of the fundamental CAD abstractions, models, concepts and algorithms that have had a significant impact on this field. This material should be of great value to researchers interested in entering these areas of research, since it will allow them to quickly focus on much of the key material in our field. We emphasize algorithms in the area of test, physical design, logic synthesis, and formal verification. These algorithms are responsible for the effectiveness and efficiency of a variety of CAD tools. Furthermore, a number of these algorithms have found applications in many other domains.

We propose a new algorithm, called linear sifting, for the optimization of decision diagrams that combines the efficiency of sifting and the power of linear transformations. The new algorithm is applicable to large examples, and in many cases leads to substantially more compact diagrams when compared to simple variable reordering. We also show in what sense linear transformations complement variable reordering and how the technique can be applied to verification issues. Going a step further, we discuss a synthesis scenario where-due to the complexity of the target function-it is inevitable to decompose the function in a preprocessing step. By using linear sifting it is possible to extract a linear filter and, hence, to achieve the necessary decomposition. Using this method we were able to synthesize functions with standard tools which fail otherwise.

Retiming combined with combinational optimization is a powerful sequential synthesis method. However, this methodology has not found wide application because formal sequential verification is not practical and current simulation methodology requires the correspondence of latches disallowing any movement of latches. We present a practical verification technique which permits such sequential synthesis for a class of circuits. In particular, we require certain constraints to be met on the feedback paths of the latches involved in the retiming process. For a general circuit, we can satisfy these constraints by fixing the location of some latches, e.g., by making them observable. We show that equivalence checking after performing repeated retiming and synthesis on this class of circuit reduces to a combinational verification problem. We also demonstrate that our methodology covers a large class of circuits by applying it to a set of benchmarks and industrial designs.

Proposes lazy group sifting for dynamic variable reordering during state traversal of finite state machines (FSMs). The proposed method relaxes the idea of pairwise grouping of the present state variables and their corresponding next state variables. This is done to produce better variable orderings during image computation without causing BDD (binary decision diagram) size blowup in the substitution of next state variables with present state variables at the end of image computation. Experimental results show that our approach is more robust in state traversal than the approaches that either unconditionally group variable pairs or never group them.

The knowledge of the reachable states of a sequential circuit can dramatically speed up optimization and model checking. However, since exact reachability analysis may be intractable, approximate techniques are often preferable. H. Cho et al. (1996) presented the machine-by-machine (MBM) and frame-by-frame (FBF) methods to perform approximate finite state machine (FSM) traversal. FBF produces tighter upper bounds than MBM; however, it usually takes much more time and it may have convergence problems. In this paper, we show that there exists a class of methods-least fixpoint approximations-that compute the same results as RFBF ("reached FBF", one of the FBF methods). We show that one member of this class, which we call "least fixpoint MBM" (LMBM), is as efficient as MBM, but provably more accurate. Therefore, the trade-off that existed between MBM and RFBF has been eliminated. LMBM can compute RFBF-quality approximations for all the large ISCAS-89 benchmark circuits in a total of less than 9000 seconds.

Techniques for the computation of fixpoints are key to the success of many formal verification algorithms. To be efficient, these techniques must take into account how sets of states are represented. When BDDs are used, this means controlling, directly or indirectly, the size of the BDDs. Traditional fixpoint computations do little to keep BDD sizes small, apart from reordering variables. In this paper, we present a new strategy that attempts to keep the size of the BDDs under control at every stage of the computation. Our contribution includes also new techniques to compute partial images, and to speed up and test convergence. We present experimental results that prove the effectiveness of our strategy by demonstrating up to 40 orders of magnitude improvement in the number of states computed.

In order to simplify a synthesis task for particularly hard functions it is sometimes inevitable to decompose the function in a preprocessing step. We propose a new algorithm for automatically decomposing a target function by extracting a linear filter within the synthesis process. The algorithm is an application of the Linear Sifting algorithm which has been proposed in Meinel et al. (1996). Using this method we were able to synthesize functions with standard tools which fail otherwise.

This paper presents a new technique to perform power-oriented re-configuration of a system implemented using LUT FPGAs. The main features of our approach are: Accurate exploitation of degrees of freedom, concurrent optimization of multiple LUTs based on Boolean relations, and in-place re-programming without re-routing. Our tool optimizes the combinational component of the CLBs after layout, and does not require any re-wiring. Hence, delay and CLB usage are left unchanged, while power is minimized. As the algorithm operates locally on the various LUT clusters, it best performs on large examples as demonstrated by our experimental results: An average power reduction of 20.6% has been obtained on standard benchmarks.

Efficient techniques for the manipulation of Binary Decision Diagrams (BDDs) are key to the success of formal verification tools. Recent advances in reachability analysis and model checking algorithms have emphasized the need for efficient algorithms for the approximation and decomposition of BDDs. In this paper we present a new algorithm for approximation and analyze its performance in comparison with existing techniques. We also introduce a new decomposition algorithm that produces balanced partitions. The effectiveness of our contributions is demonstrated by improved results in reachability analysis for some hard problem instances.

This paper presents a nouel methodology for synthesizing PTL circuifg, whose disfincfiue feafures are the use of a symbolic algorifhm for the covem.ng of fhe initial network in ferms of PTL cells, and the eqloifation of layout-level ama and delay models dun.ng fhe selection of fhe be~t couem.ngsolufion.The results produced by the synthesis procedure on the full guite of fhe kcas'85 combinational circuifs are very encouraging.

RDCs (Reachability Don’t Cares) can have a dramatic impact on the cost of CTL model checking [18]. Unfortunately, RDCs, being a global property, are often much more difficult to compute than the satisfying set of typical CTL formulas. We address this problem through the use of Approximate Reachability Don’t Cares (ARDCs), computed with the algorithms developed for the VERITAS sequential synthesis package [4, 5]. Approximate Reachable states represent an upper bound on the set of true reachable states, and thus a lower bound on the set of unreachable (Don’t Care) states. ARDCs can be 10X to 100X (or much more for very large circuits) cheaper to compute than RDCs, and in some cases have the same dramatic effect on CTL model checking as the real RDCs. We also discuss the application of ARDCs to the problem of exact computation of the RDCs themselves. Experiments on industrial benchmarks show that order of magnitude speedups are possible, and occur frequently. The experimental results presented strongly support our claim that ARDCs play a safe and important way out of a serious dilemma: RDCs are necessary for tractable model checking of many large circuits, but the computation of the RDCs themselves is often intractable. We include, and theoretically justify, significant extensions of the VERITAS algorithms, and show that they can be up to an order of magnitude faster, while computing a virtually identical upper bound. 1

Retiming and resynthesis transformations can be used for optimizing the area, power, and delay of sequential circuits. Even though this technique has been known for more than a decade, its exact optimization capability has not been formally established. We show that retiming and resynthesis can exactly implement 1-step equivalent state transition graph transformations. This result is the strongest to date. We also show how the notions of retiming and resynthesis can be moderately extended to achieve more powerful state transition graph transformations. Our work will provide theoretical foundation for practical retiming and resynthesis based optimization and verification. 1 Introduction In combinational synthesis [1, 8], the positions of the latches are fixed and the logic is optimized for area, delay, or power. In retiming [5], the latches are moved across combinational gates. Retiming can change the number of latches (and hence the area) and the minimum cycle time (i.e., the clock r...

Silicon area, performance, and testability have been, so far, the major design constraints to be met during the development of digital very-large-scale-integration (VLSI) systems. In recent years, however, things have changed; increasingly, power has been given weight comparable to the other design parameters. This is primarily due to the remarkable success of personal computing devices and wireless communication systems, which demand high-speed computations with low power consumption. In addition, there exists a strong pressure for manufacturers of high-end products to keep power under control, due to the increased costs of packaging and cooling this type of device. Last, the need of ensuring high circuit reliability has turned out to be more stringent. The availability of tools for the automatic design of low-power VLSI systems has thus become necessary. More specifically, following a natural trend, the interests of the researchers have lately shifted to the investigation of power modeling, estimation, synthesis, and optimization techniques that account for power dissipation during the early stages of the design flow. This paper surveys representative contributions to this area that have appeared in the recent literature.

In the past, the major concern of the VLSI designers werearea, performance, cost, and reliability.In recent years,however, this has changed and, increasingly, power is beinggiven comparable weight to area and speed.This is mainlydue to the remarkable success of personal computing devicesand wireless communication systems, which demandhigh-speed computation and complex functionality with lowpower consumption.In addition, there exists a strong pressurefor manufacturers of high-end products to keep powerunder control.The main driving factors for lower powerdissipation in these products are the costs associated withpackaging and cooling, and circuit reliability.Tools for the automatic design of low-power VLSI systemshave thus become mandatory.More specifically, followinga natural trend, interests of researchers have latelyshifted to the investigation of high-level power modeling,estimation, synthesis, and optimization techniques that accountfor power dissipation as the primary cost factor.This paper provides a non-exhaustive survey of the mostsuccessful and innovative ideas in this area that have appearedin the literature in the last few years.

Binary Decision Diagrams (BDDs) are efficient at manipulating large sets in a compact manner. BDDs, however, are inefficient at utilizing the memory hierarchy ofthe computer. Recent work addresses this problem by manipulating the BDDsin breath-first manner (BFS). BFS processing is quite successful at reducing the number of page faults when the BDDs do not fit in the available physical memory. When pagingdoes not take place, it is much less clear which paradigmleads to the better performance. In this paper, we perform adetailed analysis of BFS and DFS packages using simulationand direct performance monitoring ofthe memory hierarchy.We show that there is very little difference in TLB and cachemiss rates for DFS and BFS paradigms. We also show thatdifferences in execution time between carefully tuned BFSand DFS implementations are primarily a function of thelossless computed table used in BFS implementations, andnot a function of memory locality. Furthermore, we presentimplementation changes to the the Cudd package that canimprove execution times by asmuch as 26% when the problem fits in main memory, and a factor of six when paging is involved.

We propose a new algorithm, called linear sifting, for theoptimization of decision diagrams that combines the efficiency of sifting and the power of linear transformations. We show that the new algorithm is applicable to large examples, and that inmany cases it leads to substantiallymore compact diagrams when compared to simple variablereordering. We show inwhat sense linear transformationscomplement variable reordering, and we discuss applications of the new technique to synthesis and verification.

We present an algorithm that restructures the state transition graph (STG) of a sequential circuit so as to reduce power dissipation.The STG is modified without changing the behavior of the circuit, by exploiting state equivalence.Bather than aiming primarily at reducing the number of states, our algorithm redirects transitions so that the new destination states are equivalent to the original ones, while the average activity of the circuit is decreased.The impact on area is also estimated to increase the accuracy of the power analysis.The STG and all other major data structures are stored as decision diagrams, and the algorithm does not enumerate explicitly the states or the transitions.(i.e., it is symbolic.)Therefore, it can deal with circuits that have millions of states.Once the STG has been restructured we apply symbolic factoring algorithms, based on Zero-suppressed BDDs, to convert the optimized graph into a multilevel circuit.We derive an efficient circuit from the BDDs of the STG by incorporating power constraints in the symbolic factoring algorithms.

This paper presents applications of algebraic decision diagrams (ADDs) to timing analysis and resynthesis for low power of combinational CMOS circuits. We first propose a symbolic algorithm to perform true delay calculation of a technology mapped network; the procedure we propose, implemented as an extension of the SIS synthesis system, is able to provide more accurate timing information than any other method presented so far; in particular, it is able to compute and store the arrival times of all the gates of the circuit for all possible input vectors, as opposed to the traditional methods which consider only the worst case primary inputs combination. Furthermore, the approach does not require any explicit false path elimination. We then extend our timing analysis tool to the symbolic calculation of required times and slacks, and we use this information to perform resynthesis for low power of the circuit by gate resizing. Our approach takes into account false paths naturally; in fact, it guarantees that resizing of the gates does not increase the true delay of the circuit, even in the presence of false paths. Our experiments have shown that many circuits, originally free of false paths, exhibit a large number of these false paths when optimized for area; therefore, the ability to deal with circuits containing false paths is of primary importance. We present experimental results for ADD-based and static timing analysis-based resynthesis, which clearly show that our tool is superior in the case of circuits containing false paths, but at the same time, it provides competitive results in the case of circuits which are free of false paths.

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 a novel technique for re-synthesizing circuits for low-power dissipation. Power consumption is reduced through redundancy addition and removal by using learning to identify indirect logic implications within a circuit. Such implications are exploited by adding gates and connections to the circuit without altering its overall behavior and thereby enabling us to eliminate other, high power dissipating, nodes. We propose a new BDD-based method for computing indirect implications in a logic network; furthermore, we present heuristic techniques to perform redundancy addition and removal without destroying the topology of the mapped circuit. Experimental results show the effectiveness of the proposed technique in reducing power while keeping within delay and area constraints.

Exploiting circuit structure is a key issue in the implementation of algorithms for state space decomposition when the target is approximate FSM traversal. Given the gate-level description of a sequential circuit, the information about its structure can be captured by evaluating the affinity between pairs or groups of latches. Two main factors have to be considered in carrying out the structural analysis of a sequential circuit: latch connectivity and latch correlation. The first one takes into account the mutual dependency of each memory element on the others; the second one tells us how related are the functions realized by the logic feeding each latch. In this paper we estimate the affinity of two latches by combining these two factors, and we use this measure to formulate the state space decomposition problem as a graph partitioning problem. We propose an algorithm to automatically determine "good" partitions of the latch set which induce state space decomposition, and we present approximate FSM traversal and logic optimization results for the largest ISCAS'89 sequential benchmarks.

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.

Regarding finite state machines as Markov chains facilitates the application of probabilistic methods to very large logic synthesis and formal verification problems. In this paper we present symbolic algorithms to compute the steady-state probabilities for very large finite state machines (up to 10/sup 27/ states). These algorithms, based on Algebraic Decision Diagrams (ADD's)-an extension of BDD's that allows arbitrary values to be associated with the terminal nodes of the diagrams-determine the steady-state probabilities by regarding finite state machines as homogeneous, discrete-parameter Markov chains with finite state spaces, and by solving the corresponding Chapman-Kolmogorov equations. We first consider finite state machines with state graphs composed of a single terminal strongly connected component; for this type of system we have implemented two solution techniques: One is based on the Gauss-Jacobi iteration, the other one is based on simple matrix multiplication. Then we extend our treatment to the most general case of systems which can be modelled as finite state machines with arbitrary transition structures; here our approach exploits structural information to decompose and simplify the state graph of the machine. We report experimental results obtained for problems on which traditional methods fail.

This paper studies the problem of estimating worst case power dissipation in a sequential circuit.We approach this problem by nding the maximum average weight cycles in a weighted directed g r aph.In order to handle practical sized examples, we use symbolic methods, based o n A lgebraic Decision Diagrams (ADDs), for computing the maximum average length cycles as well as the number of gate transitions in the circuit, which is necessary to construct the weighted directed g r aph.

We present a boolean technique to reduce power consumption of combinational circuits that have already been optimized for area and delay and then mapped onto a library of gates. In order to achieve a better optimization, we cluster gates by collapsing two or more levels of gates into a single node. When optimizing each cluster, our method extends the algorithms used in ESPRESSO, by adding heuristics that bias the minimization toward lowering the power dissipation in the circuit. The results of our method, on a number of benchmark circuits, show an average of 11% improvement in power savings compared to existing boolean techniques.

Dynamic reordering techniques have had considerable success in reducing the impact of the initial variable order on the size of decision diagrams. Sifting, in particular, has emerged as a very good compromise between low CPU time requirements and high quality of results. Sifting, however, has the absolute position of a variable as the primary objective, and only considers the relative positions of groups of variables indirectly. In this paper we propose an extension to sifting that may move groups of variables simultaneously to produce better results. Variables are aggregated by checking whether they have a strong affinity to their neighbors. (Hence the title.) Our experiments show an average improvement in size of 11%. This improvement, coupled with the greater robustness of the algorithm, more than offsets the modest increase in CPU time that is sometimes incurred.

We address the problem of reachability analysis for large finite state systems. Symbolic techniques have revolutionized reachability analysis but still have limitations in traversing large systems. We present techniques to improve the symbolic breadth-first traversal and compute a lower bound on the reachable states. We identify the problem as one of density during traversal and our techniques seek to improve the same. Our results show a marked improvement on the existing breadth-first traversal methods.

Regarding finite state machines as Markov chains facilitates the application of probabilistic methods to very large logic synthesis and formal verification problems. Recently, we have shown how symbolic algorithms based on Algebraic Decision Diagrams may be used to calculate the steadystate probabilities of finite state machines with more than 10 8 states. These algorithms treated machines with state graphs composed of a single terminal strongly connected component. In this paper we consider the most general case of systems which can be modeled as state machines with arbitrary transition structures. The proposed approach exploits structural information to decompose and simplify the state graph of the machine. 1 Introduction Finite state machines (FSMs), or their extensions, are often employed to model real digital systems for formal verification. As the complexity of those systems increases, probabilistic approaches to design and implementation verification become of interest; for...

Symbolic computation techniques play a fundamental role in logic synthesis and formal hardware verification algorithms. Recently, Algebraic Decision Diagrams, i.e., BDDs with a set of constant values different to the set /spl lcub/0,1/spl rcub/, have been used to solve general purpose problems, such as matrix multiplication, shortest path calculation, and solution of linear systems, as well as logic synthesis and formal verification problems, such as timing analysis, probabilistic analysis of finite state machines, and state space decomposition for approximate finite state machine traversal. ADD-based procedures for single-source and all-pairs shortest path weight calculation have appeared to be very effective for the manipulation of large graphs (over 10/sup 27/ vertices and 10/sup 36/ edges). However, for those procedures to be applicable to real problems, for example flow network problems, computing only shortest path weights is not enough; what it is needed is an algorithm that, given the weight of a shortest path between two vertices of a graph, actually determines the sequence of vertices belonging to the shortest path. This paper proposes a symbolic algorithm to execute shortest path back-tracing which exploits the compactness of the ADD data structure to handle large graphs.>

Exploiting circuit structure is a key issue in the implementation of algorithms for state space decomposition when the target is approximate FSM traversal. Given the gate-level description of a sequential circuit, the information about its structure can be captured by evaluating the affinity between pairs or groups of latches. Two main factors have to be considered in carrying out the structural analysis of a sequential circuit: latch connectivity and latch correlation. We estimate the affinity of two latches by combining these two factors, and we use this measure to translate the state space decomposition problem into a graph partitioning problem. Traversal results obtained on the largest ISCAS'89 benchmarks show the effectiveness of the method.>

In this paper we present two exact algorithms for state minimization of FSM's. Our results prove that exact state minimization is feasible for a large class of practical examples, certainly including most hand-designed FSM's. We also present heuristic algorithms, that can handle large, machine-generated, FSM's. The possibly many different reduced machines with the same number of states have different implementation costs. We discuss two steps of the minimization procedure, called state mapping and solution shrinking, that have received little prior attention to the literature, though they play a significant role in delivering an optimally implemented reduced machine. We also introduce an algorithm whose main virtue is the ability to cope with very general cost functions, while providing high performance.>

We explore the nature of incomplete specification in sequential circuits. We compare it to the case of combinational circuits and propose new definitions and algorithms. We extend the existing algorithms for input don't care sequences and provide a new theory for output don't care sequences, based on the concept of information lossyness. The implementation of the proposed techniques in a program called SEQUOIA (sequential optimization of interacting automata) shows that our approach is viable and effective.>

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

computing synchronizing sequences is an important step in experimental results that show the viability of the proposed method for much larger circuits than were tractable by previous exact methods.

In this paper we present theory and experiments on the algebraic decision diagrams (ADDs). These diagrams extend BDD's by allowing values from an arbitrary finite domain to be associated with the terminal nodes. We present a treatment founded in Boolean algebras and discuss algorithms and results in applications like matrix multiplication and shortest path algorithms. Furthermore, we outline possible applications of ADD's to logic synthesis, formal verification, and testing of digital systems.

We present an algorithm for finding the maximum flow in a 0-1 network. The algorithm is symbolic and avoids explicit enumeration of the nodes and edges of the network. Therefore, it can handle much larger graphs than it was previously possible (more than 10/sup 36/ edges). The main idea is to trace (implicitly) sets of edge-disjoint augmenting paths. Disjointness is enforced by solving an edge matching problem for each layer of the network with the help of newly defined priority functions.

Finite state machine (FSM) verification based on implicit state enumeration can be extended to test generation and redundancy identification. The extended method constructs the product machine of two FSMs to be compared, and reachability analysis is performed by traversing the product machine to find any difference in I/O behavior. When an output difference is detected, the information obtained by reachability analysis is used to generate a test sequence. This method is complete, and it generates one of the shortest possible test sequences for a given fault. However, applying this method indiscriminately for all faults may result in unnecessary waste of computer resources. An efficient method based on reachability analysis of the fault-free machine (three-phase ATPG) in addition to the powerful but more resource-demanding product machine traversal is presented. The application of these algorithms to the problems of generating test sequences, identifying redundancies, and removing redundancies is reported.>

The binate covering problem (BCP) is the problem of finding a minimum cost assignment to variables that is a solution of a Boolean equation f=1. It is a generalization of the set covering (or unate covering) problem, where f is positive unate, and is generally given as a table with rows corresponding to the set elements and the columns corresponding to the subsets. Previous methods have considered the case when f is given as a product-of-sum formula or as a binary decision diagram (BDD). A branch-and-bound algorithm for the BCP that assumes f is expressed as the conjunction of multiple BDDs is presented. The BCP solver that has been implemented can be applied to several problems, including exact minimization of Boolean relations, for which results are presented. It has been possible to solve large, difficult problems (up to 4692 variables) which could not be solved by the product of sum based method.>

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.>

A. Grasselli and F. Luccio (1965) proved that a minimum state cover of an incompletely specified finite-state machine could be found by only considering prime compatibles. It was conjectured that in practice one could restrict even further the set of compatibles being considered to the set of maximal compatibles. The conditions under which a solution formed of maximal compatibles was guaranteed to be exact were determined, but the question of the practical relevance of prime compatibles remained open. It is shown here that state minimization problems which require the full generality afforded by prime compatibles for the solution to be optimal are actually found in practice. The proof relies on the concept of analogous machines-essentially machines that pose the same minimization problem. The main result is that for any incompletely specified machine there is an analogous machine that has to be minimized in the optimization of two interacting, completely specified machines. >

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.>

The authors consider the nature of incomplete specifications for a finite state machine embedded in a network of sequential machines. They show how limited controllability and observability of component machines are expressed in quite different ways. For the input don't care sequences, a general solution was known. The authors present extensions to it, both in terms of topologies contemplated and in terms of applicability to larger designs. For the output don't care sequences, they provide a general theory based on the concept of information lossyness and present algorithms to address the related optimization problem in practical cases. The implementation of the proposed techniques in a program called SEQUOIA (sequential optimization of interacting automata) shows that the proposed approach is viable and effective.>

The knowledge of the state transition graph (STG) of a sequential circuit helps in generating test sequences and identifying redundancies. The application of algorithms to the identification and removal of redundancies is reported. This strategy is based on traversing the STG of the given circuit and then performing redundancy identification using the reachability information calculated by the traversal. This method considers one candidate redundancy at a time, in an order that tries to minimize the total processing time. Substantial area and delay reductions are achieved. Experiments show that for many circuits 100% of the sequentially redundant faults can be eliminated in very reasonable amounts of time.>

The knowledge of the State Transition Graph (STG) of a sequential circuit helps in generating test sequences. For instance, by determining that a set of states is not reachable from the reset state, it is possible to identify a certain type of sequentially untestable faults. However, until recently, the ability of algorithms to store the STG of a sequential circuit has been limited to small instances. Recent advances in sequential circuit verification, based on the use of binary decision diagrams and new powerful implicit enumeration algorithms, have dramatically improved our ability to deal with large numbers of states. In this paper we report on the application of these algorithms to the problems of generating justification sequences, identifying redundancies, and dealing with hard-to-detect faults. Our experiments show substantial improvements over previously published results.

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.>

The problem of minimizing symbolic relations is addressed. The relevance of this problem in the field of optimal encoding is shown by examples. A binate covering formulation of the optimization problems involved is given, for which several algorithms are available. A novel method is proposed which is based on binary decision diagrams (BDDs) and the authors show how the covering problem can be solved in linear time in that case.>

Boolean relations are a generalization of incompletely specified logic functions. The authors give a procedure, similar to the Quine-McCluskey procedure, for finding the global optimum sum-of-product representation for a Boolean relation. This is formulated as a binate covering problem, i.e. as a generalization of the ordinary (unate) covering problem. They give an algorithm for it and review the relation of binate covering to tautology checking. The procedure has been implemented and results are presented.>

External, intermediate, and fan-out don't care sets have been used to describe information about network structure required to optimize a node of a Boolean network locally. Another method to optimize a network has been called global flow analysis. The authors relate these approaches, generalize global flow to arbitrary Boolean networks, and suggest new algorithms for these problems.>

MOZART, a concurrent fault simulator for large circuits described at the register-transfer, functional, gate, and switch levels, is described. The requirements of multilevel simulation have guided the definition of MOZART's syntax, value set, delay model, and algorithms. Performance is improved by reducing unnecessary activity. Two such techniques are levelized: two-pass simulation, which minimizes the number of events and evaluations, and list event scheduling, which allows optimized processing of simultaneous (fraternal) events for concurrent machines. Moreover, efficient handling of abnormally large or active fault machines can improve fault-simulator performance by several orders of magnitude. These and related issues are discussed; both analytical and experimental evidence is provided for the effectiveness of the solutions adopted in MOZART. A performance metric is introduced for fault simulation, based on comparison with the serial algorithm, and is more accurate than those used in the past.>

This paper addresses the problem of event-directed logic simulation with part of the elements having zero delay. Incoherences arising from spikes having null duration (i.e., multiple transitions of a signal at a given simulation time, due to the simulation algorithm) are solved by a Two-Pass procedure, combining levelizing and event-driven simulation and yielding Ordered Activity Propagation. To overcome the speed degradation with respect to One-Pass simulation, a variation of the usual Two-Pass technique, termed Predictor/Corrector, is introduced at the gate level. Ordered Activity Propagation is also beneficial to concurrent multilevel simulation.

Fault simulation of circuits described at multiple levels of abstraction (RT, gate, switch) is a major problem in the area of CAD and testing. Although the concurrent paradigm is generally acknowledged as the most efficient, several techniques are crucial to successfully extend it to multilevel simulation of large circuits. In particular, based on multilist traversal, fraternal event processing, list events, and levelizing, advances are presented here in simulation speed, accuracy, and generality. For zero-delay elements, the simulation of irrelevant activity is avoided, but the accuracy of structural (interconnect) logic simulation is maintained. What is described here has been implemented in MOZART, and detailed experimental results are reported. Relative to the good machine, the average faulty machine is simulated 900 to 17 000 times faster. The approach presented is not restricted to fault simulation, and is thus applicable to the new area of concurrent case simulation.

When designing fault-tolerant systems including programmable logic arrays (PLAs), the various aspects of these circuits concerning fault diagnosis have to be taken into account. The peculiarity of these aspects, ranging from fault models to test generation algorithms and to self-checking structures, is due to the regularity of PLAs. The fault model generally accepted for PLAs is the crosspoint defect; it is employed by dedicated test generation algorithms, based on the fact that PLAs implement a two-level combinational function. The problem of accessing inputs and outputs of the PLA can be alleviated by augmenting the PLA itself so as to simplify the test vectors to be applied, making them function independent in the limit. A further step consists in the addition of the circuitry required to generate test vectors and to evaluate the answer, thus obtaining a built-in self-test (BIST) architecture. Finally, high reliability can be achieved with PLAs featuring concurrent error detection.

The increasing complexity of VLSI systems demands structured approaches to reduce both design time and test generation effort. PLA's and scan paths have both been widely reported to be efficient in this sense. This correspondence presents an easily testable structure and its related testing strategies. The circuits are assumed to be based on the interconnection of combinatorial macros, mostly implemented by PLA's; tests are generated locally, considering the involved macro as an isolated item, and then are expressed in terms of primary inputs and outputs using a topological approach as general strategy and algebraic techniques for the propagation of signals through macros. Propagation is dealt with by new algorithms. Since the problem of test generation is NP-hard, a set of heuristics is introduced to keep the amount of computation reasonable; several implementation issues are finally investigated.

PART is a system for PLA testing and design verification, intended to be properly interfaced with other existing tools to generate a comprehensive design environment. To this purpose, it provides several facilities, among which the capability of generating a fault population on the basis of layout information. PART aims at producing a very compact test set for all detectable crosspoint defects, using limited amounts of run time and storage. This is achieved by means of an efficient partitioning algorithm together with powerful heuristics. Test minimality is ensured by a simple procedure. In the present paper these are discussed, experimental results are given and a comparison with competing strategies is made.