NDLI: DAG-aware circuit compression for formal verification

Please wait, while we are loading the content...

Table of Contents

Asymptotic probability extraction for non-normal distributions of circuit performance

Statistical design and optimization of SRAM cell for yield enhancement

Gate sizing for crosstalk reduction under timing constraints by Lagrangian relaxation

Optimizing mode transition sequences in idle intervals for component-level and system-level energy minimization

Dynamic voltage and frequency scaling under a precise energy model considering variable and fixed components of the system power dissipation

The effects of energy management on reliability in real-time embedded systems

DAG-aware circuit compression for formal verification

Dynamic transition relation simplification for bounded property checking

Theoretical framework for compositional sequential hardware equivalence verification in presence of design constraints

Checking consistency of C and Verilog using predicate abstraction and induction

SAPOR: second-order Arnoldi method for passive order reduction of RCS circuits

SPRIM: structure-preserving reduced-order interconnect macromodeling

Sparse and efficient reduced order modeling of linear subcircuits with large number of terminals

Fast simulation of VLSI interconnects

Cost-effective radiation hardening technique for combinational logic

Improving soft-error tolerance of FPGA configuration bits

A soft error rate analysis (SERA) methodology

Banked scratch-pad memory management for reducing leakage energy consumption

Reducing cache misses by application-specific re-configurable indexing

DynamoSim: a trace-based dynamically compiled instruction set simulator

The care and feeding of your statistical static timer

Analytical modeling of crosstalk noise waveforms using Weibull function

A robust cell-level crosstalk delay change analysis

Timing macro-modeling of IP blocks with crosstalk

Delay noise pessimism reduction by logic correlations

Factoring and eliminating common subexpressions in polynomial expressions

Custom-optimized multiplierless implementations of DSP algorithms

A quantitative study and estimation models for extensible instructions in embedded processors

Code partitioning for synthesis of embedded applications with phantom

Formal verification coverage: computing the coverage gap between temporal specifications

Debugging sequential circuits using Boolean satisfiability

Towards formal verification of analog designs

Automatic translation of behavioral testbench for fully accelerated simulation

Architectural-level synthesis of digital microfluidics-based biochips

Simultaneous design and placement of multiplexed chemical processing systems on microchips

A circuit model for carbon nanotube interconnects: comparative study with Cu interconnects for scaled technologies

Hybrid techniques for electrostatic analysis of nanowires

Computation of signal threshold crossing times directly from higher order moments

Modeling unbuffered latches for timing analysis

A flexibility aware budgeting for hierarchical flow timing closure

Energy optimization for a two-device data flow chain

A power aware system level interconnect design methodology for latency-insensitive systems

Exploiting level sensitive latches in wire pipelining

Floorplan design for multi-million gate FPGAs

Temporal floorplanning using the T-tree formulation

A thermal-driven floorplanning algorithm for 3D ICs

A chip-level electrostatic discharge simulation strategy

Efficient full-chip thermal modeling and analysis

Interconnect lifetime prediction under dynamic stress for reliability-aware design

Process and environmental variation impacts on ASIC timing

The impact of device parameter variations on the frequency and performance of VLSI chips

Variability in sub-100nm SRAM designs

Application-specific buffer space allocation for networks-on-chip router design

Simultaneous communication and processor voltage scaling for dynamic and leakage energy reduction in time-constrained systems

Hardware/software managed scratchpad memory for embedded system

Physical placement driven by sequential timing analysis

On interactions between routing and detailed placement

Routability-driven placement and white space allocation

True crosstalk aware incremental placement with noise map

On breakable cyclic definitions

Logical effort based technology mapping

Variability inspired implementation selection problem

M-trie: an efficient approach to on-chip logic minimization

Verifying properties of hardware and software by predicate abstraction and model checking

Soft self-synchronising codes for self-calibrating communication

SILENT: serialized low energy transmission coding for on-chip interconnection networks

Optimal wire retiming without binary search

Interval-valued reduced order statistical interconnect modeling

Static statistical timing analysis for latch-based pipeline designs

Efficient statistical timing analysis through error budgeting

Voltage-drop-constrained optimization of power distribution network based on reliable maximum current estimates

Fast flip-chip power grid analysis via locality and grid shells

HiSIM: hierarchical interconnect-centric circuit simulator

Guiding CNF-SAT search via efficient constraint partitioning

Incremental deductive & inductive reasoning for SAT-based bounded model checking

Efficient SAT-based unbounded symbolic model checking using circuit cofactoring

Efficient computation of small abstraction refinements

Exact and heuristic approaches to input vector control for leakage power reduction

Leakage control through fine-grained placement and sizing of sleep transistors

A vectorless estimation of maximum instantaneous current for sequential circuits

A new incremental placement algorithm and its application to congestion-aware divisor extraction

Unification of partitioning, placement and floorplanning

