NDLI: On resolution proofs for combinational equivalence

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

Trusted hardware: can it be trustworthy?

System-level design flow based on a functional reference for HW and SW

Design of rotary clock based circuits

An effective guidance strategy for abstraction-guided simulation

Fine-grained sleep transistor sizing algorithm for leakage power minimization

Voltage-frequency island partitioning for GALS-based networks-on-chip

Interdependent latch setup/hold time characterization via Euler-Newton curve tracing on state-transition equations

On-chip decoupling capacitance and P/G wire co-optimization for dynamic noise

Formal techniques for SystemC verification

Endurance enhancement of flash-memory storage systems: an efficient static wear leveling design

Comparative analysis of conventional and statistical design techniques

Chip multi-processor generator

Period optimization for hard real-time distributed automotive systems

NanoMap: an integrated design optimization flow for a hybrid nanotube/CMOS dynamically reconfigurable architecture

GlitchMap: an FPGA technology mapper for low power considering glitches

Fast min-cost buffer insertion under process variations

Characterization and estimation of circuit reliability degradation under NBTI using on-line $I_{DDQ}$ measurement

There is more than Moore in automotive....

Design-silicon timing correlation: a data mining perspective

Progressive decomposition: a heuristic to structure arithmetic circuits

Parameter finding methods for oscillators with a specified oscillation frequency

TLM: crossing over from buzz to adoption

MP-trees: a packing-based macro placement algorithm for mixed-size designs

Modeling the function cache for worst-case execution time analysis

Confidence scalable post-silicon statistical delay prediction under process variations

Scan test planning for power reduction

Automotive software integration

Interconnects in the third dimension: design challenges for 3D ICs

Alembic: an efficient algorithm for CNF preprocessing

An integer linear programming based routing algorithm for flip-chip design

Synthetic biology: from bacteria to stem cells

Instruction splitting for efficient code compression

A robust protocol for concurrent on-line test (COLT) of NoC-based systems-on-a-chip

Analysis and optimization of sleep modes in subthreshold circuit design

Shared resource access attributes for high-level contention models

Thousand core chips: a technology perspective

Interconnect and communication synthesis for distributed register-file microarchitecture

RISPP: rotating instruction set processing platform

A general framework for spatial correlation modeling in VLSI design

A unified approach to canonical form-based Boolean matching

SODA: sensitivity based optimization of disk architecture

Intelligent interleaving of scenarios: a novel approach to system level test generation

DDBDD: delay-driven BDD synthesis for FPGAs

Efficient parametric yield extraction for multiple correlated non-normal performance distributions of Analog/RF circuits

Integrated droplet routing in the synthesis of microfluidic biochips

Clock period minimization with minimum delay insertion

Trusted design in FPGAs

Model-driven validation of SystemC designs

Escape routing for dense pin clusters in integrated circuits

Leveraging semi-formal and sequential equivalence techniques for multimedia SOC performance validation

Width-dependent statistical leakage modeling for random dopant induced threshold voltage shift

Introducing the SuperGT network-on-chip: SuperGT QoS: more than just GT

PV-PPV: parameter variability aware, automatically extracted, nonlinear time-shifted oscillator macromodels

Optimal selection of voltage regulator modules in a power delivery network

Design for verification in system-level models and RTL

A system for coarse grained memory protection in tiny embedded processors

Fast second-order statistical static timing analysis using parameter dimension reduction

The case for the precision timed (PRET) machine

Performance analysis of FlexRay-based ECU networks

Design and analysis of hybrid NEMS-CMOS circuits for ultra low-power applications

Using negative edge triggered ffs to reduce glitching power in FPGA circuits

Exact combinatorial optimization methods for physical design of regular logic bricks

The impact of NBTI on the performance of combinational and sequential circuits

Modeling safe operating area in hardware description languages

Silicon speedpath measurement and feedback into EDA flows

Topology-based optimization of maximal sustainable throughput in a latency-insensitive system

