The generalization of Property Directed Reachability (PDR) for the theory QF_BV presented in [1] outperforms the original formulation if the required inductive invariant can be represented efficiently as a set of polytopes. However, many QF_BV model checking instances do not belong in this class and can be solved quickly with the original PDR algorithm. In this paper, we present a hybrid approach which uses both polytopes and Boolean cubes as atomic reasoning units combining the advantages of either homogeneous approach. We discuss theoretic properties of the presented algorithm and report experimental results demonstrating its effectiveness.

We present a novel, sound, and complete algorithm for deciding safety properties in programs with static memory allocation. The new algorithm extends the program verification paradigm using loop invariants presented in [1] with a counterexample guided abstraction refinement (CEGAR) loop [2] where the refinement is achieved by strengthening loop invariants using the QFBV generalization of Property Directed Reachability (PDR) discussed in [3, 4]. We compare the algorithm with other approaches to program verification and report experimental results.

In 2011, property directed reachability (PDR) was proposed as an efficient algorithm to solve hardware model checking problems. Recent experimentation suggests that it outperforms interpolation-based verification, which had been considered the best known algorithm for this purpose for almost a decade. In this work, we present a generalization of PDR to the theory of quantifier free formulae over bitvectors (QF BV), illustrate the new algorithm with representative examples and provide experimental results obtained from experimentation with a prototype implementation.

Modern synthesis flows apply a series of technology independent optimization steps followed by mapping algorithms which bind the optimized network to a specific technology library. As the exact solution of the mapping problem is computationally intractable, algorithms used in practice use heuristic, typically tree-based approaches. The application of these algorithms results in mapped but suboptimal networks. In this work, we present a novel, efficient, and effective optimization algorithm for mapped networks which can be considered a generalization of SAT-sweeping. Our algorithm searches for alternative, more efficient implementations of each net in the network. Candidate support nets for reimplementation are selected using simulation signatures and verified using Boolean satisfiability. We report experimental results on the quality of our algorithm obtained from an implementation of the approach using the logic synthesis system ABC.

Constrained random simulation has been widely adopted in contemporary hardware verification flows. In this methodology, a set of user-specified declarative constraints describe valid input stimuli for the design under test (DUT). A constraint solver produces the simulation input vectors; their generation is interleaved with the actual simulation of the design for these vectors. Besides its distribution, the solver's performance is one of the most critical characteristics that determines the overall verification efficiency. There are no general approaches to hardware acceleration for solving declarative constraints. Current setups for hardware acceleration-based verification combine a software constraint solver running on a general-purpose processor with the hardware-accelerated DUT. This approach suffers from a major efficiency bottleneck caused by the significant performance mismatch between the solver executed in software and the DUT running on an accelerator. In this paper, we present a hardware constraint solver that uses a set of parallel solving units executing Markov chain Monte Carlo sampling. We propose to combine this solver and the DUT on the same device and run both entities hardware-accelerated in order to eliminate the performance mismatch. We discuss the details of the solver architecture and its implementation and report comprehensive results on performance and distribution characteristics as well as experience obtained from our case study where we used our solver to verify a real-world hardware design.

A systematic investigation is presented about the robustness of logic synthesis tools to equivalence-preserving transformations of the input Verilog file. We have developed a framework that: 1) parses Verilog behavioral models into an abstract syntax tree; 2) generates random equivalence-preserving transformations on the syntax tree, and; 3) writes the transformed design back in Verilog format. The original and the transformed Verilog descriptions are then checked for equivalence and synthesized. Results show that average (peak) improvements in area of 2.5% (11%) and length of the critical path of 4% (13%) are achievable. Indeed these figures are comparable to recent advancements in logic synthesis ([17] [8] achieve 4.9% (23%) 5% (24%) improvements area-wise, respectively), signaling a relevant lack of robustness in synthesis tools. This lack of robustness suggests that new synthesis algorithms should be evaluated by measuring the average improvement on several transformed files to assess their real contributions to the quality of the results.