Multilevel expansion-based VLSI placement with blockages

An analytic placer for mixed-size placement and timing-driven placement

Engineering details of a stable force-directed placer

An integrated design flow for a via-configurable gate array

A metal and via maskset programmable VLSI design methodology using PLAs

Analysis and evaluation of a hybrid interconnect structure for FPGAs

Low-power programmable routing circuitry for FPGAs

A yield improvement methodology using pre- and post-silicon statistical clock scheduling

Clock schedule verification under process variations

A novel clock distribution and dynamic de-skewing methodology

On per-test fault diagnosis using the X-fault model

Diagnosis of small-signal parameters for broadband amplifiers through S-parameter measurements and sensitivity-guided evolutionary search

An efficient method for improving the quality of per-test fault diagnosis

A unified theory of timing budget management

Dynamic range estimation for nonlinear systems

Power estimation for cycle-accurate functional descriptions of hardware

Efficient harmonic balance simulation using multi-level frequency decomposition

Frequency domain simulation of high-Q oscillators with homotopy methods

Automated oscillator macromodelling techniques for capturing amplitude variations and injection locking

FLUTE: fast lookup table based wirelength estimation technique

Wire-length prediction using statistical techniques

Accurate estimation of global buffer delay within a floorplan

A path-based methodology for post-silicon timing validation

Frugal linear network-based test decompression for drastic test cost reductions

Design space exploration for aggressive test cost reduction in CircularScan architectures

Design/process learning from electrical test

Backend CAD flows for "restrictive design rules"

Hermes: LUT FPGA technology mapping algorithm for area minimization with optimum depth

DAOmap: a depth-optimal area optimization mapping algorithm for FPGA designs

Vdd programmability to reduce FPGA interconnect power

Configuration bitstream compression for dynamically reconfigurable FPGAs

High-level synthesis: an essential ingredient for designing complex ASICs

High-level synthesis using computation-unit integrated memories

Improved use of the carry-save representation for the synthesis of complex arithmetic circuits

Formal derivation of optimal active shielding for low-power on-chip buses

A general framework for probabilistic low-power design space exploration considering process variation

Timing analysis considering spatial power/ground level variation

Simultaneous escape routing and layer assignment for dense PCBs

A provably good algorithm for high performance bus routing

Simultaneous short-path and long-path timing optimization for FPGAs

Analog performance space exploration by Fourier-Motzkin elimination with application to hierarchical sizing

Robust analog/RF circuit design with projection-based posynomial modeling

Techniques for improving the accuracy of geometric-programming based analog circuit design optimization

Variational interconnect analysis via PMTBR

Stochastic analysis of interconnect performance in the presence of process variations

A stochastic integral equation method for modeling the rough surface effect on interconnect capacitance

Detection of multiple transitions in delay fault test of SPARC64 microprocessor

Minimizing the number of test configurations for FPGAs

SPIN-TEST: automatic test pattern generation for speed-independent circuits

How to bridge the abstraction gap in system level modeling and design

Analyzing software influences on substrate noise: an ADC perspective

Design space exploration for a UMTS front-end exploiting analog platforms

Adaptive sampling and modeling of analog circuit performance parameters with pseudo-cubic splines

DAG-aware circuit compression for formal verification

Content Provider	ACM Digital Library
Author	Boralv, A. Bjesse, P.
Abstract	The choice of representation for circuits and Boolean formulae in a formal verification tool is important for two reasons. First of all, representation compactness is necessary in order to keep the memory consumption low. This is witnessed by the importance of maximum processable design size for equivalence checkers. Second, many formal verification algorithms are sensitive to redundancies in the design that is processed. To address these concerns, three different auto-compressing representations for Boolean circuit networks and formulas have been suggested in the literature. We attempt to find a blend of features from these alternatives that allows us to remove as much redundancy as possible while not sacrificing runtime. By studying how the network representation size varies when we change parameters, we show that the use of only one operator node is suboptimal, and demonstrate that the most powerful of the proposed reduction rules, two-level minimization, actually can be harmful. We correct the bad behavior of two-level optimization by devising a simple linear simplification algorithm that can remove tens of thousands of nodes on examples where all obvious redundancies already have been removed. The combination of our compactor with the simplest representation outperforms all of the alternatives we have studied, with a theoretical runtime bound that is at least as good as the three studied representations.
Starting Page	42
Ending Page	49
Page Count	8
File Format	PDF
ISBN	0780387023
DOI	10.1109/ICCAD.2004.1382541
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2004-11-07
Access Restriction	Subscribed
Content Type	Text
Resource Type	Article

Central Library (ISO-9001:2015 Certified)
Indian Institute of Technology Kharagpur
Kharagpur, West Bengal, India | PIN - 721302

See location in the Map
03222 282435
Mail: support@ndl.gov.in

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in