14 Result(s)
within
Article
Sharad Malik
-
Article
Model checking unbounded concurrent lists
We present a model checking-based method for verifying list-based concurrent set data structures. Concurrent data structures are notorious for being hard to get right and thus, their verification has received ...
-
Article
On computing minimal independent support and its applications to sampling and counting
Constrained sampling and counting are two fundamental problems arising in domains ranging from artificial intelligence and security, to hardware and software testing. Recent approaches to approximate solutions...
-
Article
Specification and encoding of transaction interaction properties
Transaction-level modeling is used in hardware design for describing designs at a higher level compared to the register-transfer level (RTL) (e.g. Cai and Gajski in CODES+ISSS ’03: proceedings of the 1st IEEE/...
-
Article
Preface
-
Article
Declarative Infrastructure Configuration Synthesis and Debugging
There is a large conceptual gap between end-to-end infrastructure requirements and detailed component configuration implementing those requirements. Today, this gap is manually bridged so large numbers of conf...
-
Article
Achieving Structural and Composable Modeling of Complex Systems
This paper describes a recently released, structural and composable modeling system called the Liberty Simulation Environment (LSE). LSE automatically constructs simulators from system descriptions that closel...
-
Article
Limits of Using Signatures for Permutation Independent Boolean Comparison
This paper addresses problems that arise while checking the equivalence of two Boolean functions under arbitrary input permutations. The permutation problem has several applications in the synthesis and verifi...
-
Article
Application of BDDs in Boolean matching techniques for formal logic combinational verification
Verifying that an implementation of a combinational circuit meets its golden specification is an important step in the design process. As inputs and outputs can be swapped by synthesis tools or by interaction ...
-
Article
A Retargetable Compilation Methodology for Embedded Digital Signal Processors Using a Machine-Dependent Code Optimization Library
We address the problem of code generation for embedded DSP systems. Such systems devote a limited quantity of silicon to program memory, so the embedded software must be sufficiently dense. Additionally, this ...
-
Article
Paged Absolute Addressing Mode Optimizations for Embedded Digital Signal Processors Using Post-pass Data-flow Analysis
We address the problem of code generation for embedded DSP systems. In such systems, it is typical for one or more digital signal processors (DSPs), program memory, and custom circuitry to be integrated onto a...
-
Article
Instruction level power analysis and optimization of software
The increasing popularity of power constrained mobile computers and embedded computing applications drives the need for analyzing and optimizing power in all the components of a system. Software constitutes a ...
-
Article
Editorial
-
Article
Verification of asynchronous interface circuits with bounded wire delays
We address the problem of verifying that the gate-level implementation of an asynchronous circuit, with given or extracted bounds on wire and gate delays, is equivalent to a specification of the asynchronous c...
-
Article
A synthesis-based test generation and compaction algorithm for multifaults
Because of its inherent complexity, the problem of automatic test pattern generation for multiple stuck-at faults (multifaults) has been largely ignored. Recently, the observation that multifault testability i...
