waashk/dblp huggingface dataset:
dynamic transition relation simplification for bounded property checking. 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.
heterogeneous built-in resiliency of application specific programmable processors. using the flexibility provided by multiple functionalities we have developed a new approach for permanent fault-tolerance: heterogeneous built-in-resiliency (hbir). hbir processor synthesis imposes several unique tasks on the synthesis process: (i) latency determination targeting k-unit fault-tolerance, (ii) application-to-faulty-unit matching and (iii) hbir scheduling and assignment algorithms. we address each of them and demonstrate the effectiveness of the overall approach, the synthesis algorithms, and software implementations on a number of designs.
timing analysis in high-level synthesis. 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
micro-preemption synthesis: an enabling mechanism for multi-task vlsi systems. task preemption is a critical enabling mechanism in multi-task vlsi systems. on preemption, data in the register files must be preserved in order for the task to be resumed. this entails extra memory to preserve the context and additional clock cycles to save and restore the context. in this paper, we present techniques and algorithms to incorporate micro-preemption constraints during multi-task vlsi system synthesis. specifically, we have developed: (i) algorithms to insert and refine preemption points in scheduled task graphs subject to preemption latency constraints. (ii) techniques to minimize the context switch overhead by considering the dedicated registers required to save the state of a task on preemption and the shared registers required to save the remaining values in the tasks. (iii) a controller based scheme to preclude preemption related performance degradation. the effectiveness of all approaches, algorithms, and software implementations is demonstrated on real examples.
timing-safe false path removal for combinational modules. a combinational module is a combinational circuit that can be used under any arrival time condition at the primary inputs. an intellectual property (ip) module, if combinational, is one such example. the false-path-aware delay characterization of a combinational module without disclosing its internal structural detail is crucial for accurate timing analysis of ip-based designs.this paper addresses three related issues on delay characterization of combinational modules. we first introduce a new notion called timing-safe replaceability as a way of comparing the timing characteristics of two combinational modules formally. this notion allows us to determine whether a new module is a safe replacement of an original module under any surrounding environment with respect to timing. second, we consider false path detection of combinational modules. although false path detection is essential in accurate delay modeling, we argue that the conventional definition of false paths such as floating mode analysis is not appropriate for defining the falsity of a path for a combinational module since the falsity is relative to an arrival time condition. a new definition of false paths, termed strongly false paths, is introduced to resolve this issue. strongly false paths are those paths that are guaranteed to be false under any arrival time condition, and thus uniquely defined independent of arrival time conditions. finally, we propose a new algorithm that removes strongly false paths from a combinational module by a circuit transformation. we prove that the resulting circuit is a timing-safe replacement of the original.
implication graph based domino logic synthesis. in this paper, we present a new approach to the problem of inverter elimination in domino logic synthesis. a small piece of static cmos logic is introduced to the circuit to avoid significant area penalty resulting from duplication. to maximize the domino logic part and to minimize the static cmos logic part, a generalized atpg based logic transformation is proposed to eliminate or relocate a target inverter. based on the new concept of dominating set of mandatory assignment (dsma) and the corresponding implication graph, we propose algorithms to identify a minimum candidate set for a target inverter. experimental results show that logic transformation based on implication graph can reduce transistor counts by 25% and power delay product by 25% on average.
probabilistic state space search. 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.
techniques for improving the accuracy of geometric-programming based analog circuit design optimization. we present techniques for improving the accuracy of geometric-programming (gp) based analog circuit design optimization. we describe major sources of discrepancies between the results from optimization and simulation, and propose several methods to reduce the error. device modeling based on convex piecewise-linear (pwl) function fitting is introduced to create accurate active and passive device models. we also show that in selected cases gp can enable nonconvex constraints such as bias constraints using monotonicity, which help reduce the error. lastly, we suggest a simple method to take the modeling error into account in gp optimization, which results in a robust design over the inherent errors in gp device models. two-stage operational amplifier and on-chip spiral inductor designs are given as examples to demonstrate the presented ideas.
rectification method for lookup-table type fpga's. a method to rectify lookup-table-type field-programmable gate array (fpga) designs is presented. instead of changing the netlist, only the functionality realized by lookup tables in a chip is modified and the netlist is retained so that there is no change in the delay of the chip. the problem is formalized using characteristic functions, and a redesign technique based on boolean relations is presented
a redesign technique for combinational circuits based on gate reconnections. in this paper, we consider a redesign technique applicable to combinational circuits implemented with gate-array or standard-cell technology, where we rectify an existing circuit only by reconnecting gates on the circuit with all the gate types unchanged. this constraint allows us to reuse the original placement as is, thereby speeding up the total time needed for a redesign. we formulate this problem as a boolean-constraint problem and give a bdd-based algorithm to check the feasibility of redesign.
fast test application technique without fast scan clocks. built-in self-test (bist) schemes need to set the state of the circuit under test (cut) for each test vector applied. the two primary techniques by which the state is set are test-per-scan and test-per-clock. in a test-per-scan scheme, circuit states are set using one or more scan chains. several scan cycles are required to apply a single test vector. in very large circuits, the time to apply each test vector may be quite high. the direct option of reducing test time with a fast scan clock is difficult to realize in practice. in a test-per-clock scheme, all circuit flip-flops are loaded in parallel. a new test vector can be applied in each cycle. the area overhead incurred in accessing each storage element directly is quite significant. we propose a new broadcast bist (b2ist) scheme as a compromise between the two approaches. b2ist uses time-division multiplexing (tdm) to load multiple storage elements in a broadcast group in a single clock cycle, but through only a single scan data input. based on our b2ist simulation, we compare the layout overhead and performance of b2ist with that of traditional bist schemes on iscas benchmark circuits. thus, b2ist can achieve the performance of a test-per-clock scheme, but only incur the overhead of a test-per-scan scheme.
approximate timing analysis of combinational circuits under the xbd0 model. this paper is concerned with approximate delay computation algorithms for combinational circuits. as a result of intensive research in the early 90's efficient tools exist which can analyze circuits of thousands of gates in a few minutes or even in seconds for many cases. however, the computation time of these tools is not so predictable since the internal engine of the analysis is either a sat solver or a modified atpg algorithm, both of which are just heuristic algorithms for an np-complete problem. although they are highly tuned for cad applications, there exists a class of problem instances which exhibits the worst-case exponential cpu time behavior. in the context of timing analysis, circuits with a high amount of reconvergence, e.g. c6288 of the iscas benchmark suite, are known to be difficult to analyze under sophisticated delay models even with state-of-the-art techniques. for example [mcgeer93] could not complete the analysis of c6288 under the mapped delay model. to make timing analysis of such corner case circuits feasible we propose an approximate computation scheme to the timing analysis problem as an extension to the exact analysis method proposed in [mcgeer93]. sensitization conditions are conservatively approximated in a selective fashion so that the size of sat problems solved during analysis is controlled. experimental results show that the approximation technique is effective in reducing the total analysis time without losing accuracy for the case where the exact approach takes much time or cannot complete.
folding of logic functions and its application to look up table compaction. the paper describes the folding method of logic functions to reduce the size of memories for keeping the functions. the folding is based on the relation of fractions of logic functions. we show that the fractions of the full adder function have the bit-wise not relation and the bit-wise or relation, and that the memory size becomes half (8-bit). we propose a new 3--1 lut with the folding mechanisms whcih can implement a full adder with one lut. a fast carry propagation line is introduced for a multi-bit addition. the folding and fast carry propagation mechanisms are shown to be useful to implement other multi-bit operations and general 4 input functions without extra hardware resources. the paper shows the reduction of the area consumption when using our luts compared to the case using 4--1 luts on several benchmark circuits.
precise timing verification of logic circuits under combined delay model. a combined delay model to manipulate the variance of the delay time of logic elements and a timing verification method based on the theory of regular expressions are presented. emphasis is placed on the hazard detection problem and the verification of asynchronous circuits. the effectiveness of the method with medium sized circuits including about 100 elements is shown
atpg for noise-induced switch failures in domino logic. domino circuits have been used in most modern high-performance microprocessordesigns because of their high speed, low transistor-count andhazard-free operation. however, with technology scaling, domino circuitsare increasingly susceptible to switch failures due to various noise sourcesthat include crosstalk, charge sharing and leakage. to test for such failuresin a manufactured chip, we describe a test pattern generation methodologythat generates specific test patterns to target such failures. these testpatterns activate noise from multiple sources such that their combined effectcauses a switch failure at a domino gate output. in addition, the testpatterns propagate the resulting error to an observable output within theduration of the circuit's clock cycle. the methodology has been implementedand validated using a domino multiplier circuit.
finfets for nanoscale cmos digital integrated circuits. suppression of leakage current and reduction in device-to-device variability are key challenges for sub-45nm cmos technologies. nonclassical transistor structures such as the finfet are likely necessary to meet transistor performance requirements in the sub-20nm gate length regime. this paper presents an overview of finfet technology and describes how it can be used to improve the performance, standby power consumption, and variability in nanoscale-cmos digital ics.
a scheduling method by stepwise expansion in high-level synthesis. a fast heuristic method for the scheduling problem that minimizes hardware costs of functional units, registers, and buses on the basis of an integer linear programming (ilp) model is proposed. in the method, the total computation time can be greatly reduced compared to the general ilp method, since the number of the integer variables which appear in the ilp formulation is reduced by introducing a stepwise expansion approach. results obtained for a practical scheduling problem indicate that the computation time of the proposed method is linear to the number of the control steps, and optimal or near-optimal solutions can be found
a zero-skew clock routing scheme for vlsi circuits. a clock routing scheme that guarantees a zero-skew routing result is proposed. it is shown that the time complexity for the algorithm can be reduced to o(n2 log n) by using the modified voronoi diagram to structure the algorithm. l-shaped pairing and h-flipping operations are introduced to further reduce the clock wire length. extensions are made to the algorithm for use in building-block layout and zero skew is also achieved. significant reduction in total clock wire lengths is observed
techniques for crosstalk avoidance in the physical design of high-performance digital systems. interconnect performance does not scale well into deep submicron dimensions, and the rising number of analog effects erodes the digital abstraction necessary for high levels of integration. in particular, crosstalk is an analog phenomenon of increasing relevance. to cope with the increasingly analog nature of high-performance digital system design, we propose using a constraint-driven methodology. in this paper we describe new constraint generation ideas incorporating digital sensitivity. in constraint-driven synthesis, we show that a fundamental subproblem of crosstalk channel routing, coupling-constrained graph levelization (ccl), is np-complete, and develop a novel heuristic algorithm. to demonstrate the viability of our methodology, we introduce a gridless crosstalk-avoiding channel router as an example of a robust and truly constraint-driven synthesis tool.
driving toward higher iddq test quality for sequential circuits: a generalized fault model and its atpg. we propose a generalized stuck-at fault model for sequential circuits under the selective iddq test strategy. the proposed fault model makes a pessimistic assumption on the boolean fault effects when the fault is activated. we show that by using the proposed fault model, test sequences of higher quality can be generated and/or selected. we further propose a test vector generation and selection method for this fault model. we present results to illustrate that a high fault coverage for the proposed fault model can be achieved by a small test set under the selective iddq test environment.
efficient harmonic balance simulation using multi-level frequency decomposition. efficient harmonic balance (hb) simulation provides a useful tool for the design of rf and microwave integrated circuits. for practical circuits that can contain strong nonlinearities, however, hb problems cannot be solved reliably or efficiently using conventional techniques. various preconditioning techniques have been proposed to facilitate a robust and efficient analysis based on krylov subspace linear solvers. in this work we introduce a multi-level frequency domain preconditioner based on a hierarchical frequency decomposition approach. at each newton iteration, we recursively solve a set of smaller problems to provide an effective preconditioner for the large linearized hb problem. compared to the standard single-level block diagonal preconditioner, our experiments indicate that our approach provides a more robust, memory efficient solution while offering a 2-9/spl times/ speedup for several strongly nonlinear hb problems in our experiments.
digital sensitivity: predicting signal interaction using functional analysis. maintaining signal integrity in digital systems is becoming increasingly difficult due to the rising number of analog effects seen in deep submicron design. one such effect, the signal crosstalk problem, is now a serious design concern. signals which couple electrically may not affect system behavior because of timing or function in the digital domain. if we can isolate observable coupling effects then we can constrain layout synthesis to eliminate them. in this paper, we find that it is possible to predict signal interaction by signal functionality alone, leading to a significant amount of robust switching isolation, independent of parasitics introduced by layout or semiconductor process. we introduce techniques to predict signal interaction using functional sensitivity analysis. in general sequential networks we find that significant switching isolation can be extracted with efficient sensitivity analysis algorithms, thus giving promise to the goal of synthesizing layout free from crosstalk effects.
transistor-level timing analysis using embedded simulation. a high accuracy system for transistor-level static timing analysis is presented. accurate static timing verification requires that individual gate and interconnect delays be accurately calculated. at the sub-micron level, calculating gate and interconnect delays using delay models can result in reduced accuracy. instead, the proposed method calculates delays through numerical integration using an embedded circuit simulator. it takes into account short circuit current and carefully chooses the set of conditions that results in a tight upper bound of the worst case delay for each gate. similar repeating transistor configurations of gates in the circuit are automatically identified and a novel interpolation based caching scheme quickly computes gate delays from the delays of similar gates. a tight object code level integration with a commercial high speed transistor-level circuit simulator allows efficient invocation of the simulation.
simulation methods for rf integrated circuits. the principles employed in the development of modern rf simulators are introduced and the various techniques currently in use, or expected to be in use in the next few years, are surveyed. frequency and time domain techniques are presented and contrasted, as are steady state and envelope techniques and large and small signal techniques.
application-driven synthesis of core-based systems. we developed a new hierarchical modular approach for synthesis of area-minimal core-based data-intensive systems. the optimization approach employs a novel global least-constraining most-constrained heuristic to minimize the instruction cache misses for a given application, instruction cache size and organization. based on this performance optimization technique, we constructed a strategy to search for a minimal-area processor core, and an instruction and data cache which satisfy the performance characteristics of a set of target applications. the synthesis platform integrates the existing modeling, profiling, and simulation tools with the developed system-level synthesis tools. the effectiveness of the approach is demonstrated on a variety of modern real-life multimedia and communication applications.
hazard-non-increasing gate-level optimization algorithms. hazard-non-increasing optimization algorithms, optimizations on gate-level logic without introduction of any further static nor dynamic hazards, are presented. proofs are given for general theoretical results on hazard-non-increasing transformations which serve as the basis for these algorithms. the algorithms substantially augment the set of proven hazard-non-increasing optimization techniques in the literature. these algorithms are useful for hazard-free implementations of asynchronous designs
a quantitative approach to functional debugging. we introduce a novel cut-based debugging paradigm. it coordinates design emulation and simulation and enables fast transition from one to another. emulation or functional implementation is used for fast application execution; simulation provides complete design observability and controllability. the implementation of the new debugging approach poses several cad tasks. we formulate the optimization tasks and develop constraint-based heuristics to solve them. effectiveness of the approach is demonstrated on a set of designs.
hyhope: a fast fault simulator with efficient simulation of hypertrophic faults. in sequential circuit fault simulation, the hypertrophic faults, which result from lengthened initialization sequence in the faulty circuits, usually produce a large number of fault events during simulation and require excessive gate evaluations. these faults degrade the performance of fault simulators attempting to simulate them exactly. in this paper, an exact simulation algorithm is developed to identify the hypertropic faults and to minimize their effects during the fault simulation. the simulator hyhope based on this algorithm shows that the average speedup ratio over hope 1.1 is 1.57 for iscas89 benchmark circuits. furthermore, the result indicates the performance of hyhope is close to the approximate simulator in which faults are simply dropped when they become potentially detected.