Modeling simultaneous switching noise-induced jitter for system-on-chip phase-locked loops

RQL: global placement via relaxed quadratic spreading and linearization

An embedded multi-resolution AMBA trace analyzer for microprocessor-based SoC integration

Statistical framework for technology-model-product co-design and convergence

Critical-path-aware X-filling for effective IR-drop reduction in at-speed scan testing

Virtual platforms and timing analysis: status, challenges and future directions

Performance modeling and optimization for single- and multi-wall carbon nanotube interconnects

EHSAT: an efficient RTL satisfiability solver using an extended DPLL procedure

Computationally efficient power integrity simulation for system-on-package applications

Engineering synthetic killer circuits in bacteria

An embedded coherent-multithreading multimedia processor and its programming model

SOC test architecture optimization for signal integrity faults on core-external interconnects

Nanometer device scaling in subthreshold circuits

A probabilistic approach to model resource contention for performance estimation of multi-featured media devices

The kill rule for multicore

Selective bandwidth and resource management in scheduling for dynamically reconfigurable architectures

ASIP instruction encoding for energy and area reduction

Modeling and analysis of non-rectangular gate for post-lithography circuit simulation

Gate sizing for cell library-based designs

Dynamic power management with hybrid power sources

Automatic verification of external interrupt behaviors for microprocessor design

FlexWAFE - a high-end real-time stream processing library for FPGAs

Variation resilient low-power circuit design methodology using on-chip phase locked loop

OPC-free and minimally irregular IC design style

An efficient mechanism for performance optimization of variable-latency designs

Physical unclonable functions for device authentication and secret key generation

Language extensions to SystemC: process control constructs

TROY: track router with yield-driven wire planning

Synthesizing SVA local variables for formal verification

Modeling and estimation of full-chip leakage current considering within-die correlation

Layered switching for networks on chip

Accurate waveform modeling using singular value decomposition with applications to timing analysis

Top-k aggressors sets in delay noise analysis

Verification methodologies in a TLM-to-RTL design flow

Reducing off-chip memory access costs using data recomputation in embedded chip multi-processors

Non-linear statistical static timing analysis for non-Gaussian variation sources

Quantum-like effects in network-on-chip buffers behavior

Experimental jitter analysis in a FlexCAN based drive-by-wire automotive application

Towards an ultra-low-power architecture using single-electron tunneling transistors

Single-event-upset (SEU) awareness in FPGA routing

Concurrent wire spreading, widening, and filling

NBTI-aware synthesis of digital circuits

Autonomous automobiles: developing cars that drive themselves

Characterizing process variation in nanometer CMOS

Synchronous elastic circuits with early evaluation and token counterflow

Accelerating harmonic balance simulation using efficient parallelizable hierarchical preconditioning

Improving voltage assignment by outlier detection and incremental placement

Hardware support for secure processing in embedded systems

Extraction of statistical timing profiles using test data

Transition delay fault test pattern generation considering supply voltage noise in a SOC design

Computer-aided architecture design & optimized implementation of distributed automotive EE systems

Micro-photonic interconnects: characteristics, possibilities and limitations

On-the-fly resolve trace minimization

Off-chip decoupling capacitor allocation for chip package co-design

Programming living cells to function as massively parallel computers

Efficient computation of buffer capacities for cyclo-static dataflow graphs

A DFT method for time expansion model at register transfer level

Efficient modeling techniques for dynamic voltage drop analysis

Automatic cache tuning for energy-efficiency using local regression modeling

Implicitly parallel programming models for thousand-core microprocessors

Multiprocessor resource allocation for throughput-constrained synchronous dataflow graphs

Approximation algorithm for data mapping on block multi-threaded network processor architectures

A framework for accounting for process model uncertainty in statistical static timing analysis

Statistical leakage power minimization using fast equi-slack shell based optimization

System-on-chip power management considering leakage power variations

A framework for the validation of processor architecture compliance

How much can logic perturbation help from netlist to final routing for FPGAs

Parameterized macromodeling for analog system-level design exploration

