waashk/dblp huggingface dataset:
exhaustive simulation need not require an exponential number of tests. while simulation is today the most common form of verification, one disadvantage is the excessive number of tests needed for complete coverage. however, the number of tests may be substantially reduced if test case generation is combined with a structural analysis. the resulting set of test cases for exhaustive simulation may be smaller than exponential, which might make exhaustive simulation feasible. even if the set of test cases is still too large, choosing tests from this reduced set results in better coverage than otherwise
be careful with don't cares. abstract: it is commonly expected that any correct implementation can replace its specification inside a larger design without violating the correctness of the whole design. this property (called replaceability) is automatically satisfied in the absence of don't cares because "correctness" by definition implies that specification and implementation compute the identical function. however don't cares allow an implementation to compute a different function, and thus make it difficult to ensure replaceability. whether this problem occurs depends on the exact meaning of "don't care" and the associated definition of "correctness". we will consider three meanings of "don't care" and for each give conditions under which correct implementations may replace their specifications.
incremental synthesis. a small change in the input to logic synthesis may cause a large change in the output implementation. this is undesirable if a designer has some investment in the old implementation and does not want it perturbed more than necessary. we describe a method that solves this problem by reusing gates from the old implementation, and restricting synthesis to the modified portions only.
inaccuracies in power estimation during logic synthesis. this paper studies the confidence with which power can be estimated at various levels of design abstraction. we report the results of experiments designed to identify and evaluate the sources of inaccuracies in gate-level power estimation. in particular, we are interested in power estimation during logic synthesis. factors that may invalidate or diminish the accuracy of power estimates include optimization, technology mapping, transistor sizing, placement and wiring, and choice of input stimuli.
eta: electrical-level timing analysis. a timing analyzer which performs timing analysis considering electrical-level details such as input signal slope, gate input distinction, charge sharing, and interconnect, while also taking into account such high-level concerns as path sensitization, is described. to achieve the greatest efficiency, eta operates in two phases: (1) logic and delay precharacterization, and (2) longest path analysis. during the precharacterization phase, each gate is analyzed to get its boolean function and its load at the transistor level. during the longest path analysis phase, paths from each primary input are enumerated and examined separately. each potentially longest path is tested for sensitizability at the gate level until a sensitizable longest path is found. the circuit examples given demonstrate the importance of an accurate delay calculation in correctly finding the longest statistically sensitizable path
compatible observability don't cares revisited. codcs stand for compatible observability don't cares. we first examine the definition of compatibility and when a set of codcs is compatible. we then discuss savoj's codc computation for propagating codcs from a node's output to its fanins, and show by example, that the results can depend on the current implementation of the node. then we generalize the computation so that the result is independent of the implementation at the node. the codcs propagated by this computation are proved to be maximal in some sense. local don't cares (ldcs) are codcs of a node, pre-imaged to the primary inputs and then imaged and projected to the local fanins of the node. ldcs combine codcs with sdcs (satisfiability don't cares), but only the codc part is propagated to the fanin network. another form of local don't cares, propagates both the codc and sdc parts to the fanin network. both are shown to be compatible in some sense, but conservative. we give a method for updating both kinds of local don't cares incrementally when other nodes in the network are changed.
resource sharing in hierarchical synthesis. this paper presents a new approach to hierarchical high-level synthesis with respect to internal register-transfer structures of complex components. entire subdesigns can efficiently be used as complex components at a higher hierarchical level of the design. after synthesis, the calculated schedule of each subdesign is added to its register-transfer component model. this enables the sharing of unused subcomponents across different hierarchical levels of the design. especially, subcomponents of autonomous components, with a separate controller, can also be shared. as a result, the presented methodology offers a high degree of optimization to hierarchically specified designs.
methods for true power minimization. this paper presents methods for efficient power minimization at circuit and micro-architectural levels. the potential energy savings are strongly related to the energy profile of a circuit. these savings are obtained by using gate sizing, supply voltage, and threshold voltage optimization, to minimize energy consumption subject to a delay constraint. the true power minimization is achieved when the energy reduction potentials of all tuning variables are balanced. we derive the sensitivity of energy to delay for each of the tuning variables connecting its energy saving potential to the physical properties of the circuit. this helps to develop understanding of optimization performance and identify the most efficient techniques for energy reduction. the optimizations are applied to some examples that span typical circuit topologies including inverter chains, sram decoders, and adders. at a delay of 20% larger than the minimum, energy savings of 40% to 70% are possible, indicating that achieving peak performance is expensive in terms of energy. energy savings of about 50% can be achieved without delay penalty with the balancing of sizes, supplies, and thresholds.
binary decision diagrams and beyond: enabling technologies for formal verification. ordered binary decision diagrams (obdds) have found widespread use in cad applications such as formal verification, logic synthesis, and test generation. obdds represent boolean functions in a form that is both canonical and compact for many practical cases. they can be generated and manipulated by efficient graph algorithms. researchers have found that many tasks can be expressed as series of operations on boolean functions, making them candidates for obdd-based methods. the success of obdds has inspired efforts to improve their efficiency and to expand their range of applicability. techniques have been discovered to make the representation more compact and to represent other classes of functions. this has led to improved performance on existing obdd applications, as well as enabled new classes of problems to be solved. this paper provides an overview of the state of the art in graph-based function representations. we focus on several recent advances of particular importance for formal verification and other cad applications.
verifying properties of hardware and software by predicate abstraction and model checking. this tutorial describes automatic techniques for formally verifying hardware and software by creating boolean abstractions of the underlying unbounded system state variables.
logic synthesis for large pass transistor circuits. pass transistor logic (ptl) can be a promising alternative to static cmos for deep sub-micron design. in this work, we motivate the need for cad algorithms for ptl circuit design and propose decomposed bdds as a suitable logic level representation for synthesis of ptl networks. decomposed bdds can represent large, arbitrary functions as a multi-stage circuit and can exploit the natural, efficient mapping of a bdd to ptl. a comprehensive synthesis flow based on decomposed bdds is outlined for ptl design. we show that the proposed approach allows us to make logic-level optimizations similar to the traditional multi- level network based synthesis flow for static cmos, and also makes possible optimizations with a direct impact on area, delay and power of the final circuit implementation which do not have any equivalent in the traditional approach. we also present a set of heuristical algorithms to synthesize ptl circuits optimized for area, delay and power which are key to the proposed synthesis flow. experimental results on iscas benchmark circuits show that our technique yields ptl circuits with substantial improvements over static cmos designs. in addition, to the best of our knowledge this is the first time ptl circuits have been synthesized for the entire iscas benchmark set.
adaptive methods for netlist partitioning. an algorithm that remains in use at the core of many partitioning systems is the kernighan-lin algorithm and a variant the fidducia-matheysses (fm) algorithm. to understand the fm algorithm we applied principles of data engineering where visualization and statistical analysis are used to analyze the run-time behavior. we identified two improvements to the algorithm which, without clustering or an improved heuristic function, bring the performance of the algorithm near that of more sophisticated algorithms. one improvement is based on the observation, explored empirically, that the full passes in the fm algorithm appear comparable to a stochastic local restart in the search. we motivate this observation with a discussion of recent improvements in monte carlo markov chain methods in statistics. the other improvement is based on the observation that when an fm-like algorithm is run 20 times and the best run chosen, the performance trace of the algorithm on earlier runs is useful data for learning when to abort a later run. these improvements, implemented with a simple adaptive scheme, are orthogonal to techniques used in state-of-the-art implementations, and should therefore be applicable to other vlsi optimization algorithms.
efficient boolean function matching. efficient algorithms for performing the matching step in technology mapping are proposed. the main result is an algorithm for matching under input negations that takes time polynomial in the size of the bdds representing the functions to be matched. this algorithm is the basis for efficient methods for matching under permutations, bridging and constant inputs. a simple mapper based on the algorithms was implemented and tested on a suite of combinational circuits. using the actel type 1 mother cell, the mapper required an average of 8.5% fewer cells than mispga. when integrated into a more sophisticated technology mapper, the matching algorithms could provide even better performance
mcpower: a monte carlo approach to power estimation. an alternative technique for power estimation that combines the accuracy of simulation-based techniques with the speed of the probabilistic technique is investigated. the resulting method is statistical in nature; it consists of applying randomly-generated input patterns to the circuit and monitoring, with a simulator, the resulting power value. this is continued until a value of power is obtained with a desired accuracy, at a specified confidence level. the algorithm and experimental results are presented and the superiority of this approach is discussed
optimization of critical paths in circuits with level-sensitive latches. a simple extension of the critical path method is presented which allows more accurate optimization of circuits with level-sensitive latches. the extended formulation provides a sufficient set of constraints to ensure that, when all slacks are non-negative, the corresponding circuit will be free of late signal timing problems. cycle stealing is directly permitted by the formulation. however, moderate restrictions may be necessary to ensure that the timing constraint graph is acyclic. forcing the constraint graph to be acyclic allows a broad range of existing optimization algorithms to be easily extended to better optimize circuits with level-sensitive latches. we describe the extension of two such algorithms, both of which attempt to solve the problem of selecting parts from a library to minimize area subject to a cycle time constraint.
identification of critical paths in circuits with level-sensitive latches. an approach to timing verification of circuits with level-sensitive latches which focuses on the critical paths that constrain the operating speed of these circuits is described. the timing model used has been referred to as the `smo model' (sakallah, mudge and olukotun, 1990). three types of critical paths (long, short and loops) can arise in the smo formulation; verifying their timing is sufficient to ensure correct operation. an algorithm for identifying these paths is presented, and its relationship to other approaches to solving the smo model equations is discussed. finally, results which demonstrate the algorithm on circuits from the iscas89 benchmark suite are presented
new channel segmentation model and associated routing algorithm for high performance fpgas. in the model considered, a channel is partitioned into several regions and each region consists of tracks of equal length segments, but segment length is varied uniformly across the regions. each region is allocated a certain number of tracks. the segments are arranged in a staggered fashion. in order to make optimum use of the model, a routing algorithm is developed. the key feature of the routing algorithm is the assignment of the nets to the appropriate tracks by delay computation and delay matching techniques. experimental results show that the model and the algorithm improve the longest net delay by as much as 75.16% and the average net delay by 48.28% as compared to the conventional uniformly segmented model
molecular electronics: devices, systems and tools for gigagate, gigabit chips. new electronics technologies are emerging which may carry us beyond the limits of lithographic processing down to molecular-scale feature sizes. devices and interconnects can be made from a variety of molecules and materials including bistable and switchable organic molecules, carbon nanotubes, and, single-crystal semiconductor nanowires. they can be self-assembled into organized structures and attached onto lithographic substrates. this tutorial reviews emerging molecular-scale electronics technology for cad and system designers and highlights where iccad research can help support this technology.
improved reachability analysis of large finite state machines. bdd-based symbolic traversals are the state-of-the-art technique for reachability analysis of finite state machines. they are currently limited to medium-small circuits for two reasons: peak bdd size during image computation and bdd explosion for representing state sets. starting from these limits, this paper presents an optimized traversal technique particularly oriented to the exact exploration of the state space of large machines. this is possible thanks to: 1) temporary simplification of a finite state machine by removing some of its state elements, 2) a "divide-and-conquer" approach based on state set decomposition. an effective use of secondary memory allows us to store relevant portions of bdds and to regularize access to memory, resulting in less page faults. experimental results show that this approach is particularly effective on the larger iscas'89 and iscas'89-addendum'93 circuits.
boolean constrained encoding: a new formulation and a case study. this paper provides a new, generalized approach to the problem of encoding information as vectors of binary digits. we furnish a formal definition for the boolean constrained encoding problem, and show that this definition encompasses many particular encoding problems found in vlsi design, at various description abstraction levels. our approach can capture equivalence and/or compatibility classes in the original symbol set to encode, by allowing symbols codes to be cubes of a boolean space, instead of the usual minterms. besides, we introduce a unified framework to represent encoding constraints which is more general than previous efforts. the framework is based upon a new definition of the pseudo-dichotomy concept, and is adequate to guide the solution of encoding problems through the satisfaction of constraints extracted from the original problem statement. an encoding problem case study is presented, the state assignment of synchronous finite state machines with the simultaneous consideration of state minimization. the practical comparison with well-established approaches to solve this problem in two separate steps, shows that our solution is competitive with other published results. however, the case study is primarily intended to show the feasibility of the boolean constrained encoding problem formulation.
timing verification of sequential domino circuits. two methods are presented for static timing verification of sequential circuits implemented as a mix of static and domino logic. constraints for proper operation of domino gates are derived. an important observation is that input signals to domino gates may start changing near the end of the evaluate phase. the first method models domino gates explicitly, similar to latches. the second method treats domino gates only during pre- and post-processing steps. this method is shown to be more conservative, but easier to compute.
synthesis using sequential functional modules (sfms). this paper presents a new method used in our rtl-synthesis tool to perform technology mapping with sequential functional modules (sfms) such as counters, accumulators, shift-registers, or rotators from any target or macro library. if the library contains sfms, the method automatically recognizes them. if an rtl design contains patterns that can be implemented on sfms, the method maps them to the sfms found in the target library. this mapping reduces the design time by leveraging the library developer' s effort, leads to more regular and often smaller and faster designs, and helps to reduce timing and routing problems at later stages of the design process.
sequential redundancy identification using recursive learning. a sequential redundancy identification procedure is presented. based on uncontrollability analysis and recursive learning techniques, this procedure identifies c-cycle redundancies in large circuits, without simplifying assumptions or state transition information. the proposed procedure can identify redundant faults which require conflicting assignments on multiple lines. in this sense, it is a generalization of fires, a state-of-the-art redundancy identification algorithm. a modification of the proposed procedure is also presented for identifying untestable faults. experimental results on iscas benchmarks demonstrate that these two procedures can efficiently identify a large portion of c-cycle redundant and untestable faults.
non-linear quantification scheduling in image computation. computing the set of states reachable in one step from a given set of states, i.e. image computation, is a crucial step in several symbolic verification algorithms, including model checking and reachability analysis. so far, the best methods for quantification scheduling in image computation, with a conjunctively partitioned transition relation, have been restricted to a linear schedule. this results in a loss of flexibility during image computation. we view image computation as a problem of constructing an optimal parse tree for the image set. the optimality of a parse tree is defined by the largest bdd that is encountered during the computation of the tree. we present dynamic and static versions of a new algorithm, varscore, which exploits the flexibility offered by the parse tree approach to the image computation. we show by extensive experimentation that our techniques outperform the best known techniques so far.
switch-factor based loop rlc modeling for efficient timing analysis. timing uncertainty caused by inductive and capacitivecoupling is one of the major bottlenecks in timing analysis. in thispaper, we propose an effective loop rlc modeling technique toefficiently decouple lines with both inductive and capacitivecoupling. we generalize the rlc decoupling problem based ontransmission line theory and a switch-factor, which is the voltageratio between two nets. this switch-factor is also known as themiller factor and is widely used to model capacitive coupling.the proposed modeling technique can be directly applied to partialrlc netlists extracted using existing parasitic extraction toolswithout advance knowledge of the return path. the new modelaccurately captures the impact of neighboring switching activitywhen it significantly affects the size of current return loop. asdemonstrated in our experiments, the new model accuratelypredicts both upper and lower delay bounds as a function ofneighboring switching patterns. therefore, this approach can beeasily implemented into existing timing analysis flows such asmax-timing and min-timing analysis. finally, we apply the newmodeling approach to a range of activities across the designprocess including timing optimization, static timing analysis, highfrequency clock design, and data-bus wire planning.
a methodology for correct-by-construction latency insensitive design. in deep sub-micron (dsm) designs, performance will depend critically on the latency of long wires. we propose a new synthesis methodology for synchronous systems that makes the design functionally insensitive to the latency of long wires. given a synchronous specification of a design, we generate a functionaly equivalent synchronous implementation that can tolerate arbitrary communication latency between latches. by using latches we can break a long wire in short segments which can be traversed while meeting a single clock cycle constraint. the overall goal is to obtain a design that is robust with respect to delays of long wires, in a shorter time by reducing the multiple iterations between logical and physical design, and with performance that is optimized with respect to the speed of the single components of the design. in this paper we describe the details of the proposed methodology as well as report on the latency insensitive design of pdlx, an out-of-order microprocessor with speculative-execution.
acv: an arithmetic circuit verifier. based on a hierarchical verification methodology, we present an arithmetic circuit verifier acv, in which circuits expressed in a hardware description language, also called acv, are symbolically verified using binary decision diagrams for boolean functions and multiplicative binary moment diagrams (*bmds) for word-level functions. a circuit is described in acv as a hierarchy of modules. each module has a structural definition as an interconnection of logic gates and other modules. modules may also have functional descriptions, declaring the numeric encodings of the inputs and outputs, as well as specifying their functionality in terms of arithmetic expressions. verification then proceeds recursively, proving that each module in the hierarchy having a functional description, including the top-level one, realizes its specification. the language and the verifier contain additional enhancements for overcoming some of the difficulties in applying *bmd-based verification to circuits computing functions such as division and square root. acv has successfully verified a number of circuits, implementing such functions as multiplication, division, and square root, with word sizes up to 256 bits.