Modern logic synthesis systems apply a sequence of loosely-related function-preserving transformations to gradually improve the circuit with respect to certain criteria such as area, performance, power, etc. For the quality of a complete synthesis run, the application order of the transformations for the individual steps are critical as they can produce vastly different outcomes. In practice, the transformation sequences is encoded in synthesis scripts which are derived manually based on experience and intuition of the tool developer. These scripts are static in the sense that transformations are applied independently of the result of previous transformations or the current status of the design. Despite the importance of obtaining high quality scripts, there are only a few attempts to optimize them. In this paper, we present a novel method to select transformations dynamically during the synthesis run leveraging the theory of Markov Decision Processes. The decision to select a particular transformation is based on transition probabilities, the history of the applied synthesis steps, and expectations for future steps. We report experimental results obtained from an implementation of the approach using the logic synthesis system ABC.

Conventional logic synthesis flows are composed of three separate phases: technology independent optimization, technology mapping, and technology dependent optimization. A fundamental problem with such a three-phased approach is that the global logic structure is decided during the first phase without any knowledge of the actual technology parameters considered during later phases. Although technology dependent optimization algorithms perform some limited logic restructuring, they cannot recover from fundamental mistakes made during the first phase, which often results in non-satisfiable solutions. In this paper, we present a method for integrating the three synthesis phases using an annealing algorithm as optimization framework. The annealing-based search is driven by a complex objective function, combining both technology independent as well as technology dependent optimization criteria. Our experimental results shown that, on average, the presented approach can improve the area and delay of circuits optimized with script rugged of SIS by 11.2% and 32.5% respectively.

Cloud computing is used to describe a collection of (remote) data centers (the hardware and the software) and applications delivered from them as a service (SaaS, Software as a Service). Its success is driven by the cost-effective on-demand availability of large, scalable amounts of computing resources. The cloud has become an established paradigm for many enterprise and consumer applications such as email, web servers, productivity applications, customer relationship management, etc. However, in IC design its success is still limited.

A crisis is a terrible thing to waste. Quotes like this are often heard by experts in the industry and academia but what does this mean to me? How should I change my professional interests? How should I evolve my career? How is EDA going to evolve? The panel represents multiple points of views on these questions. Four experts will review the current job situation in EDA and provide a historical perspective for previous recessions. The panel will further discuss views on new directions for the Electronics market, how EDA should evolve, and options for career development during the slow down of the industry.

Over the past 20 years, EDA has developed a solid digital implementation methodology that combines some restrictions on the design style with a set of comprehensive tools leading to predictable design flows. The recent increased use of analog components in complex SOC designs triggered a set of verification challenges ranging from simple connectivity problems to complex interferences between analog and digital data blocks. This panel discusses the state of the affairs in analog-mixed signal verification and draws a picture of future directions in terms of new approaches and tools.

Functional verification is a major part of the effort to design electronic systems. Over the years, EDA has developed a suite of tools and methods to address the verification challenges by a patchwork of approaches. However, as the system complexity continues to increase, traditional methods may not be adequate to ensure flawless behavior. In this educational panel, we will explore how complex systems are validated in other areas. Four speakers will cover the verification challenges in airplane design, complex Mars exploration missions, modeling and rendering of movie animations, and the design of continent-wide national power grids. Using real-life examples, each speaker will introduce the general topic, outline the specific verification challenges, and discuss how they are approached in their specific domain. The following discussion will analyze commonalities and differences between the areas and explore lessons to be learned from them for EDA.

Yesterday's cell phones have rapidly evolved into versatile multi-media computers heavily loaded with a wide spectrum of technologies to support many functions and use modes. Designing and verifying such complex devices becomes increasingly challenging due to the need to: incorporate larger number of functions and diverse use modes, increased bandwidth, provide support for multimedia devices with high resolution, offer new methods for user interactions, and all of this at a fixed power budget and with high reliability. In addition, teams need to keep up with the convergence of wireless radio algorithms and be able to support more functionality moving into the software layer.

