waashk/dblp huggingface dataset:
complementary use of runtime validation and model checking. the increasing gap between design complexity and compute power for verification necessitates radically new solutions to meet the verification challenges for future generations of hardware designs. increasingly it will not be possible to completely validate hardware prior to fabrication. we will need to reconcile ourselves to the fact that hardware, like software, will be shipped with bugs. however, this can be acceptable with appropriate mechanisms for runtime validation that detect bugs and recover from them when needed. this paper takes a significant step in examining runtime validation as part of the verification methodology. it examines the strengths and weaknesses of runtime validation and how it may be used to complement model checking in a hybrid methodology. we consider the use of on-chip hardware for detecting bugs using hardware assertions. these assertions may be used for validating abstractions and assumptions for use in offline model checking. hardware based assertions monitor properties at runtime and do not suffer from the state explosion problem. offline model checking is used to validate globally distributed properties where runtime error detection has limitations in monitoring and responding to signals separated by many clock cycles. in this case the hardware based runtime validated abstractions and assumptions help in reducing the state space for model checking. our ideas are demonstrated on a highly concurrent, yet simple to understand token sharing protocol, as well as a fairly complex cache coherence system.
analysis of substrate thermal gradient effects on optimal buffer insertion. this paper studies the effects of the substrate thermal gradients on the buffer insertion techniques. using a non-uniform temperature-dependent distributed rc interconnect delay model, the buffer insertion problem is analyzed and design guidelines are provided to ensure the near-optimality of the signal performance in the presence of the thermal gradients. in addition, the effect of temperature-dependent driver resistance on the buffer insertion is studied. experimental results show that neglecting thermal gradients in the substrate and the interconnect lines can result in non-optimal solutions when using standard buffer insertion techniques and that these effects intensify with technology scaling.
shilpa: a high-level synthesis system for self-timed circuits. shilpa is a system for the high-level synthesis of self-timed circuits. it takes behavioral descriptions in a process+functional language called hopcp and produces a netlist for the actel field-programmable gate array (fpga), supported by the viewlogic tools. hopcp descriptions are initially translated into an intermediate form based on hypergraphs called hfgs. shilpa then applies action refinement, which is a technique for transforming hfgs into asynchronous hardware by a series of graph-based transformation rules. action refinement is characterized by incremental resource allocation and control decomposition. the major contributions of the proposed work are given
hierarchical interconnect circuit models. the increasing size of integrated systems combined with deep submicron physical modeling details creates an explosion in rlc interconnect modeling complexity of unmanageable proportions. interconnect extraction tools employ hierarchy to manage complexity, but this hierarchy is discarded via eliminating far away coupling terms when the equivalent rlc circuits are formed. the increasing dominance of capacitance coupling along with the emergence of on-chip inductance, however, makes the composite effect of far-away couplings increasingly evident. even if newly enforced design rules and practices will ultimately obviate the need for modeling these couplings for design verification, some approximation of the "exact" solution is required to validate these rules. this paper proposes an efficient hierarchical equivalent circuit representation of interconnect parasitics that utilizes the efficient hierarchical long-distance modeling already existing within extractors. results from a prototype simulator based on these hierarchical models demonstrates the simulation inaccuracy incurred when the far-away coupling terms are ignored. such a form of interconnect modeling may provide the key to hierarchical modeling of electro-magnetic interactions between large components on future gigascale systems.
caliber: a software pipelining algorithm for clustered embedded vliw processors. in this paper we describe a software pipelining framework, caliber (cluster aware load balancing retiming algorithm), suitable for compilers targeting clustered embedded vliw processors. caliber can be effectively used by embedded system designers to explore different code optimization alternatives, i.e., can assist the generation of high-quality customized retiming solutions for desired program memory size and throughput requirements, while minimizing register pressure. an extensive set of experimental results is presented, considering several representative benchmark loop kernels and a wide variety of clustered datapath configurations, demonstrating that our algorithm compares favorably with one of the best state-of-the-art algorithms, achieving up to 50% improvement in performance and up to 47% improvement in register requirements.
electromagnetic parasitic extraction via a multipole method with hierarchical refinement. the increasing interconnect density and operating frequencies of system-on-a-chip (soc) designs necessitates extraction of parasitic electromagnetic couplings beyond the localized confines of functional design blocks. in addition, soc design styles and gridless variable-width routing make it increasingly difficult to use precharacterized library shapes for parasitic extraction. a comprehensive capacitance and inductance extraction solution requires a hierarchical data representation and fast runtime algorithms. we illustrate through examples that both the multipole method and hierarchical refinement, which are the two most successful approaches for parasitic extraction to date, work efficiently only under certain, limiting conditions. to improve this situation we present an approach which combines the best of both methods into a concurrent multipole refinement representation of the electromagnetic interaction which is efficient for arbitrary interconnect configurations. we use a generalized formulation of electromagnetic interactions to exploit the similarities in capacitance and inductance extraction for greater efficiency.
design verification via simulation and automatic test pattern generation. we present a simulation-based method for combinational design verification that aims at complete coverage of specified design errors using conventional atpg tools. the error models used in prior research are examined and reduced to four types: gate substitution errors (gses), gate count errors (gces), input count errors (ices), and wrong input errors (wies). conditions are derived for a gate to be completely testable for gses; these conditions lead to small test sets for gses. near-minimal test sets are also derived for gces. we analyze redundancy in design errors and relate this to single stuck-line (ssl) redundancy. we show how to map all the foregoing error types into ssl faults, and describe an extensive set of experiments to evaluate the proposed method. our experiments demonstrate that high coverage of the modeled design errors can be achieved with small test sets.
pessimism reduction in crosstalk noise aware sta. high performance circuits are facing increasingly severe signal integrity problems due to crosstalk noise and crosstalk noise awareness has become an integral part of static timing analysis (sta). existing crosstalk noise aware sta methods compute noise induced delay uncertainty on a net by net basis and in a pessimistic way, without considering the overlap bounds of the victim and aggressor timing windows and realistic delay impact on early and late signal arrival times. since crosstalk induced delay on individual nets contribute cumulatively on data and clock paths, even small amounts of pessimism in computation can add up to produce several unrealistic timing violations. unlike glitch noise analysis where noise often attenuates during propagation, quality of delay noise analysis is severely affected by any pessimism in noise estimation and can unnecessarily cost valuable silicon and design resources for fixing unreal violations. in this paper, we propose two temporal techniques to reduce pessimism in crosstalk noise aware sta. the first method, "effective delay noise", is a net based method where the exact overlap points of victim and aggressor timing windows are considered to obtain the part of delay noise that actually impacts early and late signal arrival times. the second method, "path based delay noise", is a path based method where the reduced arrival uncertainty of the nets of a given path are utilized for pessimism reduction. we also propose a novel "uncertainty propagation" technique as part of the second method, which results in an iteration free crosstalk noise aware sta of the path with significantly reduced pessimism. the two techniques are combined in a proposed methodology that is compatible with existing industrial static timing analyzers with very little computational overhead compared to the traditional noise aware sta and a significant improvement in eliminating unreal violations. the proposed techniques resulted in 77% reduction of worst case negative slack and 57% reduction in the number of failing paths in the setup analysis of a 90nm industrial design.
numerical integration algorithms and asymptotic waveform evaluation (awe). an intuitive relationship between numerical integration algorithms and awe is established. a small number of data points generated during a brief fixed timestep numerical integration of linear(ized) circuits are used to form sampled waveform integration, correction and extrapolation (swice) models. this method preserves the efficiency of the awe technique, while increasing the accuracy and generality. the strengths of such an approach are illustrated from a theoretical view, as well as with practical examples
physical and reduced-order dynamic analysis of mems. in this paper, we first present an efficient physical level simulationmethod for the dynamic analysis of electrostatic micro-electro-mechanicalsystems (mems). this method is then used to analyzemems dynamics. stiffness hardening or softening of mem structureshas been shown to depend both on the applied voltage andthe geometry. the existence of multiple resonant peaks in the frequencyresponse diagram has been presented. we have shown thata dc bias along with an appropriate ac bias can give fast switchingat a considerably less peak power requirement. finally, a reducedorder model has been developed based on karhunen-loèvedecomposition for the dynamic simulation of mems. reduced ordermodels are cheap in terms of memory and computational timeand are needed to perform fast and efficient system-level compositecircuit and micro-mechanical simulations.
constraint satisfaction for relative location assignment and scheduling. tight data-and timing constraints are imposed by communication and multimedia applications. the architecture for the embedded processor imply resource constraints. instead of random-access registers, relative location storages or rotating register files are used to exploit the available parallelism of resources by means of reducing the initiation interval in pipelined schedules. therefore, the compiler or synthesis tool must deal with the difficult tasks of scheduling of operations and location assignment of values while respecting all the constraints including the storage file capacity. this paper presents a method that handles constraints of relative location storages during scheduling together with timing and resource constraints. the characteristics of the coloring of conflict graphs, representing the relative overlap of value instances, are analyzed in order to identify the bottlenecks for location assignment with the aim of serializing their lifetimes. this is done with pairs of loop instances of values until it can be guaranteed that all constraints will be satisfied. experiments show that high quality schedules for kernels and inner loops can be efficiently obtained.
cycle time and slack optimization for vlsi-chips. we consider the problem of finding an optimal clock schedule, i.e. optimal arrival times for clock signals at latches of a vlsi chip. we describe a general model which includes all previously considered models. then we show how to optimize the cycle time and optimally balance slacks on data paths and on clocktree paths.the problem of finding a clock schedule with the optimum cycle time was solved before, either by linear programming or by binary search, using a test for negative circuits in a digraph as a subroutine. we show for the first time that a direct combinatorial algorithm solves this problem optimally. incidentally, this yields a new efficient method for timing analysis with transparent latches.moreover, we extend this algorithm to the slack balancing problem: to make the chip less sensitive to routing detours, process variations and manufacturing skew it is desirable to have as few critical paths as possible. we show how to find the clock schedule with minimum number of critical paths (optimum slack distribution) in a well-defined sense. rather than fixed clock arrival times we show how to obtain as large as possible intervals for the clock arrival times. this can be considered as slack on clocktree paths. indeed, we can find the global optimum of simultaneous optimization of slacks on all data paths and clocktree paths.all the above is done by very efficient network optimization algorithms, based on parametric shortest paths. our computational results with recent ibm processor chips show that the number of critical paths decreases dramatically, in addition to a considerable improvement of the cycle time. the running times are reasonable even for the largest designs.
post-verification debugging of hierarchical designs. as vlsi designs grow in complexity and size, errors become more frequent and difficult to track. recent developments have automated most of the verification tasks but debugging still remains a resource-intensive, manually conducted procedure. this paper bridges this gap as it develops robust automated debugging methodologies that complement verification processes. unlike prior debugging techniques, the proposed one exploits the hierarchical nature of modern designs to improve the performance and quality of debugging. it also formulates the problem in terms of quantified boolean formula satisfiability to obtain dramatic reduction in memory requirements, which allows for debugging of large designs. extensive experiments conducted on industrial and benchmark designs confirm the efficiency and practicality of the proposed approach.
debugging sequential circuits using boolean satisfiability. logic debugging of today's complex sequential circuits is an important problem. in this paper, a logic debugging methodology for multiple errors in sequential circuits with no state equivalence is developed. the proposed approach reduces the problem of debugging to an instance of boolean satisfiability. this formulation takes advantage of modern boolean satisfiability solvers that handle large circuits in a computationally efficient manner. an extensive suite of experiments with large sequential circuits confirm the robustness and efficiency of the proposed approach. the results further suggest that boolean satisfiability provides an effective platform for sequential logic debugging.
precomputation-based sequential logic optimization for low power. we address the problem of optimizing logic-level sequential circuits for low power. we present a powerful sequential logic optimization method that is based on selectively precomputing the output logic values of the circuit one clock cycle before they are required, and using the precomputed values to reduce internal switching activity in the succeeding clock cycle. we present two different precomputation architectures which exploit this observation.we present an automatic method of synthesizing precomputational logic so as to achieve maximal reductions in power dissipation. we present experimental results on various sequential circuits. up to 75% reductions in average switching activity and power dissipation are possible with marginal increases in circuit area and delay.
automatic gate-level synthesis of speed-independent circuits. a cad tool for the synthesis of asynchronous control circuits using basic gates such as and gates and or gates is presented. the synthesized circuits are speed-independent-that is, they work correctly regardless of individual gate delays. synthesis results for a variety of specifications taken from industry and previously published examples are presented. the speed-independent circuits are compared with those non-speed-independent circuits synthesized using previously described algorithms, in which delay elements are added to remove circuit hazards. these synthesis results show that the new circuits are on average approximately 25% faster with an area penalty of only 15%. this work demonstrates that direct synthesis of gate-level speed-independent circuits is not only feasible, but also produces robust and relatively efficient circuits compared to those synthesized with timing constraints
estimation and bounding of energy consumption in burst-mode control circuits. this paper describes two techniques to quantify energy consumption of burst-mode asynchronous (clock-less) control circuits. the circuit specifications considered are extended burst-mode specifications, and the implementations are multi-level logic implementations whose outputs are guaranteed to be free of any voltage glitches (hazards). both techniques use stochastic analysis to combine a small number of simulations in order to quantify average energy per external signal transition. the first technique uses n-valued simulation to derive mathematically tight upper and lower bounds of energy consumption. using this technique we bound the effect of hazards under all possible operating conditions and environments for a given circuit. additionally, to drive synthesis tools for low-power, we propose a second technique that uses fixed-delay simulation to derive a realistic estimate of energy consumption within our derived upper and lower bounds. we demonstrate the feasibility of both these techniques on a variety of burst-mode control circuits used in an industrial-quality chip. our preliminary results indicate that less than 5% of the power of typical multi-level burst-mode circuits can be attributed to hazards.
hierarchical partitioning. partitioning of digital circuits has become a key problem area during the last five years. benefits from new technologies like multi-chip-modules or logic emulation strongly depend on partitioning results. most published approaches are based on abstract graph models constructed from flat netlists, which consider only connectivity information. the approach presented in this paper uses information on design hierarchy in order to improve partitioning results and reduce problem complexity. designs up to 150k gates have been successfully partitioned by descending and ascending the hierarchy. compared to a standard k-way iterative improvement partitioning approach results are improved by up to 65% and runtimes are decreased by up to 99%.
faster sat and smaller bdds via common function structure. the increasing popularity of sat and bdd techniques in verification and synthesis encourages the search for additional speed-ups. since typical sat and bdd algorithms are exponential in the worst-case, the structure of real-world instances is a natural source of improvements. while sat and bdd techniques are often presented as mutually exclusive alternatives, our work points out that both can be improved via the use of the same structural properties of instances. our proposed methods are based on efficient problem partitioning and can be easily applied as pre-processing with arbitrary sat solvers and bdd packages without source code modifications.finding a better variable-ordering is a well recognized problem for both sat solvers and bdd packages. currently, all leading edge variable-ordering algorithms are dynamic, in the sense that they are invoked many times in the course of the "host" algorithm that solves sat or manipulates bdds. examples include the dlcs ordering for sat solvers and variable-sifting during bdd manipulations. in this work we propose a universal variable-ordering mince (min cut etc.) that pre-processes a given boolean formula in cnf. mince is completely independent from target algorithms and outperforms both dlcs for sat and variable sifting for bdds. we argue that mince tends to capture structural properties of boolean functions arising from real-world applications. our contribution is validated on the iscas circuits and the dimacs benchmarks. empirically, our technique often outperforms existing techniques by a factor of two or more. our results motivate search for stronger dynamic ordering heuristics and combined static/dynamic techniques.
performance efficiency of context-flow system-on-chip platform. recent efforts in adapting computer networks into system-on-chip(soc), or network-on-chip, present a setback to the traditionalcomputer systems for the lack of effective programming model,while not taking full advantage of the almost unlimited on-chipbandwidth. in this paper, we propose a new programming model,called context-flow, that is simple, safe, highly parallelizable yettransparent to the underlying architectural details. an soc platformarchitecture is then designed to support this programmingmodel, while fully exploiting the physical proximity between theprocessing elements. we demonstrate the performance efficiencyof this architecture over bus based and packet-switch based networksby two case studies using a multi-processor architecture simulator.
generic ilp versus specialized 0-1 ilp: an update. optimized solvers for the boolean satisfiability (sat) problem have many applications in areas such as hardware and software verification, fpga routing, planning, etc. further uses are complicated by the need to express "counting constraints" in conjunctive normal form (cnf). expressing such constraints by pure cnf leads to more complex sat instances. alternatively, those constraints can be handled by integer linear programming (ilp), but generic ilp solvers may ignore the boolean nature of 0--1 variables. therefore specialized 0--1 ilp solvers extend sat solvers to handle these so-called "pseudo-boolean" constraints.this work provides an update on the on-going competition between generic ilp techniques and specialized 0--1 ilp techniques. to make a fair comparison, we generalize recent ideas for fast sat-solving to more general 0--1 ilp problems that may include counting constraints and optimization. another aspect of our comparison is evaluation on 0--1 ilp benchmarks that originate in electronic design automation (eda), but that cannot be directly solved by a sat solver. specifically, we solve instances of the max-sat and max-ones optimization problems which seek to maximize the number of satisfied clauses and the "true" values over all satisfying assignments, respectively. those problems have straightforward applications to sat-based routing and are additionally important due to reductions from max-cut, max-clique, and min vertex cover. our experimental results show that specialized 0--1 techniques tend to outperform generic ilp techniques on boolean optimization problems as well as on general eda sat problems.