Automated design of misaligned-carbon-nanotube-immune circuits

A fully-automated desynchronization flow for synchronous circuits

Side-channel attack pitfalls

Simulink-based MPSoC design flow: case study of Motion-JPEG and H.264

IPR: an integrated placement and routing algorithm

Statistical analysis of full-chip leakage power considering junction tunneling leakage

Energy-aware synthesis of networks-on-chip implemented with voltage islands

Simulating improbable events

A new twisted differential line structure in global bus design

Memory modeling in ESL-RTL equivalence checking

A memory-conscious code parallelization scheme

Beyond low-order statistical response surfaces: latent variable regression for efficient, highly nonlinear fitting

CAD-based security, cryptography, and digital rights management

Optimization of static task and bus access schedules for time-triggered distributed embedded systems with model-checking

Enhancing FPGA performance for arithmetic circuits

Modeling litho-constrained design layout

On-chip measurements complementary to design flow for integrity in SoCs

Optimization of area in digital FIR filters using gate-level metrics

Fast, non-Monte-Carlo estimation of transient performance variation due to device mismatch

Analog placement based on novel symmetry-island formulation

RIJID: random code injection to mask power analysis based side channel attacks

An analysis of timing violations due to spatially distributed thermal effects in global wires

New test data decompressor for low power applications

CAD implications of new interconnect technologies

On resolution proofs for combinational equivalence

Scalability of 3D-integrated arithmetic units in high-performance microprocessors

Synthesizing stochasticity in biochemical systems

Energy-aware scheduling for real-time multiprocessor systems with uncertain task execution time

Test generation in the presence of timing exceptions and constraints

On estimating impact of loading effect on leakage current in sub-65nm scaled CMOS circuits based on Newton-Raphson method

Reducing data-memory footprint of multimedia applications by delay redistribution

Multi-core design automation challenges

Global critical path: a tool for system-level timing analysis

Program mapping onto network processors by recursive bipartitioning and refining

Fast capacitance extraction in multilayer, conformal and embedded dielectric using hybrid boundary element method

Techniques for effective distributed physical synthesis

Accelerating system-on-chip power analysis using hybrid power estimation

Functional verification of sicortex multiprocessor: system-on-a-chip

Simultaneous multi-topology multi-objective sizing across thousands of analog circuit topologies

Quantum circuit placement: optimizing qubit-to-qubit interactions through mapping quantum circuits into a physical experiment

Self-resetting latches for asynchronous micro-pipelines

Skewed flip-flop transformation for minimizing leakage in sequential circuits

The case for low-power photonic networks on chip

SBPOR: second-order balanced truncation for passive order reduction of RLC circuits

Effects of coupling capacitance and inductance on delay uncertainty and clock skew

A self-tuning configurable cache

Line-end shortening is not always a failure

Compact state machines for high performance pattern matching

Placement of 3D ICs with thermal and interlayer via considerations

Energy-aware data compression for multi-level cell (MLC) flash memory

Designer-controlled generation of parallel and flexible heterogeneous MPSoC specification

Design methodology for pipelined heterogeneous multiprocessor system

A provably good approximation algorithm for power optimization using multiple supply voltages

Reliability analysis for flexible electronics: case study of integrated a-Si:H TFT scan driver

You can get there from here: connectivity of random graphs on grids

High performance and low power electronics on flexible substrate

Novel CNTFET-based reconfigurable logic gate design

On resolution proofs for combinational equivalence

Content Provider	ACM Digital Library
Author	Mishchenko, Alan Kuehlmann, Andreas Brayton, Robert Chatterjee, Satrajit
Abstract	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.
Starting Page	600
Ending Page	605
Page Count	6
File Format	PDF
ISBN	9781595936271
ISSN	0738100X
DOI	10.1145/1278480.1278631
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2007-06-04
Publisher Place	New York
Access Restriction	Subscribed
Subject Keyword	Resolution proofs Equivalence checking Transformation-based verification
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