Modern combinational equivalence checking (CEC) engines are complicated programs which are difficult to verify. In this paper we show how a modern CEC engine can be modified to produce a proof of equivalence when it proves a miter unsatisfiable. If the CEC engine formulates the problem as a single SAT instance (call this naive), one can use the resolution proof of unsatisfiability as a proof of equivalence. However, a modern CEC engine does not directly invoke a SAT solver for the whole miter, but instead uses a variety of techniques such as structural hashing, detection of intermediate functional equivalences, and circuit re-writing to first simplify the problem. We show that in spite of using these simplification techniques, a CEC engine can be modified to generate a single (extended) resolution proof for the whole miter just as in the naive case. The benefit of having a single proof is that the proof verification program remains extremely simple, and its correctness is much easier to establish than that of the CEC engine.

Constrained random simulation is the main workhorse in today 's hardware verification flows. It requires the random generation of input stimuli that obey a set of declaratively specified input constraints, which are then applied to validate given design properties by simulation. The efficiency of the overall flow depends critically on (1) the performance of the constraint solver and (2) the distribution of the generated solutions. In this paper we discuss the overall problem of efficient constraint solving for stimulus generation for mixed Boolean/integer variable domains and propose a new hybrid solver based on Markov-chain Monte Carlo methods with good performance and distribution.

SAT sweeping is a method for simplifying an shape And/Inverter graph (AIG) by systematically merging graph vertices from the inputs towards the outputs using a combination of structural hashing, simulation, and SAT queries. Due to its robustness and efficiency, SAT sweeping provides a solid algorithm for Booleanreasoning in functional verification and logic synthesis. In previous work, SAT sweeping merges two vertices only if they are functionally equivalent. In this paper we present a significant extension of the SAT-sweeping algorithm that exploits local observability don't-cares (ODCs) to increase the number of vertices merged. We use a novel technique to bound the use of ODCs and thus the computational effort to find them, while still finding a large fraction of them. Our reported results based on a set of industrial benchmark circuits demonstrate that ODC-based SAT sweeping results in significantly more graph simplification with great benefit for Boolean reasoning with a moderate increase in computational effort.

Boolean matching is a powerful technique that has been used in technology mapping to overcome the limitations of structural pattern matching. The current basis for performing Boolean matching is the computation of a canonical form to represent functions that are equivalent under negation and permutation of inputs and outputs. In this paper, we first present a detailed analysis of previous techniques for Boolean matching. We then describe a novel combination of existing methods and new ideas that results in a matcher which is dramatically faster than previous work. We point out that the presented algorithm is equally relevant for detecting generalized functional symmetries, which has broad applications in logic optimization and verification

In this paper we describe a new logic synthesis approach based on rule-based randomized search using simulated annealing. Our work is motivated by two observations: (1) Traditional logic synthesis applies literal count as the primary quality metric during the technology independent optimization phase. This simplistic metric often leads to poor circuit structures as it cannot foresee the impact of early choices on the final area, delay, power consumption, etc. (2) Although powerful, global Boolean optimization is not robust and corresponding algorithms cannot be used in practice without artificially restricting the application window. Other techniques, such as algebraic methods scale well but provide weaker optimization power. To address both problems, we use randomized search that is based on a simple circuit graph representation and a complete set of local transformations that include algebraic and Boolean optimization steps. The objective of the search process can be tuned to complex cost functions, combining area, timing, routability, and power. Our experimental results on benchmark functions demonstrate the significant potential of the presented approach.

Traditional approaches for sequential logic optimization include (1) explicit state-based techniques such as state minimization, (2) structural techniques such as retiming, and (3) methods that exploit sequential don't-cares derived from unreachable states. These approaches optimize a logic circuit as a single component with a single input/output behavior. In this paper we present a novel concept for sequential optimization referred to as temporal decomposition, which distinguishes the logic that initializes the circuit from the logic needed for the behavior after startup. This work was motivated by a recent observation made for bounded property verification: There is a substantial optimization potential for transition relations when the first execution steps are applied as satisfiability don't-cares. This result suggests that current designs include circuitry that is only used during the first few clock periods after reset and could be discarded or disabled after startup. In this paper we describe how temporal decomposition could be applied to treat the logic for startup separately from the remaining circuitry and discuss multiple alternatives to exploit this for an improved implementation.

Physical design EDA research in academia has historically been based on infrastructure developed independently by individual contributors. This has led to fragmentation in the community, where interaction, data interchange and comparison of results between tools are difficult. We discuss our early experience with the OpenAccess Gear system, an open source software initiative intended to provide pieces of the critical integration and analysis infrastructure that are taken for granted in proprietary tools, but often wholly absent in research tools. Built on top of the widely available OpenAccess database, OA Gear provides components such as industrial-strength static timing analysis and extensible layout and netlist visualization. We discuss preliminary results from two on-going research efforts that have adopted OA Gear as their infrastructure: retrofitting the University of Michigan Capo placer into this environment, and the addition of a timing-driven capability to the Carnegie Mellon Warp placer.

Linear pseudo-Boolean (LPB) constraints denote inequalities between arithmetic sums of weighted Boolean functions and provide a significant extension of the modeling power of purely propositional constraints. They can be used to compactly describe many discrete electronic design automation problems with constraints on linearly combined, weighted Boolean variables, yet also offer efficient search strategies for proving or disproving whether a satisfying solution exists. Furthermore, corresponding decision procedures can easily be extended for minimizing or maximizing an LPB objective function, thus providing a core optimization method for many problems in logic and physical synthesis. In this paper, we review how recent advances in satisfiability search can be extended for pseudo-Boolean constraints and describe a new LPB solver that is based on generalized constraint propagation and conflict-based learning. We present a comparison with other, state-of-the-art LPB solvers which demonstrates the overall efficiency of our method.

Bounded model checking (BMC) has gained widespread industrial use due to its relative scalability. Its exhaustiveness over all valid input vectors allows it to expose arbitrarily complex design flaws. However, BMC is limited to analyzing only a specific time window, hence will only expose those flaws which manifest within that window and thus connect readily prove correctness. The diameter of a design has thus become an important concept - a bounded check of depth equal to the diameter constitutes a complete proof. While the diameter of a design may be exponential in the number of its state elements, in practice it often ranges from tens to a few hundred regardless of design size. Therefore, a powerful diameter overapproximation technique may enable automatic proofs that otherwise would be infeasible. Unfortunately, exact diameter calculation requires exponential resources, and overapproximation techniques may yield exponentially loose bounds. In this paper, we provide a general approach for enabling the use of structural transformations, such as redundancy removal, retiming, and target enlargement, to tighten the bounds obtained by arbitrary diameter approximation techniques. Numerous experiments demonstrate that this approach may significantly increase the set of designs for which practically useful diameter bounds may be obtained.

Traditional timing-driven placement considers only combinational delays and does not take into account the potential of subsequent sequential optimization steps. As a result, the potential of re-balancing path delays through post-placement applications of clock skew scheduling and in-place retiming cannot be fully realized. In this paper we describe a new placement algorithm that is based on a tight integration of sequential timing analysis in the inner loop of an analytic solver. Instead of minimizing the maximum path delay, our approach minimizes the maximum mean delay on any circuit loop, thus enabling the full optimization potential of clock skew scheduling and in-place retiming. We present two versions of the new algorithm: one approximates sequential criticality and weights wires accordingly (Cong and Lim, 2000), the other extends this with the inclusion of explicit wire-length constraints for loops that limit the final clock period. Our algorithms are implemented using a hybrid, GORDlAN-style sequence of analytical placement steps interleaved with cell partitioning (Kleinhans et al., 1988). Our experiments on a set of large industrial designs demonstrate that the presented placement algorithm can minimize the contribution of interconnection delays to the clock period on average by 23.5% compared to a solution based on combinational delays.

Bounded model checking (BMC) is an incomplete property checking method that is based on a finite unfolding of the transition relation to disprove the correctness of a set of properties or to prove them for a limited execution length from the initial states. Current BMC techniques repeatedly concatenate the original transition relation to unfold the circuit with increasing depths. In this paper we present a method that is based on a dual unfolding scheme. The first unfolding is non-initialized and progressively simplifies concatenated frames of the transition relation. The tail of the simplified frames is then applied in the second unfolding, which starts from the initial state and checks the properties. We use a circuit graph representation for all functions and perform simplification by merging vertices that are functionally equivalent under given input constraints. In the noninitialized unfolding, previous time frames progressively tighten these constraints thus leading to an asymptotic simplification of the transition relation. As a side benefit, our method can find inductive invariants constructively by detecting when vertices are functionally equivalent across time frames. This information is then used to further simplify the transition relation and, in some cases, prove unbounded correctness of properties. Our experiments using industrial property checking problems demonstrate that the presented method significantly improves the efficiency of BMC.

In this paper, we discuss the application of circuit-based logical reasoning to simplify optimization problems expressed as integer linear programs (ILP) over circuit states. We demonstrate that a targeted restructuring of the problem formulation based on the circuit topology can significantly improve the performance and capacity of the overall optimization procedure. We further review two distinct application classes, one requiring a feasible, the other an infeasible bound of an ILP solution that cannot be computed optimally within resource limits and present algorithmic approaches to handle them. We use the problems of computing a minimal leakage state and finding the state transition with maximal peak current to exemplify these two unique classes and present results comparing our methods with alternative techniques.

Linear Pseudo-Boolean (LPB) constraints denote inequalities between arithmetic sums of weighted Boolean functions and provide a significant extension of the modeling power of purely propositional constraints. They can be used to compactly describe many discrete EDA problems with constraints on linearly combined, parameterized weights, yet also offer efficient search strategies for proving or disproving whether a satisfying solution exists. Furthermore, corresponding decision procedures can easily be extended for minimizing or maximizing an LPB objective function, thus providing a core optimization method for many problems in logic and physical synthesis. In this paper we review how recent advances in satisfiability (SAT) search can be extended for pseudo-Boolean constraints and describe a new LPB solver that is based on generalized constraint propagation and conflict-based learning.

Functional symmetries provide significant benefits for multiple tasks in synthesis and verification. Many applications require the manual specification of symmetries using special language features such as symmetric data types. Methods for automatically detecting symmetries are based on functional analysis, e.g. using BDDs, or structural methods. The latter search for circuit graph automorphisms which imply functional symmetry. We present a method for finding symmetries of Boolean functions based on a two-step approach. First, the circuit structure is modified to maximize its structural regularity and thus the number of inherent automorphisms. The next step implements a fast algorithm for detecting the automorphism generators of the circuit graph. The generators provide a compact representation of all automorphisms, which in turn encode a subset of the functional symmetries. Because of its pure structural nature, our approach avoids the complexity issues inherent to methods using BDDs, yet it still works automatically and independently from the input specification format. However, the described method may not detect all functional symmetries, however, our experiments demonstrate that it can find the majority of the symmetries present in practical circuits.

Many tasks in computer-aided design (CAD), such as equivalence checking, property checking, logic synthesis, and false paths analysis, require efficient Boolean reasoning for problems derived from circuits. Traditionally, canonical representations, e.g., binary decision diagrams (BDDs), or structural satisfiability (SAT) methods, are used to solve different problem instances. Each of these techniques offer specific strengths that make them efficient for particular problem structures. However, neither structural techniques based on SAT, nor functional methods using BDDs offer an overall robust reasoning mechanism that works reliably for a broad set of applications. The authors present a combination of techniques for Boolean reasoning based on BDDs, structural transformations, an SAT procedure, and random simulation natively working on a shared graph representation of the problem. The described intertwined integration of the four techniques results in a powerful summation of their orthogonal strengths. The presented reasoning technique was mainly developed for formal equivalence checking and property verification but can equally be used in other CAD applications. The authors' experiments demonstrate the effectiveness of the approach for a broad set of applications.

Many tasks in CAD, such as equivalence checking, property checking, logic synthesis, and false paths analysis require efficient Boolean reasoning for problems derived from circuit structures. Traditionally, canonical representations, e. g., BDDs, or SAT- based search methods are used to solve a particular class of problems. In this paper we present a combination of techniques for Boolean reasoning based on BDDs, structural transformations, and a SAT procedure natively working on a shared graph representation of the problem. The described intertwined integration of the three techniques results in a robust summation of their orthogonal strengths. Our experiments demonstrate the effectiveness of the approach.

In this paper, we present two techniques for improving min-area retiming that combine the actual register minimization with combinational optimization. First, we discuss an on-the-fly retiming approach based on a sequential AND/inverter/register graph. With this method, the circuit structure is sequentially compacted using a combination of register "dragging" and AND vertex hashing. Second, we present an extension of the classical retiming formulation that allows an optimal sharing of fan-in registers of AND clusters, similar to traditional fan-out register sharing. The combination of both techniques is capable of minimizing the circuit size beyond that possible with a standard Leiserson and Saxe retiming approach on a static netlist structure. Our work is primarily aimed at optimizing the performance of reachability-based verification methods. However, the presented techniques are equally applicable to sequential redundancy removal in technology-independent logic synthesis. A large set of experiments using benchmark and industrial circuits demonstrate the effectiveness of the described techniques.

SPFDs are a mechanism to express flexibility in Boolean networks. Introduced by Yamashita et al. in the context of FPGA synthesis [1996], they were extended later to general combinational networks. We introduce the concept of sequential SPFDs and provide an algorithm to compute them based on a partition of the state bits. The SPFDs, of each component in the partition are used to generate equivalence classes of states. We provide a formal relation between the resulting state classification and the equivalence classes produced by classical state minimization of completely specified machines. The SPFDs, associated with the state bits can be applied for re-encoding the state space. For this, we give an algorithm to re-synthesize the sequential circuit using sequential SPFDs and the new state re-encoding.

This paper presents a verification technique for functional comparison of large combinational circuits using a novel combination of known approaches. The idea is based on a tight integration of a structural satisfiability (SAT) solver, BDD sweeping, and random simulation; all three working on a shared graph representation of the circuit. The BDD sweeping and SAT solver are applied in an inter-twined manner both controlled by resource limits that are successively increased during each iteration. In this cooperative setting the BDD sweeping incrementally reduces the search space for the SAT solver until the problem is solved or the resource limits are exhausted. This approach improves on previous work in several ways: The integral application of the SAT solver significantly enhances the capacity and efficiency of BDD sweeping and extends its suitability for miscomparing designs. Further, the random simulation algorithm works on the compressed circuit graph and thus runs more efficiently. Our experiments demonstrate that the outlined approach is effective for a large class of equivalence checking instances by automatically adapting to the difficulty of the problem.

We introduce Simulation Verification with Augmentation (SIVA), a tool for checking safety properties on digital hardware designs.SIVA integrates simulation with symbolic techniques for vector generation.Specifically, the core algorithm uses a combination of ATPG and BDDs to generate input vectors which cover behavior not excited by simulation.Experimental results demonstrate considerable improvement in state space coverage compared with either simulation or formal verification in isolation.

This paper describes a probabilistic approach to state space search. The presented method applies a ranking of the design states according to their probability of reaching a given target state based on a random walk model. This ranking can be used to prioritize an explicit or partial symbolic state exploration to find a trajectory from a set of initial states to a set of target states. A symbolic technique for estimating the reachability probability is described which implements a smooth trade-off between accuracy and computing effort. The presented probabilistic state space search complements incomplete verification methods which are specialized in finding errors in large designs.

This paper presents a verification technique which isspecifically targeted to formally comparing large combinational circuits with some structural similarities. The approach combines the application of BDDs withcircuit graph hashing, automatic insertion of multiple cut frontiers, and a controlled elimination of false negative verification results caused by the cuts. Twoideas fundamentally distinguish the presented technique from previous approaches. First, originating from the cut frontiers, multiple BDDs are computedfor the internal nets of the circuit, and second, theBDD propagation is prioritized by size and discontinued once a given limit is exceeded.

In this paper we present the application of random simulation in formal verification of functional equivalence of hardware designs. We demonstrate that random simulation can effectively complement BDD-based verification approaches in three areas: (1) quick generation of counter example pattern for miscomparing designs, (2) exhaustive comparison of small functions, and (3) providing meaningful signatures for design partitioning based on functionally equivalent cut-points. The presentation describes a smooth and efficient integration of a simulation algorithm into a general verification framework. In this framework the simulator can be applied as one of various engines for Boolean reasoning the outcome of which might be undecided.

This paper describes a diagnosis technique for locating design errors in circuit implementations which do not match their functional speci cation.The method eciently propagates mismatched p atterns from erroneous outputs backward into the network and calculates circuit regions which most likely contain the error(s).In contrast to previous approaches, the described t e chnique does not depend on a xed set of error models.Therefore, it is more general and especially suitable for transistor-level circuits, which have a broader variety of possible design errors than gate-level implementations.Furthermore, the proposed method is also applicable for incomplete sets of mismatched p atterns and hence c an be used not only as a debugging aid for formal veri cation techniques but also for simulationbased approaches.Experiments with industrial CMOS circuits show that for most design errors the identi ed problem region is less than 3% of the overall circuit.

Systems for multi-level logic optimization are usually based on a set of specialized, loosely-related transformations which work on a network representation. The sequence of transformations in a synthesis scenario (script) is crucial for the performance of the whole system. This paper presents the application of a genetic algorithm for automatic tuning of scenarios, and therefore an approach for optimizing the synthesis process itself. We introduce a general context-free grammar to describe the set of relevant scenarios. For such grammars, we develop meaningful genetic operators for the implementation of an evolutionary search. Experiments with an industrial logic synthesis system show that our method can improve the efficiency of manually designed standard scenarios by an average of 8%. We also show that this approach can effectively tune scenarios to particular design styles and/or specific synthesis goals.>

High-level synthesis has been an active research field since the early eighties. However, apart from a few exceptions the technology has so far failed to make a smooth transition into the industrial environment. The main reasons are related more to the lack of an integrated methodology, including design entry, simulation, and synthesis, than to the quality of the synthesis algorithms. Experiences in applying the HIS system (High-level IBM Synthesis System) to real designs led to the development of a system and methodology which integrate language modeling, simulation, high-level, and logic synthesis. This paper presents the main concepts behind this system, namely, its modeling, synthesis, and simulation capabilities. Moreover, it addresses some of the problems encountered when transferring high-level synthesis to a production environment.>

A comprehensive timing model for behavioral-level specifications and algorithms for timing analysis in high-level synthesis is described. It is based on a timing network which models the data flow as well as the control flow in the behavioral input specification. The delay values for the network modules are created by invoking the same logic synthesis procedure applied after behavioral synthesis. The timing network is built only once for a given behavioral description. Several parameters are used to explore different scheduling possibilities as well as different optimization modes (area, delay), without changing the network. The use of the timing model in conjunction with a path-based scheduling algorithm is presented. Results for several benchmarks attested to the accuracy of this approach.>

A method and algorithms for exploring the design space between the register-transfer and behavioral levels are presented. The method consists of the specification of a high-level state machine, which combines the advantages of a specific control structure, by means of states and transitions, with the flexibility of behavioral descriptions inside each high-level state. High-level synthesis techniques are used for synthesizing this machine. As a result, the user has control over the final controller implementation and is able to perform high-level tradeoffs between control and data path.>