EDBT 2026 Demo / reviewers in the wild / expert
Srini Devadas
dblp:14/3973 · also Srinivas Devadas
· DBLP profile ↗
263ranked-venue papers
53as first author
27since 2021 · last 2026
0000-0001-8253-7714ORCID · verified
Domains — the database's venue-derived domains; a paper can count in several
Systems, architecture and hardware · 183 · 50 first-author · 5 since 2021Security and privacy · 49 · 3 first-author · 17 since 2021Software engineering, systems software and programming languages · 17 · 3 since 2021Applied, interdisciplinary, general and emerging computing · 11 · 1 since 2021Theory of computation · 7 · 1 first-author · 1 since 2021Computer networks · 5 · 2 since 2021Databases, data management, data science and information retrieval · 5 · 1 since 2021Artificial intelligence and machine learning · 3
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2026 | Concretely-Efficient Multi-Key Homomorphic Secret Sharing and Applications
Sacha Servan-Schreiber, Geoffroy Couteau, Srini Devadas |
SP | 4 |
| 2026 | Privacy-Conscious Algorithm Design Via PAC Privacy
Mayuri Sridhar, Xiaochen Zhu 0003, Srini Devadas |
SP | 3 |
| 2026 | Making Sense of Private Advertising: A Principled Approach to a Complex EcosystemabstractIn this work, we model the end-to-end pipeline of the advertising ecosystem, allowing us to identify two main issues with the current trajectory of private advertising proposals. First, prior work has largely considered ad targeting and engagement metrics individually rather than in composition. This has resulted in privacy notions that, while reasonable for each protocol in isolation, fail to compose to a natural notion of privacy for the ecosystem as a whole, permitting advertisers to extract new information about the audience of their advertisements. The second issue serves to explain the first: we prove that perfect privacy is impossible for any, even minimally, useful advertising ecosystem, due to the advertisers' expectation of conducting market research on the results. Having demonstrated that leakage is inherent in advertising, we re-examine what privacy could realistically mean in advertising, building on the well-established notion of sensitive data in a specific context. We identify that fundamentally new approaches are needed when designing privacy-preserving advertising subsystems in order to ensure that the privacy properties of the end-to-end advertising system are well aligned with people's privacy desires. Kyle Hogan, Alishah Chator, Gabriel Kaptchuk, Mayank Varia, Srini Devadas |
Proc. Priv. Enhancing Technol. | 5 |
| 2025 | One-Sided Bounded Noise: Theory, Optimization Algorithms and ApplicationsabstractWe investigate the optimal trade-off between utility and privacy using one-sided perturbation. Unlike conventional privacy-preserving statistical releases, randomization for obfuscating side-channel information is often constrained by infrastructure limitations. In practical scenarios, these constraints may only allow positive and bounded perturbations. For example, extending processing time or sending and storing dummy messages/data is typically feasible. However, implementing modifications in the opposite direction is challenging due to restrictions imposed by hardware capacity, communication protocols, and data management systems. In this paper, we establish the foundation of the positive noise mechanism within three semantic privacy frameworks: Differential Privacy (DP), Maximal Leakage (MaxL), and Probably Approximately Correct (PAC) Privacy. We then present a series of results that characterize or approximate the optimal one-sided noise distribution, subject to a second-moment budget and a bounded maximal magnitude. Building on this theoretical foundation, we develop efficient tools to solve the underlying optimization problems. Through experiments conducted in various scenarios, we demonstrate that existing techniques, such as Truncated Biased Laplace noise, are often suboptimal and result in excessive performance degradation. For instance, in an anonymous communication system with a 250K message budget, our optimized DP noise mechanism achieves a 21× reduction in dummy messages and an 18× reduction in dummy message latency overhead compared to traditional methods. Hanshen Xiao, Jun Wan 0008, Elaine Shi, Srini Devadas |
CCS | 4 |
| 2025 | Remote Direct Code ExecutionabstractWe propose remote direct code execution (RDX), which elevates the power of RDMA from memory access to code execution. We target runtime extension frameworks such as Wasm filters, BPF programs, and UDF functions, where RDX enables an agentless architecture that unlocks capabilities such as fast extension injection, update consistency guarantees, and minimal resource contention. We outline the roadmap for RDX around a new CodeFlow abstraction, encompassing programming remote extensions, exposing management stubs, remotely validating and JIT compiling code, seamlessly linking code to local context, managing remote extension state, and synchronizing code to targets. The case studies and initial results demonstrate the feasibility of RDX and its potential to spark the next wave of RDMA innovations. Yibo Huang 0005, Yiming Qiu 0001, Daqian Ding, Patrick Tser Jern Kon, Yiwen Zhang 0008, Yuzhou Mao, Archit Bhatnagar, Mosharaf Chowdhury, Srini Devadas, Jiarong Xing, Ang Chen 0001 |
HotNets | 9 |
| 2025 | PAC-Private AlgorithmsabstractProvable privacy typically requires involved analysis and is often associated with unacceptable accuracy loss. While many empirical verification or approximation methods, such as Membership Inference Attacks (MIA) and Differential Privacy Auditing (DPA), have been proposed, these do not offer rigorous privacy guarantees. In this paper, we apply recently-proposed Probably Approximately Correct (PAC) Privacy to give formal, mechanized, simulation-based proofs for a range of practical, black-box algorithms: K-Means, Support Vector Machines (SVM), Principal Component Analysis (PCA) and Random Forests. To provide these proofs, we present a new simulation algorithm that efficiently determines anisotropic noise perturbation required for any given level of privacy. We provide a proof of correctness for this algorithm and demonstrate that anisotropic noise has substantive benefits over isotropic noise. Stable algorithms are easier to privatize, and we demonstrate privacy amplification resulting from introducing regularization in these algorithms; meaningful privacy guarantees are obtained with small losses in accuracy. We propose new techniques in order to reduce instability in algorithmic output and convert intractable geometric stability verification into efficient deterministic stability verification. Thorough experiments are included, and we validate our provable adversarial inference hardness against state-of-the-art empirical attacks. Mayuri Sridhar, Hanshen Xiao, Srini Devadas |
SP | 3 |
| 2025 | Pseudorandom Correlation Functions for Garbled Circuits
Geoffroy Couteau, Srini Devadas, Alexander Koch 0001, Sacha Servan-Schreiber |
TCC (2) | 2 |
| 2025 | Expected Constant Round Byzantine Broadcast under Dishonest MajorityabstractByzantine Broadcast (BB) is a central question in distributed systems, and an important challenge is to understand its round complexity. Under the honest majority setting, it is long known that there exist randomized protocols that can achieve BB in expected constant rounds, regardless of the number of nodes n . However, whether we can match the expected constant round complexity in the corrupt majority setting —or more precisely, when \(f \ge n/2 + \omega (1)\) —remains unknown, where f denotes the number of corrupt nodes. In this article, we are the first to resolve this long-standing question. We show how to achieve BB in expected \(O((n/(n-f))^2)\) rounds. Our results hold under a weakly adaptive adversary who cannot perform “after-the-fact removal” of messages already sent by a node before it becomes corrupt. We also assume trusted setup and the Decision Linear (DLIN) assumption in bilinear groups. Jun Wan 0008, Hanshen Xiao, Elaine Shi, Srini Devadas |
J. ACM | 4 |
| 2025 | Teaching an Old Dog New Tricks: Verifiable FHE Using Commodity HardwareabstractWe present Argos, a simple approach for adding verifiability to fully homomorphic encryption (FHE) schemes using trusted hardware. Traditional approaches to verifiable FHE require expensive cryptographic proofs, which incur an overhead of up to seven orders of magnitude on top of FHE, making them impractical. With Argos, we show that trusted hardware can be securely used to provide verifiability for FHE computations, with minimal overhead relative to the baseline FHE computation. An important contribution of Argos is showing that the major security pitfall associated with trusted hardware, microarchitectural side channels, can be completely mitigated by excluding any secrets from the CPU and the memory hierarchy. This is made possible by focusing on building a platform that only enforces program and data integrity and not confidentiality (which is sufficient for verifiable FHE, since all data remain encrypted at all times). All secrets related to the attestation mechanism are kept in a separate coprocessor (e.g., a TPM)---inaccessible to any software-based attacker. Relying on a discrete TPM typically incurs significant performance overhead, which is why (insecure) software-based TPMs are used in practice. As a second contribution, we show that for FHE applications, the attestation protocol can be adapted to only incur a fixed cost. Argos requires no dedicated hardware extensions and is supported on commodity processors from 2008 onward. Our prototype implementation introduces 3% overhead for FHE evaluation, and 8% for more complex protocols. In particular, we show that Argos can be used for real-world applications of FHE, such as private information retrieval (PIR) and private set intersection (PSI), where providing verifiability is imperative. By demonstrating how to combine cryptography with trusted hardware, Argos paves the way for widespread deployment of FHE-based protocols beyond the semi-honest setting, without the overhead of cryptographic proofs. Jules Drean, Fisher Jepsen, Edward Suh, Srini Devadas, Aamer Jaleel, Gururaj Saileshwar |
Proc. Priv. Enhancing Technol. | 4 |
| 2024 | QuietOT: Lightweight Oblivious Transfer with a Public-Key Setup
Geoffroy Couteau, Lalita Devadas, Srini Devadas, Alexander Koch 0001, Sacha Servan-Schreiber |
ASIACRYPT (2) | 3 |
| 2024 | Formal Privacy Proof of Data Encoding: The Possibility and Impossibility of Learnable EncryptionabstractWe initiate a formal study on the concept of learnable obfuscation and aim to answer the following question: is there a type of data encoding that maintains the "learnability" of encoded samples, thereby enabling direct model training on transformed data, while ensuring the privacy of both plaintext and the secret encoding function? This long-standing open problem has prompted many efforts to design such an encryption function, for example, NeuraCrypt and TransNet. Nonetheless, all existing constructions are heuristic without formal privacy guarantees, and many successful reconstruction attacks are known on these constructions assuming an adversary with substantial prior knowledge. Hanshen Xiao, G. Edward Suh, Srini Devadas |
CCS | 3 |
| 2024 | Accelerating Zero-Knowledge Proofs Through Hardware-Algorithm Co-DesignabstractZero-Knowledge Proofs (ZKPs) are a cryptographic tool that enables one party (a prover) to prove to another (a verifier) that a statement is true, without requiring the prover to disclose any data to the verifier. ZKPs have many use cases, such as letting clients delegate computation to servers with cryptographic correctness guarantees, while enabling the server to use secret data in these computations. ZKP applications span verifiable machine learning (ML) and databases, online auctions, electronic voting, and blockchains. While ZKPs are already widely used in blockchains, the prohibitive costs of proof generation limit them to proving very simple computations. We present a novel accelerator, NoCap, that leverages hardware-algorithm co-design to achieve transformative speedups. NoCap generates proofs 586× faster than a 32-core CPU, and 41× faster than PipeZK, a state-of-the-art ZKP accelerator. We leverage recent algorithmic developments to achieve these speedups: we identify and combine two recent hash-based ZKP algorithms, Orion and Spartan, which have similar performance on CPUs to the ZKPs targeted by prior accelerators, but are much more amenable to hardware acceleration. Though these algorithms result in larger proofs, we show that the end-to-end speedups (including prover time, proof transmission, and verification time) more than justify this size increase. We contribute a novel hardware organization to exploit these acceleration opportunities: NoCap is a programmable vector processor with functional units tailored to the needs of hash-based ZKPs. We also contribute a co-designed implementation of the Spartan+Orion ZKP tailored to accelerators, with optimizations that improve parallelism and reduce memory traffic. As a result, NoCap achieves speedups that enable new use cases for ZKP. Nikola Samardzic, Simon Langowski, Srini Devadas, Daniel Sánchez 0003 |
MICRO | 3 |
| 2024 | A Tensor Compiler with Automatic Data Packing for Simple and Efficient Fully Homomorphic EncryptionabstractFully Homomorphic Encryption (FHE) enables computing on encrypted data, letting clients securely offload computation to untrusted servers. While enticing, FHE has two key challenges that limit its applicability: it has high performance overheads (10,000× over unencrypted computation) and it is extremely hard to program. Recent hardware accelerators and algorithmic improvements have reduced FHE’s overheads and enabled large applications to run under FHE. These large applications exacerbate FHE’s programmability challenges. Writing FHE programs directly is hard because FHE schemes expose a restrictive, low-level interface that prevents abstraction and composition. Specifically, FHE requires packing encrypted data into large vectors (tens of thousands of elements long), FHE provides limited operations on these vectors, and values have noise that grows with each operation, which creates unintuitive performance tradeoffs. As a result, translating large applications, like neural networks, into efficient FHE circuits takes substantial tedious work. We address FHE’s programmability challenges with the Fhelipe FHE compiler. Fhelipe exposes a simple, numpy-style tensor programming interface, and compiles high-level tensor programs into efficient FHE circuits. Fhelipe’s key contribution is automatic data packing , which chooses data layouts for tensors and packs them into ciphertexts to maximize performance. Our novel framework considers a wide range of layouts and optimizes them analytically. This lets Fhelipe compile large FHE programs efficiently, unlike prior FHE compilers, which either use inefficient layouts or do not scale beyond tiny programs. We evaluate Fhelipe on both a state-of-the-art FHE accelerator and a CPU. Fhelipe is the first compiler that matches or exceeds the performance of large hand-optimized FHE applications, like deep neural networks, and outperforms a state-of-the-art FHE compiler by gmean 18.5×. At the same time, Fhelipe dramatically simplifies programming, reducing code size by 10× – 48×. CCS Concepts: • Software and its engineering → Compilers; • Security and privacy → Cryptography. Aleksandar Krastev, Nikola Samardzic, Simon Langowski, Srini Devadas, Daniel Sánchez 0003 |
Proc. ACM Program. Lang. | 4 |
| 2023 | Geometry of Sensitivity: Twice Sampling and Hybrid Clipping in Differential Privacy with Optimal Gaussian Noise and Application to Deep LearningabstractWe study the fundamental problem of the construction of optimal randomization in Differential Privacy (DP). Depending on the clipping strategy or additional properties of the processing function, the corresponding sensitivity set theoretically determines the necessary randomization to produce the required security parameters. Towards the optimal utility-privacy tradeoff, finding the minimal perturbation for properly-selected sensitivity sets stands as a central problem in DP research. In practice, l2/l1-norm clippings with Gaussian/Laplace noise mechanisms are among the most common setups. However, they also suffer from the curse of dimensionality. For more generic clipping strategies, the understanding of the optimal noise for a high-dimensional sensitivity set remains limited. This raises challenges in mitigating the worst-case dimension dependence in privacy-preserving randomization, especially for deep learning applications. Hanshen Xiao, Jun Wan 0008, Srini Devadas |
CCS | 3 |
| 2023 | PAC Privacy: Automatic Privacy Measurement and Control of Data Processing
Hanshen Xiao, Srini Devadas |
CRYPTO (2) | 2 |
| 2023 | Trellis: Robust and Scalable Metadata-private Anonymous Broadcast
Simon Langowski, Sacha Servan-Schreiber, Srini Devadas |
NDSS | 3 |
| 2023 | A Theory to Instruct Differentially-Private Learning via Clipping Bias ReductionabstractWe study the bias introduced in Differentially-Private Stochastic Gradient Descent (DP-SGD) with clipped or normalized per-sample gradient. As one of the most popular but artificial operations to ensure bounded sensitivity, gradient clipping enables composite privacy analysis of many iterative optimization methods without additional assumptions on either learning models or input data. Despite its wide applicability, gradient clipping also presents theoretical challenges in systematically instructing improvement of privacy or utility. In general, without an assumption on globally-bounded gradient, classic convergence analyses do not apply to clipped gradient descent. Further, given limited understanding of the utility loss, many existing improvements to DP-SGD are heuristic, especially in the applications of private deep learning.In this paper, we provide meaningful theoretical analysis validated by thorough empirical results of DP-SGD. We point out that the bias caused by gradient clipping is underestimated in previous works. For generic non-convex optimization via DP-SGD, we show one key factor contributing to the bias is the sampling noise of stochastic gradient to be clipped. Accordingly, we use the developed theory to build a series of improvements for sampling noise reduction from various perspectives. From an optimization angle, we study variance reduction techniques and propose inner-outer momentum. At the learning model (neural network) level, we propose several tricks to enhance network internal normalization and BatchClipping to carefully clip the gradient of a batch of samples. For data preprocessing, we provide theoretical justification of recently proposed improvements via data normalization and (self-)augmentation.Putting these systematic improvements together, private deep learning via DP-SGD can be significantly strengthened in many tasks. For example, in computer vision applications, with an (ϵ = 8, δ = 10−5) DP guarantee, we successfully train ResNet20 on CIFAR10 and SVHN with test accuracy 76.0% and 90.1%, respectively; for natural language processing, with (ϵ = 4, δ = 10−5), we successfully train a recurrent neural network on IMDb data with test accuracy 77.5%. Hanshen Xiao, Zihang Xiang, Di Wang 0015, Srini Devadas |
SP | 4 |
| 2023 | Remote Direct Memory Introspection
Jiarong Xing, Yibo Huang 0005, Danyang Zhuo, Srini Devadas, Ang Chen 0001 |
USENIX Security Symposium | 5 |
| 2023 | Guest Editorial: IEEE Transactions on Computer, Special Issue on Hardware SecurityabstractARDWARE security is now widely recognized as an essential aspect of computer security, computer architecture, and VLSI design and testing due to developments over the last fifteen years. We have come a long way from questioning the validity of hardware threats to doubting the efficacy of attacks to accepting that attacks exist but arguing that solutions would be expensive to implement to developing solutions deployed in billions of devices. The set of papers in this special issue showcases the next stage of development of hardware security as a discipline. Simha Sethumadhavan, Srini Devadas |
IEEE Trans. Computers | 2 |
| 2022 | Designing Hardware for Cryptography and Cryptography for HardwareabstractThere have been few high-impact deployments of hardware implementations of cryptographic primitives. We present the benefits and challenges of hardware acceleration of sophisticated cryptographic primitives and protocols, and briefly describe our recent work. We argue the significant potential for synergistic codesign of cryptography and hardware, where customized hardware accelerates cryptographic protocols that are designed with hardware acceleration in mind. Srini Devadas, Simon Langowski, Nikola Samardzic, Sacha Servan-Schreiber, Daniel Sánchez 0003 |
CCS | 1 |
| 2022 | CraterLake: a hardware accelerator for efficient unbounded computation on encrypted dataabstractFully Homomorphic Encryption (FHE) enables offloading computation to untrusted servers with cryptographic privacy. Despite its attractive security, FHE is not yet widely adopted due to its prohibitive overheads, about 10,000X over unencrypted computation. Recent FHE accelerators have made strides to bridge this performance gap. Unfortunately, prior accelerators only work well for simple programs, but become inefficient for complex programs, which bring additional costs and challenges. Nikola Samardzic, Axel Feldmann, Aleksandar Krastev, Nathan Manohar, Nicholas Genise, Srini Devadas, Karim M. El Defrawy, Chris Peikert, Daniel Sánchez 0003 |
ISCA | 6 |
| 2022 | Spectrum: High-bandwidth Anonymous Broadcast
Zachary Newman, Sacha Servan-Schreiber, Srini Devadas |
NSDI | 3 |
| 2022 | Litmus: Towards a Practical Database Management System with Verifiable ACID Properties and Transaction CorrectnessabstractExisting secure database management systems (DBMSs) focus on security and privacy of data but overlook semantic properties, such as the correctness and ACID properties of transactions. Enforcing these properties is crucial to the functionality of applications. If these guarantees do not hold, catastrophic losses could result. Yu Xia 0005, Xiangyao Yu, Matthew Butrovich, Andrew Pavlo, Srini Devadas |
SIGMOD Conference | 5 |
| 2022 | ShorTor: Improving Tor Network Latency via Multi-hop Overlay RoutingabstractWe present ShorTor, a protocol for reducing latency on the Tor network. ShorTor uses multi-hop overlay routing, a technique typically employed by content delivery networks, to influence the route Tor traffic takes across the internet. In this way, ShorTor avoids slow paths and improves the experience for end users by reducing the latency of their connections while imposing minimal bandwidth overhead. ShorTor functions as an overlay on top of onion routing—Tor’s existing routing protocol—and is run by Tor relays, making it independent of the path selection performed by Tor clients. As such, ShorTor reduces latency while preserving Tor’s existing security properties. Specifically, the routes taken in ShorTor are in no way correlated to either the Tor user or their destination, including the geographic location of either party. We analyze the security of ShorTor using the AnoA framework, showing that ShorTor maintains all of Tor’s anonymity guarantees. We augment our theoretical claims with an empirical analysis. To evaluate ShorTor’s performance, we collect a real-world dataset of over 400,000 latency measurements between the 1,000 most popular Tor relays, which collectively see the vast majority of Tor traffic. With this data, we identify pairs of relays that could benefit from ShorTor: that is, two relays where introducing an additional intermediate network hop results in lower latency than the direct route between them. We use our measurement dataset to simulate the impact on end users by applying ShorTor to two million Tor circuits chosen according to Tor’s specification. ShorTor reduces the latency for the 99thpercentile of relay pairs in Tor by 148ms. Similarly, ShorTor reduces the latency of Tor circuits by 122ms at the 99thpercentile. In practice, this translates to ShorTor truncating tail latencies for Tor which has a direct impact on page load times and, consequently, user experience on the Tor browser. Kyle Hogan, Sacha Servan-Schreiber, Zachary Newman, Ben Weintraub, Cristina Nita-Rotaru, Srini Devadas |
SP | 6 |
| 2022 | Private Approximate Nearest Neighbor Search with Sublinear CommunicationabstractNearest neighbor search is a fundamental building-block for a wide range of applications. A privacy-preserving protocol for nearest neighbor search involves a set of clients who send queries to a remote database. Each client retrieves the nearest neighbor(s) to its query in the database without revealing any information about the query. To ensure database privacy, clients must learn as little as possible beyond the query answer, even if behaving maliciously by deviating from protocol. Existing protocols for private nearest neighbor search require heavy cryptographic tools, resulting in high computational and bandwidth overheads. In this paper, we present the first lightweight protocol for private nearest neighbor search. Our protocol is instantiated using two non-colluding servers, each holding a replica of the database. Our design supports an arbitrary number of clients simultaneously querying the database through the two servers. Each query consists of a single round of communication between the client and the two servers. No communication is required between the servers to answer queries. If at least one of the servers is non-colluding, we ensure that (1) no information is revealed on the client’s query, (2) the total communication between the client and the servers is sublinear in the database size, and (3) each query answer only leaks a small and bounded amount of information about the database to the client, even if the client is malicious. We implement our protocol and report its performance on real-world data. Our construction requires between 10 and 20 seconds of query latency over large databases of 10M feature vectors. Client overhead remained under 10ms of processing time per query and less than 10MB of communication. Sacha Servan-Schreiber, Simon Langowski, Srini Devadas |
SP | 3 |
| 2021 | Robomorphic computing: a design methodology for domain-specific accelerators parameterized by robot morphologyabstractRobotics applications have hard time constraints and heavy computational burdens that can greatly benefit from domain-specific hardware accelerators. For the latency-critical problem of robot motion planning and control, there exists a performance gap of at least an order of magnitude between joint actuator response rates and state-of-the-art software solutions. Hardware acceleration can close this gap, but it is essential to define automated hardware design flows to keep the design process agile as applications and robot platforms evolve. To address this challenge, we introduce robomorphic computing: a methodology to transform robot morphology into a customized hardware accelerator morphology. We (i) present this design methodology, using robot topology and structure to exploit parallelism and matrix sparsity patterns in accelerator hardware; (ii) use the methodology to generate a parameterized accelerator design for the gradient of rigid body dynamics, a key kernel in motion planning; (iii) evaluate FPGA and synthesized ASIC implementations of this accelerator for an industrial manipulator robot; and (iv) describe how the design can be automatically customized for other robot models. Our FPGA accelerator achieves speedups of 8× and 86× over CPU and GPU when executing a single dynamics gradient computation. It maintains speedups of 1.9× to 2.9× over CPU and GPU, including computation and I/O round-trip latency, when deployed as a coprocessor to a host CPU for processing multiple dynamics gradient computations. ASIC synthesis indicates an additional 7.2× speedup for single computation latency. We describe how this principled approach generalizes to more complex robot platforms, such as quadrupeds and humanoids, as well as to other computational kernels in robotics, outlining a path forward for future robomorphic computing accelerators. Sabrina M. Neuman, Brian Plancher, Thomas Bourgeat, Thierry Tambe, Srini Devadas, Vijay Janapa Reddi |
ASPLOS | 5 |
| 2021 | F1: A Fast and Programmable Accelerator for Fully Homomorphic EncryptionabstractFully Homomorphic Encryption (FHE) allows computing on encrypted data, enabling secure offloading of computation to untrusted servers. Though it provides ideal security, FHE is expensive when executed in software, 4 to 5 orders of magnitude slower than computing on unencrypted data. These overheads are a major barrier to FHE’s widespread adoption. Nikola Samardzic, Axel Feldmann, Aleksandar Krastev, Srini Devadas, Ronald G. Dreslinski, Chris Peikert, Daniel Sánchez 0003 |
MICRO | 4 |
| 2020 | On Differentially Private Stochastic Convex Optimization with Heavy-tailed DataabstractIn this paper, we consider the problem of designing Differentially Private (DP) algorithms for Stochastic Convex Optimization (SCO) on heavy-tailed data. The irregularity of such data violates some key assumptions used in almost all existing DP-SCO and DP-ERM methods, resulting in failure to provide the DP guarantees. To better understand this type of challenges, we provide in this paper a comprehensive study of DP-SCO under various settings. First, we consider the case where the loss function is strongly convex and smooth. For this case, we propose a method based on the sample-and-aggregate framework, which has an excess population risk of $\tilde{O}(\frac{d^3}{n\epsilon^4})$ (after omitting other factors), where $n$ is the sample size and $d$ is the dimensionality of the data. Then, we show that with some additional assumptions on the loss functions, it is possible to reduce the \emph{expected} excess population risk to $\tilde{O}(\frac{ d^2}{ n\epsilon^2 })$. To lift these additional conditions, we also provide a gradient smoothing and trimming based scheme to achieve excess population risks of $\tilde{O}(\frac{ d^2}{n\epsilon^2})$ and $\tilde{O}(\frac{d^\frac{2}{3}}{(n\epsilon^2)^\frac{1}{3}})$ for strongly convex and general convex loss functions, respectively, \emph{with high probability}. Experiments on both synthetic and real-world datasets suggest that our algorithms can effectively deal with the challenges caused by data irregularity. Di Wang 0015, Hanshen Xiao, Srini Devadas, Jinhui Xu 0001 |
ICML | 3 |
| 2020 | XRD: Scalable Messaging System with Cryptographic Privacy
Albert Kwon, David Lu, Srini Devadas |
NSDI | 3 |
| 2020 | Towards Scalable Threshold CryptosystemsabstractThe resurging interest in Byzantine fault tolerant systems will demand more scalable threshold cryptosystems. Unfortunately, current systems scale poorly, requiring time quadratic in the number of participants. In this paper, we present techniques that help scale threshold signature schemes (TSS), verifiable secret sharing (VSS) and distributed key generation (DKG) protocols to hundreds of thousands of participants and beyond. First, we use efficient algorithms for evaluating polynomials at multiple points to speed up computing Lagrange coefficients when aggregating threshold signatures. As a result, we can aggregate a 130,000 out of 260,000 BLS threshold signature in just 6 seconds (down from 30 minutes). Second, we show how "authenticating" such multipoint evaluations can speed up proving polynomial evaluations, a key step in communication-efficient VSS and DKG protocols. As a result, we reduce the asymptotic (and concrete) computational complexity of VSS and DKG protocols from quadratic time to quasilinear time, at a small increase in communication complexity. For example, using our DKG protocol, we can securely generate a key for the BLS scheme above in 2.3 hours (down from 8 days). Our techniques improve performance for thresholds as small as 255 and generalize to any Lagrange-based threshold scheme, not just threshold signatures. Our work has certain limitations: we require a trusted setup, we focus on synchronous VSS and DKG protocols and we do not address the worst-case complaint overhead in DKGs. Nonetheless, we hope it will spark new interest in designing large-scale distributed systems. Alin Tomescu, Ittai Abraham, Benny Pinkas, Guy Golan-Gueta, Srini Devadas |
SP | 7 |
| 2020 | Round-Efficient Byzantine Broadcast Under Strongly Adaptive and Majority Corruptions
Jun Wan 0008, Hanshen Xiao, Srini Devadas, Elaine Shi |
TCC (1) | 3 |
| 2020 | Expected Constant Round Byzantine Broadcast Under Dishonest Majority
Jun Wan 0008, Hanshen Xiao, Elaine Shi, Srini Devadas |
TCC (1) | 4 |
| 2020 | Taurus: Lightweight Parallel Logging for In-Memory Database Management SystemsabstractExisting single-stream logging schemes are unsuitable for in-memory database management systems (DBMSs) as the single log is often a performance bottleneck. To overcome this problem, we present Taurus, an efficient parallel logging scheme that uses multiple log streams, and is compatible with both data and command logging. Taurus tracks and encodes transaction dependencies using a vector of log sequence numbers (LSNs). These vectors ensure that the dependencies are fully captured in logging and correctly enforced in recovery. Our experimental evaluation with an in-memory DBMS shows that Taurus's parallel logging achieves up to 9.9X and 2.9X speedups over single-streamed data logging and command logging, respectively. It also enables the DBMS to recover up to 22.9X and 75.6X faster than these baselines for data and command logging, respectively. We also compare Taurus with two state-of-the-art parallel logging schemes and show that the DBMS achieves up to 2.8X better performance on NVMe drives and 9.2X on HDDs. Yu Xia 0005, Xiangyao Yu, Andrew Pavlo, Srini Devadas |
Proc. VLDB Endow. | 4 |
| 2020 | A Retrospective on Path ORAMabstractPath oblivious RAM (ORAM) is an ORAM protocol that simultaneously enjoys simplicity and efficiency. As a result, it holds promise to provide cryptographic-grade and practical access pattern protection in multiple application domains, including but not limited to secure hardware. In this paper, we review Path ORAM's key ideas and contribution, summarize its impact and subsequent works, and discuss future directions. Emil Stefanov, Marten van Dijk, Elaine Shi, Christopher W. Fletcher, Ling Ren 0001, Xiangyao Yu, Srini Devadas |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 7 |
| 2019 | Transparency Logs via Append-Only Authenticated DictionariesabstractTransparency logs allow users to audit a potentially malicious service, paving the way towards a more accountable Internet. For example, Certificate Transparency (CT) enables domain owners to audit Certificate Authorities (CAs) and detect impersonation attacks. Yet, to achieve their full potential, transparency logs must be bandwidth-efficient when queried by users. Specifically, everyone should be able to efficientlylook up log entries by their keyand efficiently verify that the log remainsappend-only. Unfortunately, without additional trust assumptions, current transparency logs cannot provide both small-sizedlookup proofs and small-sizedappend-only proofs. In fact, one of the proofs always requires bandwidth linear in the size of the log, making it expensive for everyone to query the log. In this paper, we address this gap with a new primitive called anappend-only authenticated dictionary (AAD). Our construction is the first to achieve (poly)logarithmic size for both proof types and helps reduce bandwidth consumption in transparency logs. This comes at the cost of increased append times and high memory usage, both of which remain to be improved to make practical deployment possible. Alin Tomescu, Vivek Bhupatiraju, Dimitrios Papadopoulos 0001, Charalampos Papamanthou, Nikos Triandopoulos, Srini Devadas |
CCS | 6 |
| 2019 | Sanctorum: A lightweight security monitor for secure enclavesabstractEnclaves have emerged as a particularly compelling primitive to implement trusted execution environments: strongly isolated sensitive user-mode processes in a largely untrusted software environment. While the threat models employed by various enclave systems differ, the high-level guarantees they offer are essentially the same: attestation of an enclave's initial state, as well as a guarantee of enclave integrity and privacy in the presence of an adversary.This work describes Sanctorum, a small trusted code base (TCB), consisting of a generic enclave-capable system, which is sufficient to implement secure enclaves akin to the primitive offered by Intel's SGX. While enclaves may be implemented via unconditionally trusted hardware and microcode, as it is the case in SGX, we employ a smaller TCB principally consisting of authenticated, privileged software, which may be replaced or patched as needed. Sanctorum implements a formally verified specification for generic enclaves on an in-order multiprocessor system meeting baseline security requirements, e.g., the MIT Sanctum processor and the Keystone enclave framework. Sanctorum requires trustworthy hardware including a random number generator, a private cryptographic key pair derived via a secure bootstrapping protocol, and a robust isolation primitive to safeguard sensitive information. Sanctorum's threat model is informed by the threat model of the isolation primitive, and is suitable for adding enclaves to a variety of processor systems. Ilia A. Lebedev, Kyle Hogan, Jules Drean, David Kohlbrenner, Dayeol Lee, Krste Asanovic, Dawn Song, Srini Devadas |
DATE | 8 |
| 2019 | Benchmarking and Workload Analysis of Robot Dynamics AlgorithmsabstractRigid body dynamics calculations are needed for many tasks in robotics, including online control. While there currently exist several competing software implementations that are sufficient for use in traditional control approaches, emerging sophisticated motion control techniques such as nonlinear model predictive control demand orders of magnitude more frequent dynamics calculations. Current software solutions are not fast enough to meet that demand for complex robots. The goal of this work is to examine the performance of current dynamics software libraries in detail. In this paper, we (i) survey current state-of-the-art software implementations of the key rigid body dynamics algorithms (RBDL, Pinocchio, Rigid-BodyDynamics.jl, and RobCoGen), (ii) establish a methodology for benchmarking these algorithms, and (iii) characterize their performance through real measurements taken on a modern hardware platform. With this analysis, we aim to provide direction for future improvements that will need to be made to enable emerging techniques for real-time robot motion control. To this end, we are also releasing our suite of benchmarks to enable others to help contribute to this important task. Sabrina M. Neuman, Twan Koolen, Jules Drean, Jason E. Miller, Srini Devadas |
IROS | 5 |
| 2019 | MI6: Secure Enclaves in a Speculative Out-of-Order ProcessorabstractRecent attacks have broken process isolation by exploiting microarchitectural side channels that allow indirect access to shared microarchitectural state. Enclaves strengthen the process abstraction to restore isolation guarantees. Thomas Bourgeat, Ilia A. Lebedev, Andrew Wright, Sizhuo Zhang, Arvind 0001, Srini Devadas |
MICRO | 6 |
| 2019 | Var-CNN: A Data-Efficient Website Fingerprinting Attack Based on Deep LearningabstractAbstract In recent years, there have been several works that use website fingerprinting techniques to enable a local adversary to determine which website a Tor user visits. While the current state-of-the-art attack, which uses deep learning, outperforms prior art with medium to large amounts of data, it attains marginal to no accuracy improvements when both use small amounts of training data. In this work, we propose Var-CNN, a website fingerprinting attack that leverages deep learning techniques along with novel insights specific to packet sequence classification. In open-world settings with large amounts of data, Var-CNN attains over 1% higher true positive rate (TPR) than state-of-the-art attacks while achieving 4× lower false positive rate (FPR). Var-CNN’s improvements are especially notable in low-data scenarios, where it reduces the FPR of prior art by 3.12% while increasing the TPR by 13%. Overall, insights used to develop Var-CNN can be applied to future deep learning based attacks, and substantially reduce the amount of training data needed to perform a successful website fingerprinting attack. This shortens the time needed for data collection and lowers the likelihood of having data staleness issues. Sanjit Bhat, David Lu, Albert Kwon, Srini Devadas |
Proc. Priv. Enhancing Technol. | 4 |
| 2019 | Design and Implementation of the Ascend Secure ProcessorabstractThis paper presents post-silicon results for the Ascend secure processor, taped out in a 32 nm SOI process. Ascend prevents information leakage over a processor's digital I/O pins—in particular, the processor's requests to external memory—and certifies the program's execution by verifying the integrity of the external memory. In secure processor design, encrypting main memory is not sufficient for security becausewhereandwhenmemory is accessed reveals secret information. To this end, Ascend is equipped with a hardware Oblivious RAM (ORAM) controller, which obfuscates the address bus by reshuffling memory as it is accessed. To our knowledge, Ascend is the first prototyping of ORAM in custom silicon. Ascend has also been carefully engineered to ensure its timing behaviors are independent of user private data. In 32 nm silicon, all security components combined (the ORAM controller, which includes 12 AES rounds and one SHA-3 hash unit) impose a moderate area overhead of 0.51 mm$^2$. Post tape-out, the security components of the Ascend chip have been successfully tested at 857 MHz and 1.1 V, at which point they consume 299 mW of power. Ling Ren 0001, Christopher W. Fletcher, Albert Kwon, Marten van Dijk, Srini Devadas |
IEEE Trans. Dependable Secur. Comput. | 5 |
| 2018 | Invited Paper: Secure Boot and Remote Attestation in the Sanctum ProcessorabstractDuring the secure boot process for a trusted execution environment, the processor must provide a chain of certificates to the remote client demonstrating that their secure container was established as specified. This certificate chain is rooted at the hardware manufacturer who is responsible for constructing chips according to the correct specification and provisioning them with key material. We consider a semi-honest manufacturer who is assumed to construct chips correctly, but may attempt to obtain knowledge of client private keys during the process. Using the RISC-V Rocket chip architecture as a base, we design, document, and implement an attested execution processor that does not require secure non-volatile memory, nor a private key explicitly assigned by the manufacturer. Instead, the processor derives its cryptographic identity from manufacturing variation measured by a Physical Unclonable Function (PUF). Software executed by a bootloader built into the processor transforms the PUF output into an elliptic curve key pair. The (re)generated private key is used to sign trusted portions of the boot image, and is immediately destroyed. The platform can therefore provide attestations about its state to remote clients. Reliability and security of PUF keys are ensured through the use of a trapdoor computational fuzzy extractor. We present detailed evaluation results for secure boot and attestation by a client of a Rocket chip implementation on a Xilinx Zynq 7000 FPGA. Ilia Lebedev, Kyle Hogan, Srini Devadas |
CSF | 3 |
| 2018 | Secure High-Performance Computer Architectures: Challenges and OpportunitiesabstractSummary form only given. Recent work has shown that architectural isolation can be violated through software side channel attacks that exploit microarchitectural performance optimizations such as speculation to leak secrets. While turning off microarchitectural optimizations can preclude some classes of attacks, we argue that performance and security do not have be in conflict, provided processors are designed with security in mind. We espouse a principled approach to eliminating entire attack surfaces through microarchitectural isolation, rather than plugging attack-specific privacy leaks. We argue that minimal modifications to hardware can defend against all currently-practical side channel attacks and without significant performance impact. As an application of this approach, we describe the Sanctum processor architecture that offers strong provable isolation of software modules running concurrently and sharing resources, and Sanctoom, a speculative, out-of-order variant with similar properties. These processors provide isolation even when large parts of the operating system are compromised, and their open-source implementations allow security properties to be independently verified. Srini Devadas |
HiPC | 1 |
| 2018 | DAWG: A Defense Against Cache Timing Attacks in Speculative Execution ProcessorsabstractSoftware side channel attacks have become a serious concern with the recent rash of attacks on speculative processor architectures. Most attacks that have been demonstrated exploit the cache tag state as their exfiltration channel. While many existing defense mechanisms that can be implemented solely in software have been proposed, these mechanisms appear to patch specific attacks, and can be circumvented. In this paper, we propose minimal modifications to hardware to defend against a broad class of attacks, including those based on speculation, with the goal of eliminating the entire attack surface associated with the cache state covert channel. We propose DAWG, Dynamically Allocated Way Guard, a generic mechanism for secure way partitioning of set associative structures including memory caches. DAWG endows a set associative structure with a notion of protection domains to provide strong isolation. When applied to a cache, unlike existing quality of service mechanisms such as Intel's Cache Allocation Technology (CAT), DAWG fully isolates hits, misses, and metadata updates across protection domains. We describe how DAWG can be implemented on a processor with minimal modifications to modern operating systems. We describe a non-interference property that is orthogonal to speculative execution and therefore argue that existing attacks such as Spectre Variant 1 and 2 will not work on a system equipped with DAWG. Finally, we evaluate the performance impact of DAWG on the cache subsystem. Vladimir Kiriansky, Ilia A. Lebedev, Saman P. Amarasinghe, Srini Devadas, Joel S. Emer |
MICRO | 4 |
| 2018 | Path ORAM: An Extremely Simple Oblivious RAM ProtocolabstractWe present Path ORAM, an extremely simple Oblivious RAM protocol with a small amount of client storage. Partly due to its simplicity, Path ORAM is the most practical ORAM scheme known to date with small client storage. We formally prove that Path ORAM has a O (log N ) bandwidth cost for blocks of size B = Ω (log 2 N ) bits. For such block sizes, Path ORAM is asymptotically better than the best-known ORAM schemes with small client storage. Due to its practicality, Path ORAM has been adopted in the design of secure processors since its proposal. Emil Stefanov, Marten van Dijk, Elaine Shi, T.-H. Hubert Chan, Christopher W. Fletcher, Ling Ren 0001, Xiangyao Yu, Srini Devadas |
J. ACM | 8 |
| 2018 | Sundial: Harmonizing Concurrency Control and Caching in a Distributed OLTP Database Management SystemabstractDistributed transactions suffer from poor performance due to two major limiting factors. First, distributed transactions suffer from high latency because each of their accesses to remote data incurs a long network delay. Second, this high latency increases the likelihood of contention among distributed transactions, leading to high abort rates and low performance. We present Sundial , an in-memory distributed optimistic concurrency control protocol that addresses these two limitations. First, to reduce the transaction abort rate, Sundial dynamically determines the logical order among transactions at runtime, based on their data access patterns. Sundial achieves this by applying logical leases to each data element, which allows the database to dynamically calculate a transaction's logical commit timestamp. Second, to reduce the overhead of remote data accesses, Sundial allows the database to cache remote data in a server's local main memory and maintains cache coherence. With logical leases, Sundial integrates concurrency control and cache coherence into a simple unified protocol. We evaluate Sundial against state-of-the-art distributed concurrency control protocols. Sundial outperforms the next-best protocol by up to 57% under high contention. Sundial's caching scheme improves performance by up to 4.6× in workloads with high access skew. Xiangyao Yu, Yu Xia 0005, Andrew Pavlo, Daniel Sánchez 0003, Larry Rudolph, Srini Devadas |
Proc. VLDB Endow. | 6 |
| 2017 | A Formal Foundation for Secure Remote Execution of EnclavesabstractRecent proposals for trusted hardware platforms, such as Intel SGX and the MIT Sanctum processor, offer compelling security features but lack formal guarantees. We introduce a verification methodology based on a trusted abstract platform (TAP), a formalization of idealized enclave platforms along with a parameterized adversary. We also formalize the notion of secure remote execution and present machine-checked proofs showing that the TAP satisfies the three key security properties that entail secure remote execution: integrity, confidentiality and secure measurement. We then present machine-checked proofs showing that SGX and Sanctum are refinements of the TAP under certain parameterizations of the adversary, demonstrating that these systems implement secure enclaves for the stated adversary models. Pramod Subramanyan, Rohit Sinha 0001, Ilia A. Lebedev, Srini Devadas, Sanjit A. Seshia |
CCS | 4 |
| 2017 | Using Application-Level Thread Progress Information to Manage Power and PerformanceabstractPower and thermal limitations make it impossible to run all cores on a multicore system at their maximum frequency. Therefore, modern systems require careful power management. These systems must manage complex tradeoffs between energy, power, and frequency, choosing which cores to accelerate to achieve good performance while maintaining energy efficiency or operating under a power budget. Navigating these tradeoffs is especially hard with multi-threaded applications, where performance depends on the relative progress of parallel worker threads between synchronization points. Prior work on chip-level power management for multi-threaded applications has largely relied on indirect heuristics and metrics calculated from low-level performance counters to estimate each thread's progress. However, these indirect metrics are often inaccurate. Instead, we propose to gather progress information directly from software itself. We present ThreadBeats, a simple application-level annotation framework that directly and accurately conveys thread progress information to hardware. We design DVFS controllers that exploit ThreadBeats information for two purposes: (i) improving performance by equalizing thread progress and (ii) minimizing runtime under a power budget constraint. These controllers reduce wait time at barriers by 77% on average and improve energy-delay product under a power budget by 23% over prior work. Sabrina M. Neuman, Jason E. Miller, Daniel Sánchez 0003, Srini Devadas |
ICCD | 4 |
| 2017 | Banshee: bandwidth-efficient DRAM caching via software/hardware cooperationabstractPlacing the DRAM in the same package as a processor enables several times higher memory bandwidth than conventional off-package DRAM. Yet, the latency of in-package DRAM is not appreciably lower than that of off-package DRAM. A promising use of in-package DRAM is as a large cache. Unfortunately, most previous DRAM cache designs optimize mainly for cache hit latency and do not consider bandwidth efficiency as a first-class design constraint. Hence, as we show in this paper, these designs are suboptimal for use with in-package DRAM. Xiangyao Yu, Christopher J. Hughes, Nadathur Satish, Onur Mutlu, Srini Devadas |
MICRO | 5 |
| 2017 | Leveraging Hardware Isolation for Process Level Access Control & AuthenticationabstractCritical resource sharing among multiple entities in a processing system is inevitable, which in turn calls for the presence of appropriate authentication and access control mechanisms. Generally speaking, these mechanisms are implemented via trusted software "policy checkers" that enforce certain high level application-specific "rules" to enforce a policy. Whether implemented as operating system modules or embedded inside the application ad hoc, these policy checkers expose additional attack surface in addition to the application logic. In order to protect application software from an adversary, modern secure processing platforms, such as Intel's Software Guard Extensions (SGX), employ principled hardware isolation to offer secure software containers or enclaves to execute trusted sensitive code with some integrity and privacy guarantees against a privileged software adversary. We extend this model further and propose using these hardware isolation mechanisms to shield the authentication and access control logic essential to policy checker software. While relying on the fundamental features of modern secure processors, our framework introduces productive software design guidelines which enable a guarded environment to execute sensitive policy checking code - hence enforcing application control flow integrity - and afford flexibility to the application designer to construct appropriate high-level policies to customize policy checker software. Syed Kamran Haider, Hamza Omar, Ilia A. Lebedev, Srini Devadas, Marten van Dijk |
SACMAT | 4 |
| 2017 | Atom: Horizontally Scaling Strong AnonymityabstractAtom is an anonymous messaging system that protects against traffic-analysis attacks. Unlike many prior systems, each Atom server touches only a small fraction of the total messages routed through the network. As a result, the system's capacity scales near-linearly with the number of servers. At the same time, each Atom user benefits from "best possible" anonymity: a user is anonymous among all honest users of the system, even against an active adversary who monitors the entire network, a portion of the system's servers, and any number of malicious users. The architectural ideas behind Atom have been known in theory, but putting them into practice requires new techniques for (1) avoiding heavy general-purpose multi-party computation protocols, (2) defeating active attacks by malicious servers at minimal performance cost, and (3) handling server failure and churn. Albert Kwon, Henry Corrigan-Gibbs, Srini Devadas, Bryan Ford |
SOSP | 3 |
| 2017 | Catena: Efficient Non-equivocation via BitcoinabstractWe present Catena, an efficiently-verifiable Bitcoin witnessing scheme. Catena enables any number of thin clients, such as mobile phones, to efficiently agree on a log of application-specific statements managed by an adversarial server. Catena implements a log as an OP_RETURN transaction chain andprevents forks in the log by leveraging Bitcoin's security againstdouble spends. Specifically, if a log server wants to equivocate ithas to double spend a Bitcoin transaction output. Thus, Catena logs are as hard to fork as the Bitcoin blockchain: an adversarywithout a large fraction of the network's computational power cannot fork Bitcoin and thus cannot fork a Catena log either. However, different from previous Bitcoin-based work, Catena decreases the bandwidth requirements of log auditors from 90GB to only tens of megabytes. More precisely, our clients only need to download all Bitcoin block headers (currently less than35 MB) and a small, 600-byte proof for each statement in a block. We implement Catena in Java using the bitcoinj library and use itto extend CONIKS, a recent key transparency scheme, to witnessits public-key directory in the Bitcoin blockchain where it can beefficiently verified by auditors. We show that Catena can secure many systems today, such as public-key directories, Tor directory servers and software transparency schemes. Alin Tomescu, Srini Devadas |
IEEE Symposium on Security and Privacy | 2 |
| 2017 | Bandwidth Hard Functions for ASIC Resistance
Ling Ren 0001, Srini Devadas |
TCC (1) | 2 |
| 2017 | On Iterative Collision Search for LPN and Subset Sum
Srini Devadas, Ling Ren 0001, Hanshen Xiao |
TCC (2) | 1 |
| 2017 | Brief Announcement: Practical Synchronous Byzantine ConsensusabstractThis paper presents new protocols for Byzantine state machine replication and Byzantine agreement in the synchronous and authenticated setting. The PBFT state machine replication protocol tolerates f Byzantine faults in an asynchronous setting using n = 3f + 1 replicas. We improve the Byzantine fault tolerance to n = 2f + 1 by utilizing the synchrony assumption. Our protocol also solves synchronous authenticated Byzantine agreement in fewer expected rounds than the best existing solution (Katz and Koo, 2006). Ittai Abraham, Srini Devadas, Kartik Nayak, Ling Ren 0001 |
DISC | 2 |
| 2017 | PriviPK: Certificate-less and secure email communication
Mashael Al Sabah, Alin Tomescu, Ilia A. Lebedev, Dimitrios Serpanos, Srini Devadas |
Comput. Secur. | 5 |
| 2017 | Trapdoor Computational Fuzzy Extractors and Stateless Cryptographically-Secure Physical Unclonable FunctionsabstractWe present a fuzzy extractor whose security can be reduced to the hardness of Learning Parity with Noise (LPN) and can efficiently correct a constant fraction of errors in a biometric source with a “noise-avoiding trapdoor.” Using this computational fuzzy extractor, we present a stateless construction of a cryptographically-secure Physical Unclonable Function. Our construct requires no non-volatile (permanent) storage, secure or otherwise, and its computational security can be reduced to the hardness of an LPN variant under the random oracle model. The construction is “stateless,” because there is no information stored between subsequent queries, which mitigates attacks against the PUF via tampering. Moreover, our stateless construction corresponds to a PUF whose outputs are free of noise because of internal error-correcting capability, which enables a host of applications beyond authentication. We describe the construction, provide a proof of computational security, analysis of the security parameter for system parameter choices, and present experimental evidence that the construction is practical and reliable under a wide environmental range. Charles Herder, Ling Ren 0001, Marten van Dijk, Meng-Day (Mandel) Yu, Srini Devadas |
IEEE Trans. Dependable Secur. Comput. | 5 |
| 2016 | Tardis 2.0: Optimized Time Traveling Coherence for Relaxed Consistency ModelsabstractCache coherence scalability is a big challenge in shared memory systems. Traditional protocols do not scale due to the storage and traffic overhead of cache invalidation. Tardis, a recently proposed coherence protocol, removes cache invalidation using logical timestamps and achieves excellent scalability. The original Tardis protocol, however, only supports the Sequential Consistency (SC) memory model, limiting its applicability. Tardis also incurs extra network traffic on some benchmarks due to renew messages, and has suboptimal performance when the program uses spinning to communicate between threads. Xiangyao Yu, Ethan Zou, Srini Devadas |
PACT | 4 |
| 2016 | TicToc: Time Traveling Optimistic Concurrency ControlabstractConcurrency control for on-line transaction processing (OLTP) database management systems (DBMSs) is a nasty game. Achieving higher performance on emerging many-core systems is difficult. Previous research has shown that timestamp management is the key scalability bottleneck in concurrency control algorithms. This prevents the system from scaling to large numbers of cores. In this paper we present TicToc, a new optimistic concurrency control algorithm that avoids the scalability and concurrency bottlenecks of prior T/O schemes. TicToc relies on a novel and provably correct data-driven timestamp management protocol. Instead of assigning timestamps to transactions, this protocol assigns read and write timestamps to data items and uses them to lazily compute a valid commit timestamp for each transaction. TicToc removes the need for centralized timestamp allocation, and commits transactions that would be aborted by conventional T/O schemes. We implemented TicToc along with four other concurrency control algorithms in an in-memory, shared-everything OLTP DBMS and compared their performance on different workloads. Our results show that TicToc achieves up to 92% better throughput while reducing the abort rate by 3.3x over these previous algorithms. Xiangyao Yu, Andrew Pavlo, Daniel Sánchez 0003, Srini Devadas |
SIGMOD Conference | 4 |
| 2016 | Sanctum: Minimal Hardware Extensions for Strong Software Isolation
Victor Costan, Ilia A. Lebedev, Srini Devadas |
USENIX Security Symposium | 3 |
| 2016 | Riffle: An Efficient Communication System With Strong AnonymityabstractAbstract Existing anonymity systems sacrifice anonymity for efficient communication or vice-versa. Onion-routing achieves low latency, high bandwidth, and scalable anonymous communication, but is susceptible to traffic analysis attacks. Designs based on DC-Nets, on the other hand, protect the users against traffic analysis attacks, but sacrifice bandwidth. Verifiable mixnets maintain strong anonymity with low bandwidth overhead, but suffer from high computation overhead instead. In this paper, we present Riffle, a bandwidth and computation efficient communication system with strong anonymity. Riffle consists of a small set of anonymity servers and a large number of users, and guarantees anonymity among all honest clients as long as there exists at least one honest server. Riffle uses a new hybrid verifiable shuffle technique and private information retrieval for bandwidth- and computation-efficient anonymous communication. Our evaluation of Riffle in file sharing and microblogging applications shows that Riffle can achieve a bandwidth of over 100KB/s per user in an anonymity set of 200 users in the case of file sharing, and handle over 100,000 users with less than 10 second latency in the case of microblogging. Albert Kwon, David Lazar, Srini Devadas, Bryan Ford |
Proc. Priv. Enhancing Technol. | 3 |
| 2016 | LDAC: Locality-Aware Data Access Control for Large-Scale Multicore Cache HierarchiesabstractThe trend of increasing the number of cores to achieve higher performance has challenged efficient management of on-chip data. Moreover, many emerging applications process massive amounts of data with varying degrees of locality. Therefore, exploiting locality to improve on-chip traffic and resource utilization is of fundamental importance. Conventional multicore cache management schemes either manage the private cache (L1) or the Last-Level Cache (LLC), while ignoring the other. We propose a holistic locality-aware cache hierarchy management protocol for large-scale multicores. The proposed scheme improves on-chip data access latency and energy consumption by intelligently bypassing cache line replication in the L1 caches, and/or intelligently replicating cache lines in the LLC. The approach relies on low overhead yet highly accurate in-hardware runtime classification of data locality at both L1 cache and the LLC. The decision to bypass L1 and/or replicate in LLC is then based on the measured reuse at the fine granularity of cache lines. The locality tracking mechanism is decoupled from the sharer tracking structures that cause scalability concerns in traditional cache coherence protocols. Moreover, the complexity of the protocol is low since no additional coherence states are created. However, the proposed classifier incurs a 5.6 KB per-core storage overhead. On a set of parallel benchmarks, the locality-aware protocol reduces average energy consumption by 26% and completion time by 16%, when compared to the state-of-the-art Reactive-NUCA multicore cache management scheme. Qingchuan Shi, George Kurian, Farrukh Hijaz, Srini Devadas, Omer Khan |
ACM Trans. Archit. Code Optim. | 4 |
| 2016 | Locality-aware data replication in the last-level cache for large scale multicores
Farrukh Hijaz, Qingchuan Shi, George Kurian, Srini Devadas, Omer Khan |
J. Supercomput. | 4 |
| 2015 | OSPREY: Implementation of Memory Consistency Models for Cache Coherence Protocols involving Invalidation-Free Data AccessabstractData access in modern processors contributes significantly to the overall performance and energy consumption. Traditionally, data is distributed among the cores through an on-chip cache hierarchy, and each producer/consumer accesses data through its private level-1 cache relying on the cache coherence protocol for consistency. Recently, remote access, a mechanism that reduces energy and latency through word-level access to data anywhere on chip has been proposed. Remote access does not replicate data in the private caches, and thereby removes the need for expensive cache line invalidations or updates. Researchers have implemented remote access as an auxiliary mechanism in cache coherence to improve efficiency. Unfortunately, stronger memory models, such as Intel's TSO, require strict ordering among the loads and stores. This introduces serialization penalties for data classified to be accessed remotely, which hampers each core's ability to optimally exploit memory level parallelism. In this paper we propose a novel timestamp-based scheme to detect memory consistency violations. The proposed scheme enables remote accesses to be issued and completed in parallel while continuously detecting whether any ordering violations have occurred, and rolling back the pipeline state (if needed). We implement our scheme for the locality-aware cache coherence protocol that uses remote access as an auxiliary mechanism for efficient data access. Our evaluation using a 64-core multicore processor with out-of-order speculative cores shows that the proposed technique improves completion time by 26% and energy by 20% over a state-of-the-art cache management scheme. George Kurian, Qingchuan Shi, Srini Devadas, Omer Khan |
PACT | 3 |
| 2015 | Tardis: Time Traveling Coherence Algorithm for Distributed Shared MemoryabstractA new memory coherence protocol, Tardis, is proposed. Tardis uses timestamp counters representing logical time as well as physical time to order memory operations and enforce sequential consistency in any type of shared memory system. Tardis is unique in that as compared to the widely-adopted directory coherence protocol, and its variants, it completely avoids multicasting and only requires O(log N) storage per cache block for an N-core system rather than O(N) sharer information. Tardis is simpler and easier to reason about, yet achieves similar performance to directory protocols on a wide range of benchmarks run on 16, 64 and 256 cores. Xiangyao Yu, Srini Devadas |
PACT | 2 |
| 2015 | Freecursive ORAM: [Nearly] Free Recursion and Integrity Verification for Position-based Oblivious RAMabstractOblivious RAM (ORAM) is a cryptographic primitive that hides memory access patterns as seen by untrusted storage. Recently, ORAM has been architected into secure processors. A big challenge for hardware ORAM schemes is how to efficiently manage the Position Map (PosMap), a central component in modern ORAM algorithms. Implemented naively, the PosMap causes ORAM to be fundamentally unscalable in terms of on-chip area. On the other hand, a technique called Recursive ORAM fixes the area problem yet significantly increases ORAM's performance overhead. Christopher W. Fletcher, Ling Ren 0001, Albert Kwon, Marten van Dijk, Srini Devadas |
ASPLOS | 5 |
| 2015 | A Low-Latency, Low-Area Hardware Oblivious RAM ControllerabstractWe build and evaluate Tiny ORAM, an Oblivious RAM prototype on FPGA. Oblivious RAM is a cryptographic primitive that completely obfuscates an application's data, access pattern, and read/write behavior to/from external memory (such as DRAM or disk). Tiny ORAM makes two main contributions. First, by removing an algorithmic bottleneck in prior work, Tiny ORAM is the" first hardware ORAM design to support arbitrary block sizes (e.g., 64 Bytes to 4096 Bytes). With a 64 Byte block size, Tiny ORAM can " finish an access in 1:4us, over 40x faster than the prior-art implementation. Second, through novel algorithmic and engineering-level optimizations, Tiny ORAM reduces the number of symmetric encryption operations by ~ 3x compared to a prior work. Tiny ORAM is also the " first design to implement and report real numbers for the cost of symmetric encryption in hardware ORAM constructions. Putting it together, Tiny ORAM requires 18381 (5%) LUTs and 146 (13%) Block RAM on a Xilinx XC7VX485T FPGA, including the cost of encryption. Christopher W. Fletcher, Ling Ren 0001, Albert Kwon, Marten van Dijk, Emil Stefanov, Dimitrios Serpanos, Srini Devadas |
FCCM | 7 |
| 2015 | PrORAM: dynamic prefetcher for oblivious RAMabstractOblivious RAM (ORAM) is an established technique to hide the access pattern to an untrusted storage system. With ORAM, a curious adversary cannot tell what address the user is accessing when observing the bits moving between the user and the storage system. All existing ORAM schemes achieve obliviousness by adding redundancy to the storage system, i.e., each access is turned into multiple random accesses. Such redundancy incurs a large performance overhead. Xiangyao Yu, Syed Kamran Haider, Ling Ren 0001, Christopher W. Fletcher, Albert Kwon, Marten van Dijk, Srini Devadas |
ISCA | 7 |
| 2015 | IMP: indirect memory prefetcherabstractMachine learning, graph analytics and sparse linear algebra-based applications are dominated by irregular memory accesses resulting from following edges in a graph or non-zero elements in a sparse matrix. These accesses have little temporal or spatial locality, and thus incur long memory stalls and large bandwidth requirements. A traditional streaming or striding prefetcher cannot capture these irregular access patterns. Xiangyao Yu, Christopher J. Hughes, Nadathur Satish, Srini Devadas |
MICRO | 4 |
| 2015 | Circuit Fingerprinting Attacks: Passive Deanonymization of Tor Hidden Services
Albert Kwon, Mashael Al Sabah, David Lazar, Marc Dacier, Srini Devadas |
USENIX Security Symposium | 5 |
| 2015 | Constants Count: Practical Improvements to Oblivious RAM
Ling Ren 0001, Christopher W. Fletcher, Albert Kwon, Emil Stefanov, Elaine Shi, Marten van Dijk, Srini Devadas |
USENIX Security Symposium | 7 |
| 2014 | Suppressing the Oblivious RAM timing channel while making information leakage and program efficiency trade-offsabstractOblivious RAM (ORAM) is an established cryptographic technique to hide a program's address pattern to an untrusted storage system. More recently, ORAM schemes have been proposed to replace conventional memory controllers in secure processor settings to protect against information leakage in external memory and the processor I/O bus. Christopher W. Fletcher, Ling Ren 0001, Xiangyao Yu, Marten van Dijk, Omer Khan, Srini Devadas |
HPCA | 6 |
| 2014 | Locality-aware data replication in the Last-Level CacheabstractNext generation multicores will process massive data with varying degree of locality. Harnessing on-chip data locality to optimize the utilization of cache and network resources is of fundamental importance. We propose a locality-aware selective data replication protocol for the last-level cache (LLC). Our goal is to lower memory access latency and energy by replicating only high locality cache lines in the LLC slice of the requesting core, while simultaneously keeping the off-chip miss rate low. Our approach relies on low overhead yet highly accurate in-hardware run-time classification of data locality at the cache line granularity, and only allows replication for cache lines with high reuse. Furthermore, our classifier captures the LLC pressure at the existing replica locations and adapts its replication decision accordingly. The locality tracking mechanism is decoupled from the sharer tracking structures that cause scalability concerns in traditional coherence protocols. Moreover, the complexity of our protocol is low since no additional coherence states are created. On a set of parallel benchmarks, our protocol reduces the overall energy by 16%, 14%, 13% and 21% and the completion time by 4%, 9%, 6% and 13% when compared to the previously proposed Victim Replication, Adaptive Selective Replication, Reactive-NUCA and Static-NUCA LLC management schemes. George Kurian, Srini Devadas, Omer Khan |
HPCA | 2 |
| 2014 | Power modeling and other new features in the Graphite simulatorabstractThis paper described recent improvements to the Graphite simulator designed to help explore current and emerging research topics. With these improvements, Graphite is ideally suited to explore both power and performance in future multicore and manycore processors, especially those incorporating dynamic runtime monitoring and adaptation. Separate validation of Graphite has shown performance results within about 6% on average (18% worst case) of a cycle-level simulator and normalized power trends are predicted to within 10%. This makes Graphite accurate enough for medium- to long-term studies while maintaining very high performance. Graphite is freely available for anyone to use: http://graphite.csail.mit.edu. George Kurian, Sabrina M. Neuman, George Bezerra, Anthony Giovinazzo, Srini Devadas, Jason E. Miller |
ISPASS | 5 |
| 2014 | Physical Unclonable Functions and Applications: A TutorialabstractThis paper describes the use of physical unclonable functions (PUFs) in low-cost authentication and key generation applications. First, it motivates the use of PUFs versus conventional secure nonvolatile memories and defines the two primary PUF types: “strong PUFs” and “weak PUFs.” It describes strong PUF implementations and their use for low-cost authentication. After this description, the paper covers both attacks and protocols to address errors. Next, the paper covers weak PUF implementations and their use in key generation applications. It covers error-correction schemes such as pattern matching and index-based coding. Finally, this paper reviews several emerging concepts in PUF technologies such as public model PUFs and new PUF implementation technologies. Charles Herder, Meng-Day (Mandel) Yu, Farinaz Koushanfar, Srini Devadas |
Proc. IEEE | 4 |
| 2014 | Staring into the Abyss: An Evaluation of Concurrency Control with One Thousand CoresabstractComputer architectures are moving towards an era dominated by many-core machines with dozens or even hundreds of cores on a single chip. This unprecedented level of on-chip parallelism introduces a new dimension to scalability that current database management systems (DBMSs) were not designed for. In particular, as the number of cores increases, the problem of concurrency control becomes extremely challenging. With hundreds of threads running in parallel, the complexity of coordinating competing accesses to data will likely diminish the gains from increased core counts. To better understand just how unprepared current DBMSs are for future CPU architectures, we performed an evaluation of concurrency control for on-line transaction processing (OLTP) workloads on many-core chips. We implemented seven concurrency control algorithms on a main-memory DBMS and using computer simulations scaled our system to 1024 cores. Our analysis shows that all algorithms fail to scale to this magnitude but for different reasons. In each case, we identify fundamental bottlenecks that are independent of the particular database implementation and argue that even state-of-the-art DBMSs suffer from these limitations. We conclude that rather than pursuing incremental solutions, many-core chips may require a completely redesigned DBMS architecture that is built from ground up and is tightly coupled with the hardware. Xiangyao Yu, George Bezerra, Andrew Pavlo, Srini Devadas, Michael Stonebraker |
Proc. VLDB Endow. | 4 |
| 2013 | Path ORAM: an extremely simple oblivious RAM protocolabstractWe present Path ORAM, an extremely simple Oblivious RAM protocol with a small amount of client storage. Partly due to its simplicity, Path ORAM is the most practical ORAM scheme for small client storage known to date. We formally prove that Path ORAM requires log^2 N / log X bandwidth overhead for block size B = X log N. For block sizes bigger than Omega(log^2 N), Path ORAM is asymptotically better than the best known ORAM scheme with small client storage. Due to its practicality, Path ORAM has been adopted in the design of secure processors since its proposal. Emil Stefanov, Marten van Dijk, Elaine Shi, Christopher W. Fletcher, Ling Ren 0001, Xiangyao Yu, Srini Devadas |
CCS | 7 |
| 2013 | MARTHA: architecture for control and emulation of power electronics and smart grid systemsabstractThis paper presents a novel Multicore Architecture for Real-Time Hybrid Applications (MARTHA) with time-predictable execution, low computational latency, and high performance that meets the requirements for control, emulation and estimation of next-generation power electronics and smart grid systems. Generic general-purpose architectures running real-time operating systems (RTOS) or quality of service (QoS) schedulers have not been able to meet the hard real-time constraints required by these applications. We present a framework based on switched hybrid automata for modeling power electronics applications. Our approach allows a large class of power electronics circuits to be expressed as switched hybrid models which can be executed on a single hardware platform. Michel A. Kinsy, Ivan Celanovic, Omer Khan, Srini Devadas |
DATE | 4 |
| 2013 | Heracles: a tool for fast RTL-based design space exploration of multicore processorsabstractThis paper presents Heracles, an open-source, functional, parameterized, synthesizable multicore system toolkit. Such a multi/many-core design platform is a powerful and versatile research and teaching tool for architectural exploration and hardware-software co-design. The Heracles toolkit comprises the soft hardware (HDL) modules, application compiler, and graphical user interface. It is designed with a high degree of modularity to support fast exploration of future multicore processors of di erent topologies, routing schemes, processing elements (cores), and memory system organizations. It is a component-based framework with parameterized interfaces and strong emphasis on module reusability. The compiler toolchain is used to map C or C++ based applications onto the processing units. The GUI allows the user to quickly con gure and launch a system instance for easy factorial development and evaluation. Hardware modules are implemented in synthesizable Verilog and are FPGA platform independent. The Heracles tool is freely available under the open-source MIT license at: http://projects.csail.mit.edu/heracles Michel A. Kinsy, Michael Pellauer, Srini Devadas |
FPGA | 3 |
| 2013 | Hardware-level thread migration in a 110-core shared-memory multiprocessor
Mieszko Lis, Keun Sup Shim, Brandon Cho, Ilia A. Lebedev, Srini Devadas |
Hot Chips Symposium | 5 |
| 2013 | Design tradeoffs for simplicity and efficient verification in the Execution Migration MachineabstractAs transistor technology continues to scale, the architecture community has experienced exponential growth in design complexity and significantly increasing implementation and verification costs. Moreover, Moore's law has led to a ubiquitous trend of an increasing number of cores on a single chip. Often, these large-core-count chips provide a shared memory abstraction via directories and coherence protocols, which have become notoriously error-prone and difficult to verify because of subtle data races and state space explosion. Although a very simple hardware shared memory implementation can be achieved by simply not allowing ad-hoc data replication and relying on remote accesses for remotely cached data (i.e., requiring no directories or coherence protocols), such remote-access-based directoryless architectures cannot take advantage of any data locality, and therefore suffer in both performance and energy. Our recently taped-out 110-core shared-memory processor, the Execution Migration Machine (EM2), establishes a new design point. On the one hand, EM2supports shared memory but does not automatically replicate data, and thus preserves the simplicity of directoryless architectures. On the other hand, it significantly improves performance and energy over remote-access-only designs by exploiting data locality at remote cores via fast hardware-level thread migration. In this paper, we describe the design choices made in the EM2chip as well as our choice of design methodology, and discuss how they combine to achieve design simplicity and verification efficiency. Even though EM2is a fairly large design-110 cores using a total of 357 million transistors-the entire chip design and implementation process (RTL, verification, physical design, tapeout) took only 18 man-months. Keun Sup Shim, Mieszko Lis, Myong Hyon Cho, Ilia A. Lebedev, Srini Devadas |
ICCD | 5 |
| 2013 | The locality-aware adaptive cache coherence protocolabstractNext generation multicore applications will process massive amounts of data with significant sharing. Data movement and management impacts memory access latency and consumes power. Therefore, harnessing data locality is of fundamental importance in future processors. We propose a scalable, efficient shared memory cache coherence protocol that enables seamless adaptation between private and logically shared caching of on-chip data at the fine granularity of cache lines. Our data-centric approach relies on in-hardware yet low-overhead runtime profiling of the locality of each cache line and only allows private caching for data blocks with high spatio-temporal locality. This allows us to better exploit the private caches and enable low-latency, low-energy memory access, while retaining the convenience of shared memory. On a set of parallel benchmarks, our low-overhead locality-aware mechanisms reduce the overall energy by 25% and completion time by 15% in an NoC-based multicore with the Reactive-NUCA on-chip cache organization and the ACKwise limited directory-based coherence protocol. George Kurian, Omer Khan, Srini Devadas |
ISCA | 3 |
| 2013 | Design space exploration and optimization of path oblivious RAM in secure processorsabstractKeeping user data private is a huge problem both in cloud computing and computation outsourcing. One paradigm to achieve data privacy is to use tamper-resistant processors, inside which users' private data is decrypted and computed upon. These processors need to interact with untrusted external memory. Even if we encrypt all data that leaves the trusted processor, however, the address sequence that goes off-chip may still leak information. To prevent this address leakage, the security community has proposed ORAM (Oblivious RAM). ORAM has mainly been explored in server/file settings which assume a vastly different computation model than secure processors. Not surprisingly, naïvely applying ORAM to a secure processor setting incurs large performance overheads. Ling Ren 0001, Xiangyao Yu, Christopher W. Fletcher, Marten van Dijk, Srini Devadas |
ISCA | 5 |
| 2013 | A framework to accelerate sequential programs on homogeneous multicoresabstractThis paper presents a light-weight dynamic optimization framework for homogeneous multicores. Our system profiles applications at runtime to detect hot program paths, and offloads the optimization of these paths to a Partner core. Our work contributes two insights: (1) that the dynamic optimization process is highly insensitive to runtime factors in homogeneous multicores and (2) that the Partner core's view of application hot paths can be noisy, allowing the entire optimization process to be implemented with very little dedicated hardware in a multicore. Christopher W. Fletcher, Rachael Harding, Omer Khan, Srini Devadas |
VLSI-SoC | 4 |
| 2013 | Optimal and Heuristic Application-Aware Oblivious RoutingabstractConventional oblivious routing algorithms do not take into account resource requirements (e.g., bandwidth, latency) of various flows in a given application. As they are not aware of flow demands that are specific to the application, network resources can be poorly utilized and cause serious local congestion. Also, flows, or packets, may share virtual channels in an undetermined way; the effects of head-of-line blocking may result in throughput degradation. In this paper, we present a framework for application-aware routing that assures deadlock freedom under one or more virtual channels by forcing routes to conform to an acyclic channel dependence graph. In addition, we present methods to statically and efficiently allocate virtual channels to flows or packets, under oblivious routing, when there are two or more virtual channels per link. Using the application-aware routing framework, we develop and evaluate a bandwidth-sensitive oblivious routing scheme that statically determines routes considering an application's communication characteristics. Given bandwidth estimates for flows, we present a mixed integer-linear programming (MILP) approach and a heuristic approach for producing deadlock-free routes that minimize maximum channel load. Our framework can be used to produce application-aware routes that target the minimization of latency, number of flows through a link, bandwidth, or any combination thereof. Our results show that it is possible to achieve better performance than traditional deterministic and oblivious routing schemes on popular synthetic benchmarks using our bandwidth-sensitive approach. We also show that, when oblivious routing is used and there are more flows than virtual channels per link, the static assignment of virtual channels to flows can help mitigate the effects of head-of-line blocking, which may impede packets that are dynamically competing for virtual channels. We experimentally explore the performance tradeoffs of static and dynamic virtual channel allocation on bandwidth-sensitive and traditional oblivious routing methods. Michel A. Kinsy, Myong Hyon Cho, Keun Sup Shim, Mieszko Lis, G. Edward Suh, Srini Devadas |
IEEE Trans. Computers | 6 |
| 2013 | PUF Modeling Attacks on Simulated and Silicon DataabstractWe discuss numerical modeling attacks on several proposed strong physical unclonable functions (PUFs). Given a set of challenge-response pairs (CRPs) of a Strong PUF, the goal of our attacks is to construct a computer algorithm which behaves indistinguishably from the original PUF on almost all CRPs. If successful, this algorithm can subsequently impersonate the Strong PUF, and can be cloned and distributed arbitrarily. It breaks the security of any applications that rest on the Strong PUF's unpredictability and physical unclonability. Our method is less relevant for other PUF types such as Weak PUFs. The Strong PUFs that we could attack successfully include standard Arbiter PUFs of essentially arbitrary sizes, and XOR Arbiter PUFs, Lightweight Secure PUFs, and Feed-Forward Arbiter PUFs up to certain sizes and complexities. We also investigate the hardness of certain Ring Oscillator PUF architectures in typical Strong PUF applications. Our attacks are based upon various machine learning techniques, including a specially tailored variant of logistic regression and evolution strategies. Our results are mostly obtained on CRPs from numerical simulations that use established digital models of the respective PUFs. For a subset of the considered PUFs-namely standard Arbiter PUFs and XOR Arbiter PUFs-we also lead proofs of concept on silicon data from both FPGAs and ASICs. Over four million silicon CRPs are used in this process. The performance on silicon CRPs is very close to simulated CRPs, confirming a conjecture from earlier versions of this work. Our findings lead to new design requirements for secure electrical Strong PUFs, and will be useful to PUF designers and attackers alike. Ulrich Rührmair, Jan Sölter, Frank Sehnke, Xiaolin Xu 0001, Ahmed Mahmoud, Vera Stoyanova, Gideon Dror, Jürgen Schmidhuber, Wayne P. Burleson, Srini Devadas |
IEEE Trans. Inf. Forensics Secur. | 10 |
| 2012 | A low-overhead dynamic optimization framework for multicoresabstractThis paper argues for a "less is more" design philosophy when integrating dynamic optimization into a multicore system. The primary insight is that dynamic optimization is inherently loosely-coupled and can therefore be supported on multicores with very low-overhead by using a Partner core. We exploit this property by designing a dynamic optimizer composed of a two-core partnership that requires a minimal amount of dedicated hardware and is resilient to (a) reducing the Partner core's clock frequency, (b) changing the Partner core's placement on the multicore die and (c) varying the latency of dynamic optimization operations. Christopher W. Fletcher, Rachael Harding, Omer Khan, Srini Devadas |
PACT | 4 |
| 2012 | Self-aware computing in the Angstrom processorabstractAddressing the challenges of extreme scale computing requires holistic design of new programming models and systems that support those models. This paper discusses the Angstrom processor, which is designed to support a new Self-aware Computing (SEEC) model. In SEEC, applications explicitly state goals, while other systems components provide actions that the SEEC runtime system can use to meet those goals. Angstrom supports this model by exposing sensors and adaptations that traditionally would be managed independently by hardware. This exposure allows SEEC to coordinate hardware actions with actions specified by other parts of the system, and allows the SEEC runtime system to meet application goals while reducing costs (e.g., power consumption). Henry Hoffmann, Jim Holt, George Kurian, Eric Lau, Martina Maggio, Jason E. Miller, Sabrina M. Neuman, Mahmut E. Sinangil, Yildiz Sinangil, Anant Agarwal, Anantha P. Chandrakasan, Srini Devadas |
DAC | 12 |
| 2012 | Lynx: A Programmatic SAT Solver for the RNA-Folding Problem
Vijay Ganesh 0001, Charles W. O'Donnell, Mate Soos, Srini Devadas, Martin C. Rinard, Armando Solar-Lezama |
SAT | 4 |
| 2012 | HORNET: A Cycle-Level Multicore SimulatorabstractWe present hornet, a parallel, highly configurable, cycle-level multicore simulator based on an ingress-queued wormhole router network-on-chip (NoC) architecture. The parallel simulation engine offers cycle-accurate as well as periodic synchronization; while preserving functional accuracy, this permits tradeoffs between perfect timing accuracy and high speed with very good accuracy. When run on six separate physical cores on a single die, speedups can exceed a factor of over 5, and when run on a two-die 12-core system with 2-way hyperthreading, speedups exceed$12\times$. Most hardware parameters are configurable, including memory hierarchy, interconnect geometry, bandwidth, crossbar dimensions, parameters driving power, and thermal effects. A highly parametrized table-based NoC design allows a variety of routing and virtual channel allocation algorithms out of the box, ranging from simple dimension-ordered routing to complex Valiant, ROMM, O1Turn or PROM schemes, BSOR, and adaptive routing. Hornet can run in network-only mode using synthetic traffic or traces, or directly emulate a MIPS-based multicore. Hornet is freely available under the open-source MIT license at http://csg.csail.mit.edu/hornet/. Pengju Ren, Mieszko Lis, Myong Hyon Cho, Keun Sup Shim, Christopher W. Fletcher, Omer Khan, Nanning Zheng 0001, Srini Devadas |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 8 |
| 2012 | Selecting Spatiotemporal Patterns for Development of Parallel ApplicationsabstractDesign patterns for parallel computing attempt to make the field accessible to nonexperts by generalizing the common techniques experts use to develop parallel software. Existing parallel patterns have tremendous descriptive power, but it is often unclear to nonexperts how to choose a pattern based on the specific performance goals of a given application. This paper addresses the need for a pattern selection methodology by presenting four patterns and an accompanying decision framework for choosing from these patterns given an application's throughput and latency goals. The patterns are based on recognizing that one can partition an application's data or instructions and that these partitionings can be done in time or space, hence we refer to them as spatiotemporal partitioning strategies. This paper introduces a taxonomy that describes each of the resulting four partitioning strategies and presents a three-step methodology for selecting one or more given a throughput and latency goal. Several case studies are presented to illustrate the use of this methodology. These case studies cover several simple examples as well as more complicated applications including a radar processing application and an H.264 video encoder. Henry Hoffmann, Anant Agarwal, Srini Devadas |
IEEE Trans. Parallel Distributed Syst. | 3 |
| 2011 | FPGA-Based True Random Number Generation Using Circuit Metastability with Adaptive Feedback Control
Mehrdad Majzoobi, Farinaz Koushanfar, Srini Devadas |
CHES | 3 |
| 2011 | Lightweight and Secure PUF Key Storage Using Limits of Machine Learning
Meng-Day (Mandel) Yu, David M'Raïhi, Richard Sowell, Srini Devadas |
CHES | 4 |
| 2011 | Heracles: Fully Synthesizable Parameterized MIPS-Based Multicore SystemabstractHeracles is an open-source complete multicore system written in Verilog. It is fully parameterized and can be reconfigured and synthesized into different topologies and sizes. Each processing node has a fully bypassed, 7-stage pipelined microprocessor running the MIPS-III ISA, a 4-stage input-buffer, virtual-channel router, and a local variable-size shared memory. Our design is highly modular with clear interfaces between the core, the memory hierarchy, and the on-chip network. In the baseline design, the microprocessor is attached to two caches, one instruction cache and one data cache, which are oblivious to the global memory organization. The memory system in Heracles can be configured as one single global shared memory (SM), or distributed shared memory (DSM), or any combination thereof. Each core is connected to the rest of the network of processors by a parameterized, realistic, wormhole router. We show different topology configurations of the system, and their synthesis results on the Xilinx Virtex-5 LX330T FPGA board. We also provide a small MIPS cross-compiler tool chain to assist in developing software for Heracles. Michel A. Kinsy, Michael Pellauer, Srini Devadas |
FPL | 3 |
| 2011 | ARCc: A case for an architecturally redundant cache-coherence architecture for large multicoresabstractThis paper proposes an architecturally redundant cache-coherence architecture (ARCc) that combines the directory and shared-NUCA based coherence protocols to improve performance, energy and dependability. Both coherence mechanisms co-exist in the hardware and ARCc enables seamless transition between the two protocols. We present an online analytical model implemented in the hardware that predicts performance and triggers a transition between the two coherence protocols at application-level granularity. The ARCc architecture delivers up to 1.6× higher performance and up to 1.5× lower energy consumption compared to the directory-based counterpart. It does so by identifying applications which benefit from the large shared cache capacity of shared-NUCA because of lower off-chip accesses, or where remote-cache word accesses are efficient. Omer Khan, Henry Hoffmann, Mieszko Lis, Farrukh Hijaz, Anant Agarwal, Srini Devadas |
ICCD | 6 |
| 2011 | Memory coherence in the age of multicoresabstractAs we enter an era of exascale multicores, the question of efficiently supporting a shared memory model has become of paramount importance. On the one hand, programmers demand the convenience of coherent shared memory; on the other, growing core counts place higher demands on the memory subsystem and increasing on-chip distances mean that interconnect delays are becoming a significant part of memory access latencies. In this article, we first review the traditional techniques for providing a shared memory abstraction at the hardware level in multicore systems. We describe two new schemes that guarantee coherent shared memory without the complexity and overheads of a cache coherence protocol, namely execution migration and library cache coherence. We compare these approaches using an analytical model based on average memory latency, and give intuition for the strengths and weaknesses of each. Finally, we describe hybrid schemes that combine the strengths of different schemes. Mieszko Lis, Keun Sup Shim, Myong Hyon Cho, Srini Devadas |
ICCD | 4 |
| 2011 | Scalable, accurate multicore simulation in the 1000-core eraabstractWe present HORNET, a parallel, highly configurable, cycle-level multicore simulator based on an ingress-queued worm-hole router NoC architecture. The parallel simulation engine offers cycle-accurate as well as periodic synchronization; while preserving functional accuracy, this permits tradeoffs between perfect timing accuracy and high speed with very good accuracy. When run on 6 separate physical cores on a single die, speedups can exceed a factor of over 5, and when run on a two-die 12-core system with 2-way hyperthreading, speedups exceed 11 ×. Most hardware parameters are configurable, including memory hierarchy, interconnect geometry, bandwidth, crossbar dimensions, and parameters driving power and thermal effects. A highly parametrized table-based NoC design allows a variety of routing and virtual channel allocation algorithms out of the box, ranging from simple DOR routing to complex Valiant, ROMM, or PROM schemes, BSOR, and adaptive routing. HORNET can run in network-only mode using synthetic traffic or traces, directly emulate a MIPS-based multicore, or function as the memory subsystem for native applications executed under the Pin instrumentation tool. HORNET is freely available under the open-source MIT license at http://csg.csail.mit.edu/hornet/. Mieszko Lis, Pengju Ren, Myong Hyon Cho, Keun Sup Shim, Christopher W. Fletcher, Omer Khan, Srini Devadas |
ISPASS | 7 |
| 2011 | Deadlock-free fine-grained thread migrationabstractAbstract—Several recent studies have proposed fine-grained, hardware-level thread migration in multicores as a solution to power, reliability, and memory coherence problems. The need for fast thread migration has been well documented, however, a fast, deadlock-free migration protocol is sorely lacking: existing solutions either deadlock or are too slow and cumbersome to ensure performance with frequent, fine-grained thread migrations. In this study, we introduce the Exclusive Native Context (ENC) protocol, a general, provably deadlock-free migration protocol for instruction-level thread migration architectures. Simple to implement, ENC does not require additional hardware beyond common migration-based architectures. Our evaluation using synthetic migrations and the SPLASH-2 application suite shows that ENC offers performance within 11.7 % of an idealized deadlock-free migration protocol with infinite resources. I. Myong Hyon Cho, Keun Sup Shim, Mieszko Lis, Omer Khan, Srini Devadas |
NOCS | 5 |
| 2011 | Efficient Traversal of Beta-Sheet Protein Folding Pathways Using Ensemble Models
Solomon Shenker, Charles W. O'Donnell, Srini Devadas, Bonnie Berger, Jérôme Waldispühl |
RECOMB | 3 |
| 2011 | Time-Predictable Computer Architecture for Cyber-Physical Systems: Digital Emulation of Power Electronics SystemsabstractThe smart grid concept is a good example of a complex cyber-physical system (CPS) that exhibits intricate interplay between control, sensing, and communication infrastructure on one side, and power processing and actuation on the other side. The more extensive use of computation, sensing, and communication, tightly coupled with power processing, calls for a fundamental reassessment of some of the prevailing paradigms in the real-time control and communication abstractions. Today these abstractions are mostly thought of as embedded systems, and the overall framework needs to be reformed in order to fully realize the potential of the emerging field of cyber-physical systems. This paper details the design and application of a new ultrahigh speed real-time emulation platform for Hardware-in-the-Loop (HiL) testing and design of high-power power electronics systems. Our real-time hardware emulation for HiL systems is based on a reconfigurable, heterogeneous, multicore processor architecture that emulates power electronics, and includes a circuit compiler that translates graphic system models into processor executable machine code. We present the hardware architecture, and describe the process of power electronic circuit compilation. This approach yields real-time execution on the order of 1μs simulation time step (including input/output latency) for a broad class of power electronics converters. To the best of our knowledge, no current academic or industrial HiL system has such a fast emulation response time. We present HiL experimental results for three representative systems: a variable speed induction motor drive, a utility grid connected photovoltaic converter system, and a hybrid electric vehicle motor drive. Michel A. Kinsy, Omer Khan, Ivan Celanovic, Dusan Majstorovic, Nikola L. Celanovic, Srini Devadas |
RTSS | 6 |
| 2011 | Brief announcement: distributed shared memory based on computation migrationabstractShare on Brief announcement: distributed shared memory based on computation migration Authors: Mieszko Lis Massachusetts Institute of Technology, Cambridge, MA, USA Massachusetts Institute of Technology, Cambridge, MA, USAView Profile , Keun Sup Shim Massachusetts Institute of Technology, Cambridge, MA, USA Massachusetts Institute of Technology, Cambridge, MA, USAView Profile , Myong Hyon Cho Massachusetts Institute of Technology, Cambridge, MA, USA Massachusetts Institute of Technology, Cambridge, MA, USAView Profile , Christopher W. Fletcher Massachusetts Institute of Technology, Cambridge, MA, USA Massachusetts Institute of Technology, Cambridge, MA, USAView Profile , Michel Kinsy Massachusetts Institute of Technology, Cambridge, MA, USA Massachusetts Institute of Technology, Cambridge, MA, USAView Profile , Ilia Lebedev Massachusetts Institute of Technology, Cambridge, MA, USA Massachusetts Institute of Technology, Cambridge, MA, USAView Profile , Omer Khan Massachusetts Institute of Technology, Cambridge, MA, USA Massachusetts Institute of Technology, Cambridge, MA, USAView Profile , Srinivas Devadas Massachusetts Institute of Technology, Cambridge, MA, USA Massachusetts Institute of Technology, Cambridge, MA, USAView Profile Authors Info & Claims SPAA '11: Proceedings of the twenty-third annual ACM symposium on Parallelism in algorithms and architecturesJune 2011 Pages 253–256https://doi.org/10.1145/1989493.1989530Online:04 June 2011Publication History 3citation154DownloadsMetricsTotal Citations3Total Downloads154Last 12 Months8Last 6 weeks0 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my Alerts New Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteGet Access Mieszko Lis, Keun Sup Shim, Myong Hyon Cho, Christopher W. Fletcher, Michel A. Kinsy, Ilia A. Lebedev, Omer Khan, Srini Devadas |
SPAA | 8 |
| 2011 | A method for probing the mutational landscape of amyloid structureabstractMOTIVATION: Proteins of all kinds can self-assemble into highly ordered β-sheet aggregates known as amyloid fibrils, important both biologically and clinically. However, the specific molecular structure of a fibril can vary dramatically depending on sequence and environmental conditions, and mutations can drastically alter amyloid function and pathogenicity. Experimental structure determination has proven extremely difficult with only a handful of NMR-based models proposed, suggesting a need for computational methods. RESULTS: We present AmyloidMutants, a statistical mechanics approach for de novo prediction and analysis of wild-type and mutant amyloid structures. Based on the premise of protein mutational landscapes, AmyloidMutants energetically quantifies the effects of sequence mutation on fibril conformation and stability. Tested on non-mutant, full-length amyloid structures with known chemical shift data, AmyloidMutants offers roughly 2-fold improvement in prediction accuracy over existing tools. Moreover, AmyloidMutants is the only method to predict complete super-secondary structures, enabling accurate discrimination of topologically dissimilar amyloid conformations that correspond to the same sequence locations. Applied to mutant prediction, AmyloidMutants identifies a global conformational switch between Aβ and its highly-toxic 'Iowa' mutant in agreement with a recent experimental model based on partial chemical shift data. Predictions on mutant, yeast-toxic strains of HET-s suggest similar alternate folds. When applied to HET-s and a HET-s mutant with core asparagines replaced by glutamines (both highly amyloidogenic chemically similar residues abundant in many amyloids), AmyloidMutants surprisingly predicts a greatly reduced capacity of the glutamine mutant to form amyloid. We confirm this finding by conducting mutagenesis experiments. AVAILABILITY: Our tool is publically available on the web at http://amyloid.csail.mit.edu/. CONTACT: [email protected]; [email protected]. Charles W. O'Donnell, Jérôme Waldispühl, Mieszko Lis, Randal Halfmann, Srini Devadas, Susan Lindquist, Bonnie Berger |
Bioinform. | 5 |
| 2010 | Modeling attacks on physical unclonable functionsabstractWe show in this paper how several proposed Physical Unclonable Functions (PUFs) can be broken by numerical modeling attacks. Given a set of challenge-response pairs (CRPs) of a PUF, our attacks construct a computer algorithm which behaves indistinguishably from the original PUF on almost all CRPs. This algorithm can subsequently impersonate the PUF, and can be cloned and distributed arbitrarily. This breaks the security of essentially all applications and protocols that are based on the respective PUF. The PUFs we attacked successfully include standard Arbited PUFs and Ring Oscillator PUFs of arbitrary sizes, and XO Arbiter PUFs, Lightweight Secure PUFs, and Feed-Forward Arbiter PUFs of up to a given size and complexity. Our attacks are based upon various machine learning techniques including Logistic Regression and Evolution Strategies. Our work leads to new design requirements for secure electrical PUFs, and will be useful to PUF designers and attackers alike. Ulrich Rührmair, Frank Sehnke, Jan Sölter, Gideon Dror, Srini Devadas, Jürgen Schmidhuber |
CCS | 5 |
| 2009 | Oblivious Routing in On-Chip Bandwidth-Adaptive NetworksabstractOblivious routing can be implemented on simple router hardware, but network performance suffers when routes become congested. Adaptive routing attempts to avoid hot spots by re-routing flows, but requires more complex hardware to determine and configure new routing paths. We propose onchip bandwidth-adaptive networks to mitigate the performance problems of oblivious routing and the complexity issues of adaptive routing. In a bandwidth-adaptive network, the bisection bandwidth of network can adapt to changing network conditions. We describe one implementation of a bandwidth-adaptive network in the form of a two-dimensional mesh with adaptive bidirectional links, where the bandwidth of the link in one direction can be increased at the expense of the other direction. Efficient local intelligence is used to reconfigure each link, and this reconfiguration can be done very rapidly in response to changing traffic demands. We compare the hardware designs of a unidirectional and bidirectional link and evaluate the performance gains provided by a bandwidth-adaptive network in comparison to a conventional network under uniform and bursty traffic when oblivious routing is used. Myong Hyon Cho, Mieszko Lis, Keun Sup Shim, Michel A. Kinsy, Tina Wen, Srini Devadas |
PACT | 6 |
| 2009 | Physical Unclonable Functions and Secure Processors
Srini Devadas |
CHES | 1 |
| 2009 | Application-aware deadlock-free oblivious routingabstractConventional oblivious routing algorithms are either not application-aware or assume that each flow has its own private channel to ensure deadlock avoidance. We present a framework for application-aware routing that assures deadlock-freedom under one or more channels by forcing routes to conform to an acyclic channel dependence graph. Arbitrary minimal routes can be made deadlock-free through appropriate static channel allocation when two or more channels are available. Given bandwidth estimates for flows, we present a mixed integer-linear programming (MILP) approach and a heuristic approach for producing deadlock-free routes that minimize maximum channel load. The heuristic algorithm is calibrated using the MILP algorithm and evaluated on a number of benchmarks through detailed network simulation. Our framework can be used to produce application-aware routes that target the minimization of latency, number of flows through a link, bandwidth, or any combination thereof. Michel A. Kinsy, Myong Hyon Cho, Tina Wen, G. Edward Suh, Marten van Dijk, Srini Devadas |
ISCA | 6 |
| 2009 | Static virtual channel allocation in oblivious routingabstractMost virtual channel routers have multiple virtual channels to mitigate the effects of head-of-line blocking. When there are more flows than virtual channels at a link, packets or flows must compete for channels, either in a dynamic way at each link or by static assignment computed before transmission starts. In this paper, we present methods that statically allocate channels to flows at each link when oblivious routing is used, and ensure deadlock freedom for arbitrary minimal routes when two or more virtual channels are available. We then experimentally explore the performance trade-offs of static and dynamic virtual channel allocation for various oblivious routing methods, including DOR, ROMM, Valiant and a novel bandwidth-sensitive oblivious routing scheme (BSORM). Through judicious separation of flows, static allocation schemes often exceed the performance of dynamic allocation schemes. Keun Sup Shim, Myong Hyon Cho, Michel A. Kinsy, Tina Wen, Mieszko Lis, G. Edward Suh, Srini Devadas |
NOCS | 7 |
| 2009 | Simultaneous Alignment and Folding of Protein Sequences
Jérôme Waldispühl, Charles W. O'Donnell, Sebastian Will, Srini Devadas, Rolf Backofen, Bonnie Berger |
RECOMB | 4 |
| 2009 | Efficient stochastic simulation of reaction-diffusion processes via direct compilationabstractAbstract We present the Stochastic Simulator Compiler (SSC), a tool for exact stochastic simulations of well-mixed and spatially heterogeneous systems. SSC is the first tool to allow a readable high-level description with spatially heterogeneous simulation algorithms and complex geometries; this permits large systems to be expressed concisely. Meanwhile, direct native-code compilation allows SSC to generate very fast simulations. Availability: SSC currently runs on Linux and Mac OS X, and is freely available at http://web.mit.edu/irc/ssc/. Contact: [email protected] Supplementary information: Supplementary data are available at Bioinformatics online. Mieszko Lis, Maxim N. Artyomov, Srini Devadas, Arup K. Chakraborty |
Bioinform. | 3 |
| 2008 | The Trusted Execution Module: Commodity General-Purpose Trusted Computing
Victor Costan, Luis F. G. Sarmenta, Marten van Dijk, Srini Devadas |
CARDIS | 4 |
| 2008 | Diastolic arrays: throughput-driven reconfigurable computingabstractDiastolic arrays are arrays of processing elements that communicate exclusively through First-In First-Out (FIFO) queues. FIFO virtualization units enable relaxed timing of data transfers, and include hardware support to guarantee bandwidth and buffer space for all data transfers, which may follow composite paths through the network. We show that the architecture of diastolic arrays enables efficient synthesis from high-level specifications of communicating finite state machines so average throughput is maximized. Preliminary results are presented on an H.264 decoding benchmark. Myong Hyon Cho, Chih-Chi Cheng, Michel A. Kinsy, G. Edward Suh, Srini Devadas |
ICCAD | 5 |
| 2008 | Efficient Algorithms for Probing the RNA Mutation LandscapeabstractThe diversity and importance of the role played by RNAs in the regulation and development of the cell are now well-known and well-documented. This broad range of functions is achieved through specific structures that have been (presumably) optimized through evolution. State-of-the-art methods, such as McCaskill's algorithm, use a statistical mechanics framework based on the computation of the partition function over the canonical ensemble of all possible secondary structures on a given sequence. Although secondary structure predictions from thermodynamics-based algorithms are not as accurate as methods employing comparative genomics, the former methods are the only available tools to investigate novel RNAs, such as the many RNAs of unknown function recently reported by the ENCODE consortium. In this paper, we generalize the McCaskill partition function algorithm to sum over the grand canonical ensemble of all secondary structures of all mutants of the given sequence. Specifically, our new program, RNAmutants, simultaneously computes for each integer k the minimum free energy structure MFE(k) and the partition function Z(k) over all secondary structures of all k-point mutants, even allowing the user to specify certain positions required not to mutate and certain positions required to base-pair or remain unpaired. This technically important extension allows us to study the resilience of an RNA molecule to pointwise mutations. By computing the mutation profile of a sequence, a novel graphical representation of the mutational tendency of nucleotide positions, we analyze the deleterious nature of mutating specific nucleotide positions or groups of positions. We have successfully applied RNAmutants to investigate deleterious mutations (mutations that radically modify the secondary structure) in the Hepatitis C virus cis-acting replication element and to evaluate the evolutionary pressure applied on different regions of the HIV trans-activation response element. In particular, we show qualitative agreement between published Hepatitis C and HIV experimental mutagenesis studies and our analysis of deleterious mutations using RNAmutants. Our work also predicts other deleterious mutations, which could be verified experimentally. Finally, we provide evidence that the 3' UTR of the GB RNA virus C has been optimized to preserve evolutionarily conserved stem regions from a deleterious effect of pointwise mutations. We hope that there will be long-term potential applications of RNAmutants in de novo RNA design and drug design against RNA viruses. This work also suggests potential applications for large-scale exploration of the RNA sequence-structure network. Binary distributions are available at http://RNAmutants.csail.mit.edu/. Jérôme Waldispühl, Srini Devadas, Bonnie Berger, Peter Clote |
PLoS Comput. Biol. | 2 |
| 2008 | Controlled physical random functions and applicationsabstractThe cryptographic protocols that we use in everyday life rely on the secure storage of keys in consumer devices. Protecting these keys from invasive attackers, who open a device to steal its key, is a challenging problem. We propose controlled physical random functions (CPUFs) as an alternative to storing keys and describe the core protocols that are needed to use CPUFs. A physical random functions (PUF) is a physical system with an input and output. The functional relationship between input and output looks like that of a random function. The particular relationship is unique to a specific instance of a PUF, hence, one needs access to a particular PUF instance to evaluate the function it embodies. The cryptographic applications of a PUF are quite limited unless the PUF is combined with an algorithm that limits the ways in which the PUF can be evaluated; this is a CPUF. A major difficulty in using CPUFs is that you can only know a small set of outputs of the PUF—the unknown outputs being unrelated to the known ones. We present protocols that get around this difficulty and allow a chain of trust to be established between the CPUF manufacturer and a party that wishes to interact securely with the PUF device. We also present some elementary applications, such as certified execution. Blaise Gassend, Marten van Dijk, Dwaine E. Clarke, Emina Torlak, Srini Devadas, Pim Tuyls |
ACM Trans. Inf. Syst. Secur. | 5 |
| 2007 | Physical Unclonable Functions for Device Authentication and Secret Key GenerationabstractPhysical Unclonable Functions (PUFs) are innovative circuit primitives that extract secrets from physical characteristics of integrated circuits (ICs). We present PUF designs that exploit inherent delay characteristics of wires and transistors that differ from chip to chip, and describe how PUFs can enable low-cost authentication of individual ICs and generate volatile secret keys for cryptographic operations. G. Edward Suh, Srini Devadas |
DAC | 2 |
| 2007 | Learning biophysically-motivated parameters for alpha helix predictionabstractBACKGROUND: Our goal is to develop a state-of-the-art protein secondary structure predictor, with an intuitive and biophysically-motivated energy model. We treat structure prediction as an optimization problem, using parameterizable cost functions representing biological "pseudo-energies". Machine learning methods are applied to estimate the values of the parameters to correctly predict known protein structures. RESULTS: Focusing on the prediction of alpha helices in proteins, we show that a model with 302 parameters can achieve a Qalpha value of 77.6% and an SOValpha value of 73.4%. Such performance numbers are among the best for techniques that do not rely on external databases (such as multiple sequence alignments). Further, it is easier to extract biological significance from a model with so few parameters. CONCLUSION: The method presented shows promise for the prediction of protein secondary structure. Biophysically-motivated elementary free-energies can be learned using SVM techniques to construct an energy cost function whose predictive performance rivals state-of-the-art. This method is general and can be extended beyond the all-alpha case described here. Blaise Gassend, Charles W. O'Donnell, William Thies, Marten van Dijk, Srini Devadas |
BMC Bioinform. | 6 |
| 2006 | Speeding up Exponentiation using an Untrusted Computational Resource
Marten van Dijk, Dwaine E. Clarke, Blaise Gassend, G. Edward Suh, Srini Devadas |
Des. Codes Cryptogr. | 5 |
| 2005 | Design and Implementation of the AEGIS Single-Chip Secure Processor Using Physical Random FunctionsabstractSecure processors enable new applications by ensuring private and authentic program execution even in the face of physical attack. In this paper, we present the AEGIS secure processor architecture, and evaluate its RTL implementation on FPGAs. By using physical random functions, we propose a new way of reliably protecting and sharing secrets that is more secure than existing solutions based on non-volatile memory. Our architecture gives applications the flexibility of trusting and protecting only a portion of a given process, unlike prior proposals which require a process to be protected in entirety. We also put forward a specific model of how secure applications can be programmed in a high-level language and compiled to run on our system. Finally, we evaluate a fully functional FPGA implementation of our processor, assess the implementation tradeoffs, compare performance, and demonstrate the benefits of partially protecting a program. G. Edward Suh, Charles W. O'Donnell, Ishan Sachdev, Srini Devadas |
ISCA | 4 |
| 2005 | Towards Constant Bandwidth Overhead Integrity Checking of Untrusted DataabstractWe present an adaptive tree-log scheme to improve the performance of checking the integrity of arbitrarily large untrusted data, when using only a small fixed-sized trusted state. Currently, hash trees are used to check the data. In many systems that use hash trees, programs perform many data operations before performing a critical operation that exports a result outside of the program's execution environment. The adaptive tree-log scheme we present uses this observation to harness the power of the constant runtime bandwidth overhead of a log-based scheme. For all programs, the adaptive tree-log scheme's bandwidth overhead is guaranteed to never be worse than a parameterizable worst case bound. Furthermore, for all programs, as the average number of times the program accesses data between critical operations increases, the adaptive tree-log scheme's bandwidth overhead moves from a logarithmic to a constant bandwidth overhead. Dwaine E. Clarke, G. Edward Suh, Blaise Gassend, Ajay Sudan, Marten van Dijk, Srini Devadas |
S&P | 6 |
| 2005 | AEGIS: A single-chip secure processor
G. Edward Suh, Charles W. O'Donnell, Srini Devadas |
Inf. Secur. Tech. Rep. | 3 |
| 2005 | Extracting secret keys from integrated circuitsabstractModern cryptographic protocols are based on the premise that only authorized participants can obtain secret keys and access to information systems. However, various kinds of tampering methods have been devised to extract secret keys from conditional access systems such as smartcards and ATMs. Arbiter-based physical unclonable functions (PUFs) exploit the statistical delay variation of wires and transistors across integrated circuits (ICs) in manufacturing processes to build unclonable secret keys. We fabricated arbiter-based PUFs in custom silicon and investigated the identification capability, reliability, and security of this scheme. Experimental results and theoretical studies show that a sufficient amount of inter-chip variation exists to enable each IC to be identified securely and reliably over a practical range of environmental variations such as temperature and power supply voltage. We show that arbiter-based PUFs are realizable and well suited to build, for example, key-cards that need to be resistant to physical attacks. Daihyun Lim, Jae W. Lee, Blaise Gassend, G. Edward Suh, Marten van Dijk, Srini Devadas |
IEEE Trans. Very Large Scale Integr. Syst. | 6 |
| 2004 | Secure program execution via dynamic information flow trackingabstractWe present a simple architectural mechanism called dynamic information flow tracking that can significantly improve the security of computing systems with negligible performance overhead. Dynamic information flow tracking protects programs against malicious software attacks by identifying spurious information flows from untrusted I/O and restricting the usage of the spurious information.Every security attack to take control of a program needs to transfer the program's control to malevolent code. In our approach, the operating system identifies a set of input channels as spurious, and the processor tracks all information flows from those inputs. A broad range of attacks are effectively defeated by checking the use of the spurious values as instructions and pointers.Our protection is transparent to users or application programmers; the executables can be used without any modification. Also, our scheme only incurs, on average, a memory overhead of 1.4% and a performance overhead of 1.1%. G. Edward Suh, Jae W. Lee, David Zhang 0001, Srini Devadas |
ASPLOS | 4 |
| 2004 | Rate Guarantees and Overload Protection in Input-Queued SwitchesabstractDespite increasing bandwidth demand and the significant research and commercial activity in large-scale terabit routers for multi-gigabit/s links, many current switch designs do not provide adequate support for rate guarantees. In particular, designs based on the popular combined-input/output-queueing (CIOQ) paradigm have unpredictable performance despite implementing sophisticated scheduling schemes on egress links, because the crossbar arbitration between ingress and egress links is done without regard to desired rate guarantees or prevailing traffic conditions. This work describes the design of an input-queued switch system and its associated arbitration and rate allocation algorithms that achieve both absolute rate guarantees and proportional bandwidth sharing even under overloaded or adversarial traffic. Our algorithms are simple and scalable and require a switch speedup of two to provide rate guarantees; we give the theoretical justification and report on simulation results that justify our claims. A semiconductor chipset based on variants of these algorithms for routers with an aggregate capacity of 160 Gbps with links up to 10 Gbps is now commercially available, and a second-generation chipset supporting 640 Gbps is also available. Hari Balakrishnan, Srini Devadas, Douglas Ehlert, Arvind 0001 |
INFOCOM | 2 |
| 2004 | Identification and authentication of integrated circuitsabstractAbstract This paper describes a technique to reliably and securely identify individual integrated circuits (ICs) based on the precise measurement of circuit delays and a simple challenge–response protocol. This technique could be used to produce key‐cards that are more difficult to clone than ones involving digital keys on the IC. We consider potential venues of attack against our system, and present candidate implementations. Experiments on Field Programmable Gate Arrays show that the technique is viable, but that our current implementations could require some strengthening before it can be considered as secure. Copyright © 2004 John Wiley & Sons, Ltd. Blaise Gassend, Daihyun Lim, Dwaine E. Clarke, Marten van Dijk, Srini Devadas |
Concurr. Pract. Exp. | 5 |
| 2004 | Access-controlled resource discovery in pervasive networksabstractAbstract Networks of the future will be characterized by a variety of computational devices that display a level of dynamism not seen in traditional wired networks. Because of the dynamic nature of these networks, resource discovery is one of the fundamental problems that must be solved. While resource discovery systems are not a novel concept, securing these systems in an efficient and scalable way is challenging. This paper describes the design and implementation of an architecture for access‐controlled resource discovery. This system achieves this goal by integrating access control with the Intentional Naming System (INS), a resource discovery and service location system. The integration is scalable, efficient, and fits well within a proxy‐based security framework designed for dynamic networks. We provide performance experiments that show how our solution outperforms existing schemes. The result is a system that provides secure, access‐controlled resource discovery that can scale to large numbers of resources and users. Copyright © 2004 John Wiley & Sons, Ltd. Sanjay Raman, Dwaine E. Clarke, Matthew Burnside, Srini Devadas, Ronald L. Rivest |
Concurr. Pract. Exp. | 4 |
| 2004 | Dynamic Partitioning of Shared Cache Memory
G. Edward Suh, Larry Rudolph, Srini Devadas |
J. Supercomput. | 3 |
| 2003 | Incremental Multiset Hash Functions and Their Application to Memory Integrity Checking
Dwaine E. Clarke, Srini Devadas, Marten van Dijk, Blaise Gassend, G. Edward Suh |
ASIACRYPT | 2 |
| 2003 | Embedded intelligent SRAMabstractMany embedded systems use a simple pipelined RISC processor for computation and an on-chip SRAM for data storage. We present an enhancement called Intelligent SRAM (ISRAM) that consists of a small computation unit with an accumulator that is placed near the on-chip SRAM. The computation unit can perform operations on two words from the same SRAM row or on one word from the SRAM and the other from the accumulator. This ISRAM enhancement requires only a few additional instructions to support the computation unit. We present a computation partitioning algorithm that assigns the computations to the processor or to the new computation unit for a given data flow graph of the program. Performance improvement comes from the reduction in the number of accesses to the SRAM, the number of instructions, and the number of pipeline stalls compared to the same operations in the processor. The experimental results on various benchmarks show up to 1.48 performance speedup with our enhancement. Prabhat Jain, G. Edward Suh, Srini Devadas |
DAC | 3 |
| 2003 | Caches and Hash Trees for Efficient Memory Integrity VerificationabstractWe study the hardware cost of implementing hash-tree based verification of untrusted external memory by a high performance processor. This verification could enable applications such as certified program execution. A number of schemes are presented with different levels of integration between the on-processor L2 cache and the hash-tree machinery. Simulations show that for the best of our methods, the performance overhead is less than 25%, a significant decrease from the 10/spl times/ overhead of a naive implementation. Blaise Gassend, G. Edward Suh, Dwaine E. Clarke, Marten van Dijk, Srini Devadas |
HPCA | 5 |
| 2003 | AEGIS: architecture for tamper-evident and tamper-resistant processingabstractWe describe the architecture for a single-chip aegis processor which can be used to build computing systems secure against both physical and software attacks. Our architecture assumes that all components external to the processor, such as memory, are untrusted. We show two different implementations. In the first case, the core functionality of the operating system is trusted and implemented in a security kernel. We also describe a variant implementation assuming an untrusted operating system.aegis provides users with tamper-evident, authenticated environments in which any physical or software tampering by an adversary is guaranteed to be detected, and private and authenticated tamper-resistant environments where additionally the adversary is unable to obtain any information about software or data by tampering with, or otherwise observing, system operation. aegis enables many applications, such as commercial grid computing, secure mobile agents, software licensing, and digital rights management.Preliminary simulation results indicate that the overhead of security mechanisms in aegis is reasonable. G. Edward Suh, Dwaine E. Clarke, Blaise Gassend, Marten van Dijk, Srini Devadas |
ICS | 5 |
| 2003 | Efficient Memory Integrity Verification and Encryption for Secure ProcessorsabstractSecure processors enable new sets of applications such as commercial grid computing, software copy-protection, and secure mobile agents by providing security from both physical and software attacks.This paper proposes new hardware mechanisms for memory integrity verification and encryption, which are two key primitives required in singlechip secure processors.The integrity verification mechanism offers significant performance advantages over existing ones when the checks are infrequent as in grid computing applications.The encryption mechanism improves the performance in all cases. G. Edward Suh, Dwaine E. Clarke, Blaise Gassend, Marten van Dijk, Srini Devadas |
MICRO | 5 |
| 2003 | Techniques for accurate performance evaluation in architecture explorationabstractWe present a system that automatically generates a cycle-accurate and bit-true instruction level simulator (ILS) and a hardware implementation model given a description of a target processor. An ILS can be used to obtain a cycle count for a given program running on the target architecture, while the cycle length, die size, and power consumption can be obtained from the hardware implementation model. These figures allow us to accurately and rapidly evaluate target architectures within an architecture exploration methodology for system-level synthesis. In an architecture exploration scheme, both the ILS and the hardware model must be generated automatically, else a substantial programming and hardware design effort has to be expended in each design iteration. Our system uses the Instruction Set Description language to support the automatic generation of the ILS and the hardware synthesis model, as well as other related tools. George Hadjiyiannis, Srini Devadas |
IEEE Trans. Very Large Scale Integr. Syst. | 2 |
| 2002 | Controlled Physical Random FunctionsabstractA physical random function (PUF) is a random function that can only be evaluated with the help of a complex physical system. We introduce controlled physical random functions (CPUFs) which are PUFs that can only be accessed via an algorithm that is physically bound to the PUF in an inseparable way. CPUFs can be used to establish a shared secret between a physical device and a remote user. We present protocols that make this possible in a secure and flexible way, even in the case of multiple mutually mistrusting parties. Once established, the shared secret can be used to enable a wide range of applications. We describe certified execution, where a certificate is produced that proves that a specific computation was carried out on a specific processor. Certified execution has many benefits, including protection against malicious nodes in distributed computation networks. We also briefly discuss a software licensing application. Blaise Gassend, Dwaine E. Clarke, Marten van Dijk, Srini Devadas |
ACSAC | 4 |
| 2002 | Silicon physical random functionsabstractWe introduce the notion of a Physical Random Function (PUF). We argue that a complex integrated circuit can be viewed as a silicon PUF and describe a technique to identify and authenticate individual integrated circuits (ICs).We describe several possible circuit realizations of different PUFs. These circuits have been implemented in commodity Field Programmable Gate Arrays (FPGAs). We present experiments which indicate that reliable authentication of individual FPGAs can be performed even in the presence of significant environmental variations.We describe how secure smart cards can be built, and also briefly describe how PUFs can be applied to licensing and certification applications. Blaise Gassend, Dwaine E. Clarke, Marten van Dijk, Srini Devadas |
CCS | 4 |
| 2002 | A New Memory Monitoring Scheme for Memory-Aware Scheduling and PartitioningabstractWe propose a low overhead, online memory monitoring scheme utilizing a set of novel hardware counters. The counters indicate the marginal gain in cache hits as the size of the cache is increased, which gives the cache miss-rate as a function of cache size. Using the counters, we describe a scheme that enables an accurate estimate of the isolated miss-rates of each process as a function of cache size under the standard LRU replacement policy. This information can be used to schedule jobs or to partition the cache to minimize the overall miss-rate. The data collected by the monitors can also be used by an analytical model of cache and memory behavior to produce a more accurate overall miss-rate for the collection of processes sharing a cache in both time and space. This overall miss-rate can be used to improve scheduling and partitioning schemes. G. Edward Suh, Srini Devadas, Larry Rudolph |
HPCA | 2 |
| 2002 | Functional vector generation for sequential HDL models under an observability-based code coverage metricabstractDesign validation and verification is the process of ensuring correctness of a design described at different levels of abstraction during the design process. Design validation is the main bottleneck in improving design turnaround time. Currently, simulation is the primary methodology for validation of the first description of a design. In this paper we integrate directed search methods and observability-based code coverage metric (OCCOM) computation into an algorithm for generating test vectors under OCCOM for sequential HDL models. A prototype system for design validation under OCCOM has been built. The system uses repeated coverage computation to minimize the number of vectors generated. Experimental results using the test vector generation system are presented. Farzan Fallah, Pranav Ashar, Srini Devadas |
IEEE Trans. Very Large Scale Integr. Syst. | 3 |
| 2001 | Software-Assisted Cache Replacement Mechanisms for Embedded SystemsabstractWe address the problem of improving cache predictability and performance in embedded systems through the use of software-assisted replacement mechanisms. These mechanisms require additional software controlled state information that affects the cache replacement decision. Software instructions allow a program to kill a particular cache element, i.e. effectively make the element the least recently used element, or keep that cache element, i.e. the element will never be evicted. We prove basic theorems that provide conditions under which kill and keep instructions can be inserted into program code, such that the resulting performance is guaranteed to be as good as or better than the original program run using the standard LRU policy. We developed a compiler algorithm based on the theoretical results that, given an arbitrary program, determines when to perform software-assisted replacement, i.e., when to insert either a kill or keep instruction. Empirical evidence is provided that shows that performance and predictability (worst-case performance) can be improved for many programs. Prabhat Jain, Srini Devadas, Daniel W. Engels, Larry Rudolph |
ICCAD | 2 |
| 2001 | Analytical cache models with applications to cache partitioning
G. Edward Suh, Srini Devadas, Larry Rudolph |
ICS | 2 |
| 2001 | Effects of Memory Performance on Parallel Job Scheduling
G. Edward Suh, Larry Rudolph, Srini Devadas |
JSSPP | 3 |
| 2001 | Functional vector generation for HDL models using linearprogramming and Boolean satisfiabilityabstractOur strategy for automatic generation of functional vectors is based on exercising selected paths in the given hardware description language (HDL) model. The HDL model describes interconnections of arithmetic, logic, and memory modules. Given a path in the HDL model, the search for input stimuli that exercise the path can be converted into a standard satisfiability (SAT) checking problem by expanding the arithmetic modules into logic gates. However, this approach is not very efficient. We present a new HDL-SAT checking algorithm that works directly on the HDL model. The primary feature of our algorithm is a seamless integration of linear-programming techniques for feasibility checking of arithmetic equations that govern the behavior of data-path modules and SAT checking for logic equations that govern the behavior of control modules. This feature is critically important to efficiency, since it avoids module expansion and allows us to work with logic and arithmetic equations whose cardinality tracks the size of the HDL model. We describe the details of the HDL-SAT checking algorithm in this paper. Experimental results that show significant speedups over state-of-the-art gate-level SAT checking methods are included. Farzan Fallah, Srini Devadas, Kurt Keutzer |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 2 |
| 2001 | OCCOM-efficient computation of observability-based code coveragemetrics for functional verificationabstractFunctional simulation is still the primary workhorse for verifying the functional correctness of hardware designs. Functional verification is necessarily incomplete because it is not computationally feasible to exhaustively simulate designs. It is important, therefore, to quantitatively measure the degree of verification coverage of the design. Coverage metrics proposed for measuring the extent of design verification provided by a set of functional simulation vectors should compute statement execution counts (controllability information) and check to see whether effects of possible errors activated by program stimuli can be observed at the circuit outputs (observability information). Unfortunately, the metrics proposed thus far either do not compute both types of information or are inefficient, i.e., the overhead of computing the metric is very large. In this paper, we provide the details of an efficient method to compute an observability-based code coverage metric that can be used while simulating complex hardware description language (HDL) designs. This method offers a more accurate assessment of design verification coverage than line coverage and is significantly more computationally efficient than prior efforts to assess observability information because it breaks up the computation into two phases: functional simulation of a modified HDL model followed by analysis of a flowgraph extracted from the HDL model. Commercial HDL simulators can be directly used for the time-consuming first phase and the second phase can be performed efficiently using concurrent evaluation techniques. Farzan Fallah, Srini Devadas, Kurt Keutzer |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 2 |
| 2000 | Application-specific memory management for embedded systems using software-controlled cachesabstractWe propose a way to improve the performance of embedded processors running data-intensive applications by allowing software to allocate on-chip memory on an application-specific basis. On-chip memory in the form of cache can be made to act like scratch-pad memory via a novel hardware mechanism, which we call column caching. Column caching enables dynamic cache partitioning in software, by mapping data regions to a specified sets of cache “columns” or “ways.” When a region of memory is exclusively mapped to an equivalent sized partition of cache, column caching provides the same functionality and predictability as a dedicated scratchpad memory for time-critical parts of a real-time application. The ratio between scratchpad size and cache size can be easily and quickly varied for each application, or each task within an application. Thus, software has much finer software control of on-chip memory, providing the ability to dynamically tradeoff performance for on-chip memory. Derek Chiou, Prabhat Jain, Larry Rudolph, Srini Devadas |
DAC | 4 |
| 2000 | Observability Analysis of Embedded Software for Coverage-Directed ValidationabstractThe most common approach to checking correctness of a hardware or software design is to verify that a description of the design has the proper behavior as elicited by a series of input stimuli. In the case of software, the program is simply run with the appropriate inputs, and in the case of hardware, its description written in a hardware description language (HDL) is simulated with the appropriate input vectors. In coverage-directed validation, coverage metrics are defined that quantitatively measure the degree of verification coverage of the design. Motivated by recent work on observability-based coverage metrics for models described in a hardware description language, we develop a method that computes an observability-based code coverage metric for embedded software written in a high-level programming language. Given a set of input vectors, our metric indicates the instructions that had no effect on the output. An assignment that was not relevant to generate the output value cannot be considered as being covered. Results show that our method offers a significantly more accurate assessment of design verification coverage than statement coverage. Existing coverage methods for hardware can be used with our method to build a verification methodology for mixed hardware/software or embedded systems. José C. Costa, Srini Devadas, José Monteiro 0001 |
ICCAD | 2 |
| 2000 | Solving covering problems using LPR-based lower boundsabstractUnate and binate covering problems are a subclass of general integer linear programming problems with which several problems in logic synthesis, such as two-level logic minimization and technology mapping, are formulated. Previous branch-and-bound methods for solving these problems exactly use lower bounding techniques based on finding maximal independent sets. In this paper, we examine lower bounding techniques based on linear programming relaxation (LPR) for the covering problem. We show that a combination of traditional reductions (essentiality and dominance) and incremental computation of LPR-based lower bounds can exactly solve difficult covering problems orders of magnitude faster than traditional methods. Farzan Fallah, Stan Y. Liao, Srini Devadas |
IEEE Trans. Very Large Scale Integr. Syst. | 3 |
| 1999 | Simulation Vector Generation from HDL Descriptions for Observability-Enhanced Statement CoverageabstractValidation of RTL circuits remains the primary bottleneck in improving designturnaround time, and simulation remains the primary methodology for validation. Simulation-based validation has suffered from a disconnect between the metrics used to measure the error coverage of a set of simulation vectors, and the vector generation process. This disconnect has resulted in the simulation of virtually endless streams of vectors which achieve enhanced error coverage only infrequently. Another drawback has been that most error coverage metrics proposed have either been too simplistic or too inefficient to compute. Recently, an effective observability-based statement coverage metric was proposed along with a fast companion procedure for evaluating it. The contribution of our work is the development of a vector generation procedure targeting the observability-based statement coverage metric. Our method uses repeated coverage computation to minimize the number of vectors generated. For vector gen... Farzan Fallah, Pranav Ashar, Srini Devadas |
DAC | 3 |
| 1999 | A Methodology for Accurate Performance Evaluation in Architecture ExplorationabstractWe present a system that automatically generates a cycle-accurate and bit-true Instruction Level Simulator (ILS) and a hardware implementation model given a description of a target processor. An ILS can be used to obtain a cycle count for a given program running on the target architecture, while the cycle length, die size, and power consumption can be obtained from the hardware implementation model. These figures allow us to accurately and rapidly evaluate target architectures within an architecture exploration methodology for system-level synthesis. In an architecture exploration scheme,both the ILS and the hardware model must be generated automatically, else a substantial programming and hardware design effort has to be expended in each design iteration. Our system uses the ISDL machine description language to support the automatic generation of the ILS and the hardware synthesis model, as well as other related tools. 1 Introduction Embedded systems typically require low cost and l... George Hadjiyiannis, Pietro Russo, Srini Devadas |
DAC | 3 |
| 1999 | A text-compression-based method for code size minimization in embedded systemsabstractWe address the problem of code-size minimization in VLSI systems with embedded DSP processors. Reducing code size reduces the production cost of embedded systems we use data-compression methods to develop code-size minimization strategies. In our framework, the compressed program consists of a skeleton and a dictionary. We show that the dictionary can be computed by solving a set-covering problem derived from the original program. To execute the compressed code, we describe two methods that have different performance characteristics and different degrees of freedom in compressing the code. We also address performance considerations, and show that they can be incorporated easily into the set-covering formulation, and present experimental results obtained with Texas Instruments' optimizing TMS3220C25 compiler. Stan Y. Liao, Srini Devadas, Kurt Keutzer |
ACM Trans. Design Autom. Electr. Syst. | 2 |
| 1998 | Functional Vector Generation for HDL Models Using Linear Programming and 3-SatisfiabilityabstractOur strategy for automatic generation of functional vectors is based on exercising selected paths in the given hardware description language (HDL) model. The HDL model describes interconnections of arithmetic, logic and memory modules. Given a path in the HDL model, the search for input stimuli that exercise the path can be converted into a standard satisfiability checking problem by expanding the arithmetic modules into logic-gates. However, this approach is not very efficient. Farzan Fallah, Srini Devadas, Kurt Keutzer |
DAC | 2 |
| 1998 | OCCOM: Efficient Computation of Observability-Based Code Coverage Metrics for Functional VerificationabstractFunctional simulation is still the primary workhorse for verifying the functional correctness of hardware designs. Functional verification is necessarily incomplete because it is not computationally feasible to exhaustively simulate designs. It is important therefore to quantitatively measure the degree of verification coverage of the design. Coverage metrics proposed for measuring the extent of design verification provided by a set of functional simulation vectors should compute statement execution counts (controllability information), and check to see whether effects of possible errors activated by program stimuli can be observed at the circuit outputs (observability information). Unfortunately, the metrics proposed thus far, either do not compute both types of information, or are inefficient, i.e., the overhead of computing the metric is very large. In this paper, we provide the details of an efficient method to compute an Observability-based Code COverage Metric (OCCOM) that can be used while simulating complex HDL designs. This method offers a more accurate assessment of design verification coverage than line coverage, and is significantly more computationally efficient than prior efforts to assess observability Information because it breaks up the computation into two phases: Functional simulation of a modified HDL model, followed by analysis of a flowgraph extracted from the HDL model. Commercial HDL simulators can be directly used for the time-consuming first phase, and the second phase can be performed efficiently using concurrent evaluation techniques. Farzan Fallah, Srini Devadas, Kurt Keutzer |
DAC | 2 |
| 1998 | Instruction Selection, Resource Allocation, and Scheduling in the AVIV Retargetable Code GeneratorabstractThe AVIV retargetable code generator produces optimized machine code for target processors with different instruction set architectures AVIV optimizes for minimum code size. Silvina Hanono, Srini Devadas |
DAC | 2 |
| 1998 | An algorithmic approach to optimizing fault coverage for BIST logic synthesisabstractMost approaches to the synthesis of built-in self-test (BIST) circuitry use a manual choose-and-evaluate approach, where a particular BIST generator is chosen and then evaluated by fault-simulating the design with the vectors that the chosen generator generates. We develop an algorithmic synthesis-during-test approach in this paper, wherein the tasks of synthesizing the BIST logic and directed test pattern generation (DTPG) are intertwined to maximize the resulting fault coverage. Our approach is applicable to a variety of BIST strategies including those that use linear- and nonlinear-feedback shift registers. We show how our method can be used to synthesize LFSR polynomials, LFSR seeds, LFSR weights, nonlinear feedback, or bit-fixing logic. Experimental data is presented. Srini Devadas, Kurt Keutzer |
ITC | 1 |
| 1998 | Code density optimization for embedded DSP processors using data compression techniquesabstractCode-size minimization in embedded systems is an important problem because code size directly affects production cost. We address the problem of code compression in systems with embedded DSP processors. We use data-compression methods to develop code-size minimization strategies. In our framework, the compressed program consists of a skeleton and a dictionary. We show that the dictionary can be computed by solving a set-covering problem derived from the original program. We also address performance considerations, and show that they can be incorporated easily into the set-covering formulation. Experimental results are presented. Stan Y. Liao, Srini Devadas, Kurt Keutzer |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 2 |
| 1998 | Sequential logic optimization for low power using input-disabling precomputation architecturesabstractPrecomputation is a recently proposed logic optimization technique which selectively disables the inputs of a logic circuit, thereby reducing switching activity and power dissipation, without changing logic functionality. In sequential precomputation, output values required in a particular clock cycle are selectively precomputed one clock cycle earlier, and the original logic circuit is "turned off" in the succeeding clock cycle. We target a general precomputation architecture for sequential logic circuits, and show that it is significantly more powerful than the architecture previously treated in the literature. The very power of this architecture makes the synthesis of precomputation logic a challenging problem. We present a method to automatically synthesize precomputation logic for this architecture. Up to 66% reduction in power dissipation is possible using the proposed architecture. For many examples, the proposed architecture result in significantly less power dissipation than previously developed methods. José Monteiro 0001, Srini Devadas, Abhijit Ghosh |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 2 |
| 1998 | BDD-based synthesis of extended burst-mode controllersabstractWe examine the implications of a new hazard-free combinational logic synthesis method, which generates multiplexor-based networks from binary decision diagrams (BDD's)-representations of logic functions factored recursively with respect to input variables-on extended burst-mode asynchronous synthesis. First, this method guarantees that there exists a hazard-free BDD-based implementation for every legal extended burst-mode specification. Second, it reduces the constraints on state minimization and assignment, which reduces the number of additional state variables required in many cases. Third, in cases where conditional signals are sampled, it eliminates the need for state variable changes preceding output changes, which reduces overall input-to-output latency. Last, we describe a circuit that exemplifies how the BDD variable ordering affects the path delay. Kenneth Y. Yun, Bill Lin 0001, David L. Dill, Srini Devadas |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 4 |
| 1998 | A new viewpoint on code generation for directed acyclic graphsabstractWe present a new viewpoint on code generation for directed acyclic graphs (DAGs). Our formulation is based on binate covering , the problem of satisfying, with minimum cost, a set of disjunctive clauses, and can take into account commutativity of operators and of the machine model. An important contribution of this work is a set of necessary and sufficient conditions for a valid schedule to be derived, based on the notion of worms and worm-partitions . This set of conditions can be compactly expressed with clauses that relate scheduling to code selection. For the case of one-register machines, we can derive clauses that lead to generation of optimal code for the DAG. Recent advances in exact binate covering algorithms allows us to use this strategy to generate optimal code for large basic blocks. The optimal code generated by our algorithm results in significant reductions in overall code size. Stan Y. Liao, Kurt Keutzer, Steven W. K. Tjiang, Srini Devadas |
ACM Trans. Design Autom. Electr. Syst. | 4 |
| 1998 | A low power, low bandwidth protocol for remote wireless terminals
George Hadjiyiannis, Anantha P. Chandrakasan, Srini Devadas |
Wirel. Networks | 3 |
| 1997 | ISDL: An Instruction Set Description Language for RetargetabilityabstractWe present the Instruction Set Description Language,ISDL, a machine description language used to describetarget architectures to a retargetable compiler. The featuresand flexibility of ISDL enable the description of vastly differentarchitectures, in particular VLIW architectures. ISDL explicitlysupports constraints that define valid operation groupingswithin an instruction, increasing the range of specifiable architectures.We have written a tool that, given an ISDL descriptionof a processor, automatically generates an assembler forit. Ongoing work includes the development of an automaticcode-generator generator. George Hadjiyiannis, Silvina Hanono, Srini Devadas |
DAC | 3 |
| 1997 | Solving Covering Problems Using LPR-Based Lower BoundsabstractUnate and binate covering problems are a special class ofgeneral integer linear programming problems with which several problemsin logic synthesis, such as two-level logic minimization and technologymapping, are formulated. Previous branch-and-bound methodsfor exactly solving these problems use lower-bounding techniques basedon finding maximal independent sets. In this paper we examine lower-boundingtechniques based on linear programming relaxation (LPR) forthe binate covering problem. We show that a combination of traditionalreductions (essentiality and dominance) and incremental computation ofLPR-based lower bounds can exactly solve difficult covering problemsorders of magnitude faster than traditional methods. Stan Y. Liao, Srini Devadas |
DAC | 2 |
| 1997 | Analysis and Evaluation of Address Arithmetic Capabilities in Custom DSP ArchitecturesabstractMany application-specific architectures provideindirect addressing modes with auto-increment/decrementarithmetic.Since these architectures generally do not featurean indexed addressing mode, stack-allocated variablesmust be accessed by allocating address registers and performingaddress arithmetic.Subsuming address arithmeticinto auto-increment/decrement arithmetic improves boththe performance and size of the generated code.Our objective in this paper is to provide a method forcomprehensively analyzing the performance benefits andhardware cost due to an auto-increment/decrement featurethat varies from -l to +l, and allowing access to k addressregisters in an address generator.We provide this methodvia a parameterizable optimization algorithm that operateson a procedure-wise basis.Hence, the optimizationtechniques in a compiler can be used not only to generateefficient or compact code, but also to help the designerof a custom DSP architecture make decisions on addressarithmetic featuers.We present two sets of experimental results based onselected benchmark programs: (1) the values of l and kbeyond which there is little or no improvement in performance,and (2) the values of l and k which result in minimumcode area. Ashok Sudarsanam, Stan Y. Liao, Srini Devadas |
DAC | 3 |
| 1997 | Switching activity estimation using limited depth reconvergent path analysisabstractWe describe a method of polynomial simulation to calculate switching activities in a general-delay combinational logic circuit.This method is a generalization of the exact signal probability evaluation method due to Parker and McCluskey, which as been extended to handle temporal correlation and arbitrary transport delays.Our method is parameterized by a single parameter 1, which determines the speed-accuracy tradeoff.1 indicates the depth in terms of logic levels over which spatial signal correlation is taken into account.This is done by only taking into account reconvergentpaths whose length is at most 1.The rationale is that ignoring spatial correlation for signals that reconverge after many levels of logic introduces negligible error.We present results that show that the error in the switching activity and power estimates is very small even for small values of 1.In fact, for most of the examples we tried, power estimates withl= 1 are within 5% of the exact.However, this error can be higher than 20 % for some examples.More robust estimates are obtained with I= 2, providing a good compromise between speed and accuracy.' 'llesupporf of alogic function is the set of primary inputs thnt the function depends on. José C. Costa, José Monteiro 0001, Srini Devadas |
ISLPED | 3 |
| 1997 | Estimation of average switching activity in combinational logic circuits using symbolic simulationabstractWe address the problem of estimating the average switching activity of combinational circuits under random input sequences. Switching activity is strongly affected by gate delays, and for this reason we use a variable delay model in estimating switching activity. Unlike most probabilistic methods that estimate switching activity, our method takes into account correlation caused at internal gates in the circuit due to reconvergence of input signals. This method assumes a particular delay model and further assumes that the primary inputs to the combinational circuit are uncorrelated. Both these assumptions can be relaxed at the cost of increased complexity. We describe extensions to handle transmission gates and inertial delays in this paper. José Monteiro 0001, Srini Devadas, Abhijit Ghosh, Kurt Keutzer, Jacob K. White 0001 |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 2 |
| 1996 | Scheduling Techniques to Enable Power ManagementabstractShut-down" techniques are effective in reducing the power dissipation of logic circuits.Recently, methods have been developed that identify conditions under which the output of a module in a logic circuit is not used for a given clock cycle.When these conditions are met, input latches for that module are disabled, thus eliminating any switching activity and power dissipation.In this paper, we introduce these power management techniques in behavioral synthesis.We present a scheduling algorithm which maximizes the "shut-down" period of execution units in a system.Given a throughput constraint and the number of execution units available, the algorithm first schedules operations that generate controlling signals and activates only those modules whose result is eventually used.We present results which show that this scheduling technique can save up to 40% in power dissipation. José Monteiro 0001, Srini Devadas, Pranav Ashar, Ashutosh Mauskar |
DAC | 2 |
| 1996 | An observability-based code coverage metric for functional simulationabstractFunctional simulation is the most widely used method for design verification. At various levels of abstraction, e.g., behavioral, register-transfer level and gate level, the designer simulates the design using a large number of vectors attempting to debug and verify the design. A major problem with functional simulation is the lack of good metrics and tools to evaluate the quality of a set of functional vectors. Metrics used currently are based on instruction counts and are quite simplistic. Designers are forced to use ad-hoc methods to terminate functional simulation, e.g., CPU time limitations, We propose a new metric for measuring the extent of design verification provided by a set of functional simulation vectors. This metric is universal, and can be used uniformly for all designs. Our metric computes observability information to determine whether effects of errors that are activated by the program stimuli can be observed at the circuit outputs. We provide preliminary experimental evidence that supports the validity of the proposed metric. We believe that using this metric in design verification will result in higher-quality functional tests and improved correctness checking. Srini Devadas, Abhijit Ghosh, Kurt Keutzer |
ICCAD | 1 |
| 1996 | Addendum to "Synthesis of robust delay-fault testable circuits: Theory"abstractFor original paper see ibid., vol. 11, pp. 87-101 (Jan. 1992). The robust nature of the gate delay fault tests corresponding to Theorems 7 and 8 in the original paper is clarified and described in greater detail. There are two types of robust tests for gate delay faults: a hazard-free robust test for a gate delay fault on a gate g is a robust test where only paths that pass through g are event sensitized; a general robust test for a gate delay fault on a gate g is a robust test where paths that do not pass through g can be event sensitized. The two types of robust tests are illustrated. Srini Devadas, Kurt Keutzer |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 1 |
| 1996 | Storage Assignment to Decrease Code SizeabstractDSP architectures typically provide indirect addressing modes with autoincrement and decrement. In addition, indexing mode is generally not available, and there are usually few, if any, general-purpose registers. Hence, it is necessary to use address registers and perform address arithmetic to access automatic variables. Subsuming the address arithmetic into autoincrement and decrement modes improves the size of the generated code. In this article we present a formulation of the problem of optimal storage assignment such that explicit instructions for address arithmetic are minimized. We prove that for the case of a single address register the decision problem is NP-complete, even for a single basic block. We then generalize the problem to multiple address registers. For both cases heuristic algorithms are given, and experimental results are presented. Stan Y. Liao, Srini Devadas, Kurt Keutzer, Steven W. K. Tjiang, Albert R. Wang |
ACM Trans. Program. Lang. Syst. | 2 |
| 1996 | Correction to "Power Estimation Methods for Sequential Logic Circuits" [Correspondence]
Chi-Ying Tsui, José Monteiro 0001, Massoud Pedram, Srini Devadas, Alvin M. Despain, Bill Lin 0001 |
IEEE Trans. Very Large Scale Integr. Syst. | 4 |
| 1995 | A Survey of Optimization Techniques Targeting Low Power VLSI CircuitsabstractWe survey state-of-the-art optimization methods that target low power dissipation in VLSI circuits. Optimizations at the circuit, logic, architectural and system levels are considered. Srini Devadas, Sharad Malik |
DAC | 1 |
| 1995 | Code Optimization Techniques for Embedded DSP MicroprocessorsabstractWe address the problem of code optimization for embedded DSP microprocessors.Such processors (e.g., those in the TMS320 series) have highly irregular datapaths, and conventional code generation methods typically result in inefficient code.In this paper we formulate and solve some optimization problems that arise in code generation for processors with irregular datapaths.In addition to instruction scheduling and register allocation, we also formulate the accumulator spilling and mode selection problems that arise in DSP microprocessors.We present optimal and heuristic algorithms that determine an instruction schedule simultaneously optimizing accumulator spilling and mode selection.Experimental results are presented. Stan Y. Liao, Srini Devadas, Kurt Keutzer, Steven W. K. Tjiang, Albert R. Wang |
DAC | 2 |
| 1995 | Instruction selection using binate covering for code size optimizationabstractWe address the problem of instruction selection in code generation for embedded DSP microprocessors. Such processors have highly irregular data-paths, and conventional code generation methods typically result in inefficient code. Instruction selection can be formulated as directed acyclic graph (DAG) covering. Conventional methods for instruction selection use heuristics that break up the DAG into a forest of trees and then cover them independently. This breakup can result in suboptimal solutions for the original DAG. Alternatively, the DAG covering problem can be formulated as a binate covering problem, and solved exactly or heuristically using branch-and-bound methods. We show that optimal instruction selection on a PAG in the case of accumulator-based architectures requires a partial scheduling of nodes in the DAG, and we augment the binate covering formulation to minimize spills and reloads. We show how the irregular data transfer costs of typical DSP data-paths can be modeled in the binate covering formulation. Stan Y. Liao, Srini Devadas, Kurt Keutzer, Steven W. K. Tjiang |
ICCAD | 2 |
| 1995 | Storage Assignment to Decrease Code SizeabstractDSP architectures typically provide indirect addressing modes with auto-increment and decrement. In addition, indexing mode is not available, and there are usually few, if any, general-purpose registers. Hence, it is necessary to use address registers and perform address arithmetic to access automatic variables. Subsuming the address arithmetic into auto-increment and auto-decrement modes improves the size of the generated code. Stan Y. Liao, Srini Devadas, Kurt Keutzer, Steven W. K. Tjiang, Albert R. Wang |
PLDI | 2 |
| 1995 | Synthesis of hazard-free multilevel logic under multiple-input changes from binary decision diagramsabstractWe describe a new method for directly synthesizing a hazard-free multilevel logic implementation from a given logic specification. The method is based on free/ordered Binary Decision Diagrams (BDD's), and is naturally applicable to multiple-output logic functions. Given an incompletely-specified (multiple-output) Boolean function, the method produces a multilevel logic network that is hazard-free for a specified set of multiple-input changes. We assume an arbitrary (unbounded) gate and wire delay model under a pure delay (PD) assumption, we permit multiple-input changes, and we consider both static and dynamic hazards under the fundamental-mode assumption. Our framework is thus general and powerful. While it is not always possible to generate hazard-free implementations using our technique, we show that in some cases hazard-free multilevel implementations can be generated when hazard-free two-level representations cannot be found. This problem is generally regarded as a difficult problem and it has important applications in the field of asynchronous design. The method has been automated and applied to a number of examples.> Bill Lin 0001, Srini Devadas |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 2 |
| 1995 | Probabilistic manipulation of Boolean functions using free Boolean diagramsabstractWe propose a data structure for Boolean functions termed "the free Boolean diagram." A free Boolean diagram allows decision vertices as in the conventional binary decision diagram, but also allows function vertices corresponding to the AND and XOR functions. It has been shown previously that the equivalence of two free Boolean diagrams can be decided probabilistically in polynomial time. Based on the equivalence checking method, we develop a set of algorithms for the probabilistic construction of free Boolean diagrams from multilevel combinational logic circuits, and for their manipulation. These algorithms are modified versions of reduced, ordered binary decision diagram manipulation methods. We provide the implementation details of a free Boolean diagram package. We show that functions difficult to verify using reduced, ordered binary decision diagrams can be verified using the free Boolean diagrams package using substantially less memory.> Amelia Shen, Srini Devadas, Abhijit Ghosh |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 2 |
| 1995 | Power estimation methods for sequential logic circuitsabstractRecently developed methods for power estimation have primarily focused on combinational logic. We present a framework for the efficient and accurate estimation of average power dissipation in sequential circuits. Switching activity is the primary cause of power dissipation in CMOS circuits. Accurate switching activity estimation for sequential circuits is considerably more difficult than that for combinational circuits, because the probability of the circuit being in each of its possible states has to be calculated. The Chapman-Kolmogorov equations can be used to compute the exact state probabilities in steady state. However, this method requires the solution of a linear system of equations of size 2/sup N/ where N is the number of flip-flops in the machine. We describe a comprehensive framework for exact and approximate switching activity estimation in a sequential circuit. The basic computation step is the solution of a nonlinear system of equations which is derived directly from a logic realization of the sequential machine. Increasing the number of variables or the number of equations in the system results in increased accuracy. For a wide variety of examples, we show that the approximation scheme is within 1-3% of the exact method, but is orders of magnitude faster for large circuits. Previous sequential switching activity estimation methods can have significantly greater inaccuracies.> Chi-Ying Tsui, José Monteiro 0001, Massoud Pedram, Srini Devadas, Alvin M. Despain, Bill Lin 0001 |
IEEE Trans. Very Large Scale Integr. Syst. | 4 |
| 1994 | Automatic Verification of Pipelined MicroprocessorsabstractAbstract- We address the problem of automatically verifying large digital designs at the logic level, against high-level specifications. In this paper, we present a methodology which allows for the verification of a specific class of synchronous machines, namely pipelined microprocessors. The specification is the instruction set of the microprocessor with respect to which the correctness property is to be verified. A relation, namely the β-relation, is established between the input/output behavior of the implementation and specification. The relation corresponds to changes in the input/output behavior that result from pipelining, and takes into account data hazards and control transfer instructions that modify pipelined execution. The correctness requirement is that the β-relation hold between the implementation and specification. We use symbolic simulation of the specification and implementation to verify their functional equivalence. We characterize the pipelined and unpipelined microprocessors as definite machines (i.e. a machine in which for some constant k, the output of the machine depends only on the last k inputs) for verification purposes. We show that only a small number of cycles, rather than exhaustive state transition graph traversal and state enumeration, have to be simulated for each machine to verify whether the implementation is in β-relation with the specification. Experimental results are presented. 1 Vishal Bhagwati, Srini Devadas |
DAC | 2 |
| 1994 | A Methodology for Efficient Estimation of Switching Activity in Sequential Logic CircuitsabstractW e describe a computationally ecient s c heme to approximate average switching activity in sequential circuits which requires the solution of a non-linear system of equations of size N, where the variables correspond to state line probabilities.W e show that the approximation method is within 3% of the exact Chapman-Kolmogorov method, but is orders of magnitude faster for large circuits.Previous sequential switching activity estimation methods can have signi cantly greater inaccuracies. José Monteiro 0001, Srini Devadas, Bill Lin 0001 |
DAC | 2 |
| 1994 | Precomputation-based sequential logic optimization for low power
Mazhar Alidina, José Monteiro 0001, Srini Devadas, Abhijit Ghosh, Marios C. Papaefthymiou |
ICCAD | 3 |
| 1994 | Synthesis of hazard-free multi-level logic under multiple-input changes from binary decision diagrams
Bill Lin 0001, Srini Devadas |
ICCAD | 2 |
| 1994 | Performance-driven synthesis of asynchronous controllers
Kenneth Y. Yun, Bill Lin 0001, David L. Dill, Srini Devadas |
ICCAD | 4 |
| 1994 | Event-based verification of synchronous, globally controlled, logic designs against signal flow graphsabstractWe address the problem of automatically verifying large digital designs at the logic level, against high-level specifications. We present a technique which allows for the verification of a specific class of systems, namely systems with synchronous globally timed control. To a first approximation, these are systems where a single controller directs the data through the data path and decides (globally) when to move the data. We address the verification of these systems against a Signal Flow Graph (SFG) specification, or a specification in an applicative language such as SILAGE. In this paper, a method is presented for verifying the implementation against an intermediate SFG, which is an expansion of the original specification in such a way that all the operations correspond to Register Transfers (RT's) in the implementation. In this SFG, complex arithmetic operations such as multiplications may have been decomposed into simpler ones, such as shifts and additions, and new operations may have been introduced for maintaining iteration indices and computing addresses of memory locations. SFG's can be viewed as maximally parallel synchronous machines. Both the implementation and the specification are then Finite State Machines, having string functions (input/output mappings) associated with them. Correctness is taken to mean that a certain relation (the /spl beta/-relation) holds between these string functions.> Filip Van Aelten, Jonathan Allen, Srini Devadas |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 3 |
| 1994 | Event suppression: improving the efficiency of timing simulation for synchronous digital circuitsabstractTiming simulation is a widely used method to verify the timing behavior of a design. In a synchronous digital system the timing property that needs to be verified is that there is no event at the outputs of the combinational parts of the circuit at or after time /spl tau/, the clock period. In this paper we first show that conventional timing simulation applied to this problem has exponential complexity. Next we demonstrate that for this problem a complete history of circuit activity before time /spl tau/ is not needed. We exploit this observation and present an event suppression method that potentially leads to an exponential reduction in the number of events that need to be processed during simulation. This is backed by encouraging experimental results.> Srini Devadas, Kurt Keutzer, Sharad Malik, Albert R. Wang |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 1 |
| 1994 | Precomputation-based sequential logic optimization for low powerabstractWe 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. The primary optimization step is the synthesis of the precomputation logic, which computes the output values for a subset of input conditions. If the output values can be precomputed, the original logic circuit can be "turned off" in the next clock cycle and will have substantially reduced switching activity. The size of the precomputation logic determines the power dissipation reduction, area increase and delay increase relative to the original circuit. Given a logic-level sequential circuit, we present an automatic method of synthesizing precomputation 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.> Mazhar Alidina, José Monteiro 0001, Srini Devadas, Abhijit Ghosh, Marios C. Papaefthymiou |
IEEE Trans. Very Large Scale Integr. Syst. | 3 |
| 1994 | Certified timing verification and the transition delay of a logic circuitabstractMost research in timing verification has implicitly assumed a single vector floating mode computation of delay which is an approximation of the multivector transition delay. In this paper we examine the transition delay of a circuit and demonstrate that the transition delay of a circuit can differ from the floating delay of a circuit. We then provide a procedure for directly calculating the transition delay of a circuit. The most practical benefit of this procedure is the fact that it not only results in a delay calculation but outputs a vector sequence that may be timing simulated to certify static timing verification.> Srini Devadas, Kurt Keutzer, Sharad Malik, Albert R. Wang |
IEEE Trans. Very Large Scale Integr. Syst. | 1 |
| 1993 | Boolean factorization using multiple-valued minimizationabstractWe show that the problem of factoring a sum-of-products representation of a logic function can be transformed into one of multiple-valued prime generation followed by branch-and-bound covering. We give a factorization method that generates potential Boolean factors by generating the primes of a multiple-valued function with an associated don't-care set. A covering problem is solved wherein a set of primes with minimal cost is selected to obtain a Boolean factorization. This method can exploit Boolean identifiers in factorization such as a-a = a-a = a. Common factors across a set of Boolean functions can be identified by using multiple-output prime generation and covering. We show how all the kernels of an expression can be generated by generating the primes of a multiple-valued function. A covering step can be used to arrive at an algebraic factorization. Stan Y. Liao, Srini Devadas, Abhijit Ghosh |
ICCAD | 2 |
| 1993 | Retiming sequential circuits for low powerabstractSwitching activity is the primary cause of power dissipation in CMOS combinational and sequential circuits. We give a method of estimating power in pipelined sequential CMOS circuits that accurately models the correlation between the vectors applied to the combinational logic of the circuit. We explore the implications of the observation that the switching activity at flip-flop outputs in a synchronous sequential circuit can be significantly less than the activity at the flip-flop inputs. We present a retiming method that targets the power dissipation of a sequential circuit. José Monteiro 0001, Srini Devadas, Abhijit Ghosh |
ICCAD | 2 |
| 1993 | Probabilistic construction and manipulation of free Boolean diagramsabstractWe propose a data structure for Boolean functions termed the Free Boolean Diagram (FBD). We extend a previous result to show that the equivalence of two Free Boolean Diagrams can be decided probabilistically in polynomial time. Based on the equivalence checking method, we develop a set of algorithms for the probabilistic construction of Free Boolean Diagrams from multilevel combinational logic circuits, and for their manipulation. These algorithms are modified versions of ordered Binary Decision Diagram manipulation methods. We provide the implementation details of a Free Boolean Diagram package. Results on applying this package to problems in combinational logic verification are presented. Amelia Shen, Srini Devadas, Abhijit Ghosh |
ICCAD | 2 |
| 1993 | A synthesis-based test generation and compaction algorithm for multifaults
Srini Devadas, Kurt Keutzer, Sharad Malik |
J. Electron. Test. | 1 |
| 1993 | Guest editorial
Srini Devadas, Petra Michel |
J. Electron. Test. | 1 |
| 1993 | Gate-Delay-Fault Testability Properties of Multiplexor-Based Networks
Pranav Ashar, Srini Devadas, Kurt Keutzer |
Formal Methods Syst. Des. | 2 |
| 1993 | Path-delay-fault testability properties of multiplexor-based networks
Pranav Ashar, Srini Devadas, Kurt Keutzer |
Integr. | 2 |
| 1993 | Verification of relations between synchronous machinesabstractUses string function theory to develop an efficient methodology for the verification of logic implementations against behavioral specifications. First, the authors define five primitive relations between string functions, other than strict automata equivalence, namely: don't care times, parallelism, encoding, input don't care and output don't care relations. These relations have attributes, For instance, the parallelism relation has an attribute corresponding to the degree of parallelism. For each of these primitive relations, the authors derive transformations on the specification and the implementation such that the relation holds between the specification and implementation if and only if the transformed circuits exhibit the same input/output behavior. This reduces the problem of verifying primitive relations to automata equivalence checking. They enlarge the set of relations between specifications and implementations by including arbitrary compositions of the five primitive relations. To reduce the cost of verifying such a composite relation, the authors show that, given an arbitrary composite relation, a fixed order composite relation can be constructed under certain assumptions), where the primitive relations occur at most once in a predetermined order, such that the original relation holds between two machines if and only if the fixed order relation holds. For the fixed order composite relation, they derive again transformations on the specification and the implementation which reduce verifying the composite relation to performing one equivalence check. The end result is a sound and complete proof method for proving arbitrary compositions of relations by transforming the specification and the implementation and performing an equivalence check on the transformed finite state machines.> Filip Van Aelten, Jonathan Allen, Srini Devadas |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 3 |
| 1993 | Delay-fault test generation and synthesis for testability under a standard scan design methodologyabstractThe problems of test generation and synthesis aimed at producing VLSI sequential circuits that are delay-fault testable under a standard scan design methodology are considered. Theoretical results regarding the standard scan-delay testability of finite state machines (FSMs) described at the state transition graph (STG) level are given. It is shown that a one-hot coded and optimized FSM whose STG satisfies a certain property is guaranteed to be fully gate-delay-fault testable under standard scan. This result is extended to arbitrary-length encodings, and a heuristic state assignment algorithm that results in highly gate-delay-fault testable sequential FSMs is developed. The authors also consider the problem of delay test generation for large sequential circuits and modify a PODEM-based combinational test pattern generator. The modifications involve a two-time-frame expansion of the combinational logic of the circuit and the use of backtracking heuristics tailored for the problem. A version of the scan shifting technique is also used in the test pattern generator. Test generation, flip-flop ordering, flip-flop selection and test set compaction results on large benchmark circuits are presented.> Kwang-Ting Cheng, Srini Devadas, Kurt Keutzer |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 2 |
| 1993 | Comparing two-level and ordered binary decision diagram representations of logic functionsabstractAn example is given of a class of functions with 2n+logn inputs that have two-level or sum-of-products representations containing n/sup 2/ product terms and ordered binary decision diagram representations that have at least Omega (1/sup n/2/) vertices under any possible variable ordering.> Srini Devadas |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 1 |
| 1993 | Computation of floating mode delay in combinational circuits: theory and algorithmsabstractAddresses the problem of accurately computing the delay of a combinational logic circuit in the floating mode of operation. (In this mode the state of the circuit is considered to be unknown when a vector is applied at the inputs.) It is well known that using the length of the topologically longest path as an estimate of circuit delay may be pessimistic since this path may be false, i.e., it cannot propagate an event. Thus, the true delay corresponds to the length of the longest true path. This forces one to examine the conditions under which a path is true. The authors introduce the notion of static cosensitization of paths which leads to necessary and sufficient conditions for determining the truth or falsity of a single path, or a set of paths. The authors apply these results to develop a delay computation algorithm that has the unique feature that it is able to determine the truth or falsity of entire sets of paths simultaneously. This algorithm uses conventional stuck-at-fault testing techniques to arrive at a delay computation method that is both correct and computationally practical, even for particularly difficult circuits.> Srini Devadas, Kurt Keutzer, Sharad Malik |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 1 |
| 1993 | Computation of floating mode delay in combinational circuits: practice and implementationabstractDelay computation in combinational logic circuits is complicated by the existence of unsensitizable (false) paths and this problem is arising with increasing frequency in circuits produced by high-level synthesis procedures. Various sensitization conditions have been proposed in the past to eliminate false paths in logic circuits, but the authors use a recently developed single-vector condition, that is known to be necessary and sufficient for a path to be responsible for the delay of a circuit (i.e., true) in the floating delay model. They build on this theory and develop an efficient and correct delay computation algorithm, for the floating mode delay. The algorithm uses a technique called timed-test generation and can be incorporated into any stuck-at fault test generation framework. The authors describe in detail an implementation of the timed-test generation algorithm that uses both logical and timed forward/backward implication and backtrace procedures to simultaneously prove the truth or falsity of sets of paths in the circuit. Logical and temporal conflict detection during implication and backtrace are used to speed up the algorithm. Unlike previous techniques, the algorithm remains highly efficient: even when a large number of distinct gate and path delays exist in the given circuit.> Srini Devadas, Kurt Keutzer, Sharad Malik, Albert R. Wang |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 1 |
| 1993 | Sequential test generation and synthesis for testability at the register-transfer and logic levelsabstractThe problem of test generation for nonscan sequential VLSI circuits is addressed. A novel method of test generation that efficiently generates test sequences for stuck-at faults in the logic circuit by exploiting register-transfer-level (RTL) design information is presented. The approach is targeted at circuits with highly connected state transition graphs (STGs) as in data paths, but explicit use is not made of the STG. The efficacy of the method stems from the use of the RTL description and good heuristics. The authors have successfully generated tests for entire chips with large numbers of latches within reasonable amounts of CPU time and have obtained maximum fault coverage. The algorithms require significantly smaller times than other test generators. A synthesis procedure that produces an optimized, fully testable logic implementation of a sequential circuit from a RTL description of the sequential circuit is also described. Datapath-controller circuits as well as digital signal processors whose STGs are very large, can be synthesized. The problem of synthesis of sequential logic for testability is also addressed.> Abhijit Ghosh, Srini Devadas, A. Richard Newton |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 2 |
| 1993 | Statistical timing analysis of combinational logic circuitsabstractEfficient methods for computing an exact probability distribution of the delay of a combinational circuit, given probability distributions for the gate and wire delays, are developed. The derived distribution can give the probability that a combinational circuit will achieve a certain performance, across the possible range. This information can then be used to predict the expected performance of the entire circuit. The techniques presented target fast analysis as well as reduced memory requirements. The notion of a correct approximation, based on convex inequality, which never overestimates the percentage of circuits that will achieve any given performance is defined. It is shown that given the assumption that all the topologically longest paths are responsible for the delay, the computation technique provides a correct probabilistic measure in the sense given above. Methods are given to identify and to ignore false paths in the probabilistic analysis, so as to obtain correct and less pessimistic answers to the performance prediction question. Some practical results are given for a number of benchmark combinational circuits.> Horng-Fei Jyu, Sharad Malik, Srini Devadas, Kurt Keutzer |
IEEE Trans. Very Large Scale Integr. Syst. | 3 |
| 1992 | Certified Timing Verification and the Transition Delay of a Logic Circuit
Srini Devadas, Kurt Keutzer, Sharad Malik, Albert R. Wang |
DAC | 1 |
| 1992 | Estimation of Average Switching Activity in Combinational and Sequential Circuits
Abhijit Ghosh, Srini Devadas, Kurt Keutzer, Jacob K. White 0001 |
DAC | 2 |
| 1992 | Automatic generation and verification of sufficient correctness properties for synchronous processorsabstractA general strategy for automatically generating and verifying sufficient correctness properties for a broad class of synchronous processors is presented. Given a particular specification and implementation pair, it is shown how basic correctness properties can be algorithmically translated into a set of computation tree logic (CTL) formulae which are sufficient for equivalence between the behavioral and logic descriptions. Preliminary experimental results on the verification of microcoded and array processors are presented.> Filip Van Aelten, Stan Y. Liao, Jonathan Allen, Srini Devadas |
ICCAD | 4 |
| 1992 | Verification of asynchronous interface circuits with bounded wire delaysabstractThe 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 circuit behavior described as a classical flow table, under the fundamental mode of operation, is considered. A procedure for extracting the complete set of possible flow tables from a gate-level description of an asynchronous circuit under the bounded wire delay model is given. Given an extracted flow table and the initial flow table specification, procedures for constructing a product flow table so as to check for machine equivalence are discussed.> Srini Devadas, Kurt Keutzer, Sharad Malik, Albert R. Wang |
ICCAD | 1 |
| 1992 | On average power dissipation and random pattern testability of CMOS combinational logic networksabstractThe implications of the observation that the probability of the occurrence of a transition on a wire of a circuit affects both the average power dissipation and the random pattern testability of a circuit are investigated. It is shown that restructuring a logic circuit can significantly affect its average power dissipation. Various methods for the synthesis of combinational logic networks are presented and the effect of different algorithms on the power dissipation of the circuit is demonstrated. The dual problem of improving the random pattern testability of logic circuits is emphasized. It is shown that modifying the signal probabilities can significantly affect the random pattern testability of a circuit.> Amelia Shen, Abhijit Ghosh, Srini Devadas, Kurt Keutzer |
ICCAD | 3 |
| 1992 | Statistical Timing Analysis of Combinational CircuitsabstractThe authors develop efficient methods for computing an exact probability distribution of the delay of a combinational circuit, given probability distributions for the gate and wire delays. The derived distribution can give the probability that a combinational circuit will achieve a certain performance, across the possible range. The techniques target fast analysis as well as reduced memory requirements. The authors define a notion of falsity of paths when dealing with probability distributions on gate and wire delays, and they give methods for identifying and ignoring false paths in their probabilistic analysis, so as to obtain correct and accurate answers to the performance prediction question. Some results and comparisons are given for a number of combinational circuit benchmarks.> Srini Devadas, Horng-Fei Jyu, Kurt Keutzer, Sharad Malik |
ICCD | 1 |
| 1992 | Boolean satisfiability and equivalence checking using general Binary Decision Diagrams
Pranav Ashar, Abhijit Ghosh, Srini Devadas |
Integr. | 3 |
| 1992 | Necessary and sufficient conditions for hazard-free robust transistor stuck-open-fault testability in multilevel networksabstractThe authors address the problem of synthesizing circuits that are highly testable for transistor stuck-open fault testability in arbitrary, multilevel networks. They consider single stuck-open faults that are detectable using two-pattern tests, under a robust fault model wherein hazards, races, or glitches cannot invalidate a test. Using these results the authors show that algebraic factorization, including the constrained use of the complement, can be used to synthesize fully-stuck-open-fault testable multilevel networks. They provide a comprehensive set of practical results.> Michael J. Bryan, Srini Devadas, Kurt Keutzer |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 2 |
| 1992 | Synthesis of robust delay-fault-testable circuits: theoryabstractThe authors give a comprehensive theoretical framework for the analysis and synthesis of delay-fault-testable combinational logic circuits. For each of the common models of delay-fault testability, robust gate-delay faults and robust path-delay faults, they provide the necessary and sufficient conditions for complete testability under that model for two-level circuits. The authors describe the conditions in terminology common to two-level minimization and show their relationship to properties produced by two-level minimizers. Similar conditions for multilevel networks are presented. It is shown that constrained algebraic factorization is required to retain complete gate-delay-fault testability beginning from a two-level network. The authors present preliminary experimental results using these synthesis techniques.> Srini Devadas, Kurt Keutzer |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 1 |
| 1992 | Synthesis of robust delay-fault-testable circuits: practiceabstractThe authors show how an orchestration of combinational synthesis for testability approaches can result in logic-level implementations of large integrated circuit designs that are completely robustly gate-delay-fault and path-delay-fault testable. For control portions of VLSI circuits, Boolean covering and algebraic factorization procedures that guarantee path-delay-fault testability are used, starting from a sum-of-products representation of a function. Hierarchical composition rules are used in the synthesis of regular structures occurring in data path portions, such as parity generators and arithmetic units. It is shown how test vectors to detect all path delay faults can be obtained as a by-product of the synthesis process. These techniques were used on circuits with over 5000 gates, and preliminary experimental results on a data encryption chip, a small microprocessor, and a speech recognition chip are presented.> Srini Devadas, Kurt Keutzer |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 1 |
| 1992 | Validatable nonrobust delay-fault testable circuits via logic synthesisabstractThe authors advocate a synthesis approach to delay-fault testing, wherein completely path-delay-fault testable circuits are automatically synthesized, meeting area and performance requirements. They give necessary and sufficient conditions for validatable nonrobust fault testability of paths in arbitrary multilevel networks. Validatable nonrobust testing as opposed to robust testing offers degrees of freedom that enable the development of efficient synthesis procedures that target delay-fault testability, and also provides a means of producing compact test vector sets. The authors then focus on the development of synthesis procedures that produce networks that are fully testable under the nonrobust fault model. They show that primality and irredundancy are both a necessary and sufficient condition for complete validatable nonrobust testability in the two-level case. They prove that synthesizing a multilevel network using algebraic factorization retains complete validatable nonrobust testability. Preliminary results that verify the procedures are reported.> Srini Devadas, Kurt Keutzer |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 1 |
| 1992 | Estimation of power dissipation in CMOS combinational circuits using Boolean function manipulationabstractIt is shown that a simplified model of power dissipation relates maximizing dissipation to maximizing gate output activity, appropriately weighted to account for differing load capacitances. To find the input or input sequence that minimizes the weighted activity, algorithms are given for transforming the problem to a weighted max-satisfiability problem, and exact and approximate algorithms for solving weighted max-satisfiability are presented. Algorithms for constructing the max-satisfiability problem for both dynamic and static CMOS, where for the latter dissipation caused by glitching is considered, are presented. The authors present efficient exact and approximate methods for solving weighted max-satisfiability and show that these methods are viable for large-scale problems through examination of experimental results.> Srini Devadas, Kurt Keutzer, Jacob K. White 0001 |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 1 |
| 1992 | Heuristic minimization of Boolean relations using testing techniquesabstractA Boolean relation is a one-to-many multioutput Boolean mapping and is a generalization of incompletely specified logic functions. Boolean relations arise in several contexts (for instance, in a finite state machine with sets of equivalent states). Minimization of Boolean relations is important from the point of view of synthesis, especially synthesis for testability. A fast heuristic procedure for finding an optimal sum-of-products representation for a function compatible with a Boolean relation is described. Starting with an initial function compatible with the relation, a process of iterative logic improvement based on test generation techniques is used to derive a minimal function.> Abhijit Ghosh, Srini Devadas, A. Richard Newton |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 2 |
| 1991 | Robust Delay-Fault Test Generation and Synthesis for Testability Under A Standard Scan Design MethodologyabstractOne of the principal reasons that robust delay-fault testing has not been used extensively in industry is that the application of a robust test vector pair to the combinational logic portion of a VLSI sequential circuit requires that the memory elements in the circuit be enhanced scan flip flops, i.e. flip-flops that can store, not just one, but two bits of state.This is because an arbitrary vector pair may not be able to be robustly applied to a sequential circuit under a standard scan design methodology.In this paper, we address the problem of test generation for, and the synthesis of, VLSI sequential circuits that are robustly delay-fault testable under a standard scan design methodology.We present synthesis and test results on several real designs. Kwang-Ting Cheng, Srini Devadas, Kurt Keutzer |
DAC | 2 |
| 1991 | A Synthesis-Based Test Generation and Compaction Algorithm for MultifaultsabstractBecauseof its inherent complexity, the problem Multifault Compaction forFlattenable Circuits 3.1 Srini Devadas, Kurt Keutzer, Sharad Malik |
DAC | 1 |
| 1991 | Verification of Relations Between Synchronous MachinesabstractThe problem of implementation verification at the behavioral level is addressed. A formalism is needed for specifying synchronous circuits and expressing correctness requirements that leave room for modifying the input/output behavior of the implementation. Furthermore, a procedure is needed to verify these requirements. The authors model both specifications and implementations as synchronous logic circuits, and cast the correctness requirements as relations between string functions associated with a specification and an implementation. They define six primitive relations between string functions, namely delay, don't care times, parallelism, encoding, input don't care, and output don't care relations. These relations have attributes, for instance, a delay time for the delay relation. It is shown that these relations can be verified by transforming the specification and the implementation and performing an input/output equivalence check. The authors also allow for composite relations, and show that, given an arbitrary composite relation, a closely related composition can be constructed which can be verified through one equivalence check. Experimental results are presented.> Filip Van Aelten, Jonathan Allen, Srini Devadas |
ICCAD | 3 |
| 1991 | Delay Computation in Combinational Logic Circuits: Theory and AlgorithmsabstractThe authors provide necessary and sufficient conditions for a path to be true in the floating mode of operation. Static cosensitization is introduced as a necessary condition, which allows one to avoid the problem of identifying false paths as responsible for delay. The results are extended to determine the truth or falsity of entire sets of paths simultaneously by expressing them in terms of the testability of a multifault in an ENF (equivalent normal form) expression. This result is applied directly to an unmodified multilevel circuit. Because the circuits that are most troublesome for false-path-eliminating static timing analyzers are those with millions of paths, and in particular millions of longest paths, the ability to handle entire sets of paths simultaneously results in a very efficient delay computation procedure. This is demonstrated by the results from a preliminary implementation of the algorithm.> Srini Devadas, Kurt Keutzer, Sharad Malik |
ICCAD | 1 |
| 1991 | Finite State Machine Decomposition by Transition PairingabstractThe authors develop a method based on the premise that optimal state assignment corresponds to finding an optimal general decomposition of a finite state mechanism (FSM). They discuss the use of this approach for encoding state transition graphs extracted from logic-level descriptions. The notion of transition pairing is used to decompose a given FSM into several submachines such that the state assignment problem for the submachines is simpler than the original problem, attempting to avoid compromising the optimality of the solution. A novel decomposition algorithm that can decompose a FSM into an arbitrary number of submachines and a novel constraint satisfaction algorithm to encode the different submachines are given. Experimental results validate the use of decomposition-based techniques to solve the encoding problem.> James H. Kukula, Srini Devadas |
ICCAD | 2 |
| 1991 | Boolean Satisfiability and Equivalence Checking Using General Binary Decision DiagramsabstractIt is shown how general binary decision diagrams (BDDs), i.e., BDDs where input variables are allowed to appear multiple times along any path in the BDD, can be used to check for Boolean satisfiability. This satisfiability checking strategy is based on an input smoothing operation on general BDDs. Various input smoothing strategies for general BDDs are developed. In order to verify the equivalence of two functions f/sub 1/ and f/sub 2/, f/sub 1/(+)f/sub 2/ is checked for satisfiability. Using general BDDs different implementations of a 16*16 multiplier, a modified Achilles' heel function and a complex add-shift function were verified. It was not possible to construct OBDDs for any of the three functions.> Pranav Ashar, Abhijit Ghosh, Srini Devadas |
ICCD | 3 |
| 1991 | Design Verfication and Reachability Analysis Using Algebraic ManipulationabstractDesign verification is the process of checking that the specification of a circuit satisfies certain correctness properties. Approaches to design verification have involved the use of temporal logic and model checking, as well as the use of higher-order logic and theorem proving. Current approaches suffer from either limited expressivity of the logic, the state explosion problem, or difficulty in automating the verification process. The primary source of the complexity explosion in automata theoretic or temporal logic approaches is the state space explosion due to the need to construct the state space of the system under analysis. Symbolic analysis techniques are used based on linear algebra, specifically matrix multiplication, to compactly represent the state space of circuits described by a behavioral or register-transfer-level specification and thereby avoid this state space explosion, for classes of circuits.> Srini Devadas, Kurt Keutzer, A. S. Krishnakumar |
ICCD | 1 |
| 1991 | Gate-Delay-Fault Testability Properties of Multiplexor-Based NetworksabstractWe investigate the gate-delay-fault testability properties of multilevel, multiplexor-based logic circuits. Based on this investigation, we describe a procedure for synthesizing gate-delay-fault testable multilevel circuits. The procedure involves the construction of a multilevel circuit from a general, unordered Binary Decision Diagram (BDD) by replacing vertices of the BDD with multiplexors. The procedure relies on the following result derived in this article: If the multilevel circuit constructed from the BDD is initially fully single stuck-at fault testable, or made fully single stuck-at fault testable by redundancy removal, then it is completely robustly gate-delay-fault testable. Once the initial gate-delay-fault testable circuit has been obtained, constrained algebraic factorization is used to improve the area and performance characteristics without compromising testability. Unlike previous techniques for synthesizing robustly gate-delay-fault testable circuits, this procedure can be used to synthesize fully testable circuits directly from nonflattenable, logic-level implementations. Pranav Ashar, Srini Devadas, Kurt Keutzer |
ITC | 2 |
| 1991 | A Partial Enhanced-Scan Approach to Robust Delay-Fault Test Generation for Sequential CircuitsabstractThe authors address the problem of robust path-delay-fault test generation for sequential circuits by using a partial enhanced-scan/standard-scan approach and by using the notion of scan shifting. Vector pairs that can be obtained by single-bit shifts can be applied at speed under standard scan. An algorithm is given to determine an efficient ordering of the flip-flops in the scan chain using the information derived from running a delay test generator on the circuit. Given an ordering of the flip-flops, the authors give an optimization algorithm that attempts to minimize the number of flip-flops to be made enhanced-scan so as to obtain the required level of delay-fault coverage. Kwang-Ting Cheng, Srini Devadas, Kurt Keutzer |
ITC | 2 |
| 1991 | Recent progress in synthesis for testabilityabstractDescribes recent work involving the automatic synthesis of VLSI circuits with testability considerations. The first put of this paper explores the potential for logic synthesis to allow designers to more comprehensively test circuits while simultaneously diminishing the need for fault simulation and automatic test pattern generation. Logic optimization procedures can be used to produce circuits that are completely testable for single stuck-at faults. Testing for faults such as multiple stuck-at faults, gate delay faults and path delay faults is a greater challenge, but logic synthesis and optimization procedures can produce circuits that have high degrees of testability under these models as well. For each of these fault models test vectors can be produced as a by-product of the synthesis process and vector minimization algorithms can be used in the place of fault simulation to reduce the size of the test vector sets. The second part of the paper considers the difficult problem of synthesizing sequential circuits with high degrees of single stuck-at fault coverage without incurring the area and performance penalty of scan registers. Initial results at combining synthesis for testability approaches with register-transfer level automatic test-pattern generation to produce vector sets that give complete single stuck-at fault coverage without the use of scan.> Srini Devadas, Kurt Keutzer, Abhijit Ghosh |
VTS | 1 |
| 1991 | An automata-theoretic approach to behavioral equivalence
Srini Devadas, Kurt Keutzer |
Integr. | 1 |
| 1991 | Optimum and heuristic algorithms for an approach to finite state machine decompositionabstractOptimum and heuristic algorithms for the general decomposition of finite state machines (FSMs) such that the sum total of the number of product terms in the one-hot-coded and logic-minimized submachines is minimum or minimal are presented. This cost function is much more reflective of the area of an optimally state-assigned and minimized submachine than the number of states/edges in the submachine. The problem of optimum two-way FSM decomposition is formulated as one of symbolic output partitioning, and it is shown that this is an easier problem than optimum state assignment. A procedure of constrained prime implicant generation and covering that represents an optimum FSM decomposition algorithm, under the specified cost function, is described. It is shown that by means of this formulation, arbitrary decomposition topologies can be targeted by suitably modifying the constraints on the ability to encode during the covering. A novel iterative optimization strategy of symbolic implicant expansion and reduction, modified from two-level Boolean minimizers, that represents a heuristic algorithm based on the exact procedure is presented. Reduction and expansion are performed on functions with symbolic rather than binary-valued outputs. Preliminary experimental results that illustrate both the efficacy of the proposed algorithms and the validity of the selected cost function are presented.> Pranav Ashar, Srini Devadas, A. Richard Newton |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 2 |
| 1991 | Irredundant interacting sequential machines via optimal logic synthesisabstractThe authors develop optimal synthesis procedures for interacting nonscan sequential circuits composed of interacting finite state machines. For each of the different classes of redundancies, the authors define don't care sets, which if optimally exploited will result in the implicit elimination of any such redundancies in a given circuit. It is shown that notions of sequential don't cares and conditional compatibility are required to eliminate redundancies. Using a complex don't care set in an optimal sequential synthesis procedure of state minimization, state assignment, and combinational logic optimization results in fully testable single or interacting finite-state machines (FSMs). Preliminary experimental results indicate that irredundant sequential circuits can be synthesized with no area overhead and within reasonable CPU times with optimal logic synthesis.> Pranav Ashar, Srini Devadas, A. Richard Newton |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 2 |
| 1991 | Optimizing interacting finite state machines using sequential don't caresabstractApproaches are presented to multilevel sequential logic synthesis-algorithms and techniques for the area and performance optimizations of interconnected finite state machine descriptions. Techniques are presented for the exploitation of sequential don't cares in arbitrary, interconnected sequential machine structures. Exploiting these don't care sequences can results in significant improvements in area and performance. The problem of moving logic across state machine boundaries so as to make particular machines less complex at the possible expense of making others more complex is addressed. Optimization algorithms that incrementally modify state machine structures across latch boundaries are also presented. The use of more global state machine decomposition and factorization algorithms for area optimization is described, and experimental results using these algorithms on sequential circuits are presented.> Srini Devadas |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 1 |
| 1991 | A unified approach to the synthesis of fully testable sequential machinesabstractAn attempt is made to unify and extend the various approaches to synthesizing fully testable sequential circuits that can be modeled as finite state machines (FSMs). The authors first identify classes of redundancies and isolate equivalent-state redundancies as those most difficult to eliminate. It is then shown that the essential problem behind equivalent-state redundancies is the creation of valid/invalid state pairs. The remainder of this research is devoted to techniques for developing differentiating sequences for valid/invalid state pairs created by a fault, as well as to techniques for retaining these sequences in the presence of that fault. A variety of techniques have been proposed to address this problem. At one end of the spectrum there are optimal synthesis procedures that ensure full testability by eliminating redundancies via the use of appropriate don't care sets. At the other end of the spectrum there are constrained synthesis procedures that produce fully and easily testable sequential circuits by restricting the implementation of the logic. The notion of fault-effect disjointness is used to explore the landscape between these two extremes and a spectrum of methods that place relatively more-or-less emphasis on either logic optimization or constrained synthesis is demonstrated. Techniques used in this exploration include fault simulation, Boolean covering, algebraic factorization, and state assignment. Experimental results using the proposed synthesis procedures and comparisons to previous approaches are presented.> Srini Devadas, Kurt Keutzer |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 1 |
| 1991 | Exact algorithms for output encoding, state assignment, and four-level Boolean minimizationabstractA novel minimization procedure of prime implicant generation and covering that operates on symbolic outputs, rather than binary-valued outputs, is proposed for solving the output encoding problem. An exact solution to this minimization problem is also an exact solution to the encoding problem. While this covering problem is more complex than the classic unate covering problem, a single logic minimization step replaces O(N-factorial) minimizations. The input encoding problem can be exactly solved using multiple-valued Boolean minimization. An exact algorithm is presented for state assignment by generalizing the proposed output encoding approach to the multiple-valued input case. Four-level Boolean minimization entails finding a cascaded pair of two-level logic functions that implement another logic function, such that the sum of the product terms in the two cascaded functions or truth tables is minimum. Four-level Boolean minimization can be formulated as an encoding problem and solved exactly using the proposed algorithms. Preliminary experimental results are presented which indicate that this approach is significantly more efficient than exhaustive search. Computationally efficient heuristic approaches based on the exact algorithms are proposed for output encoding, state assignment, and four-level Boolean minimization.> Srini Devadas, A. Richard Newton |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 1 |
| 1991 | Test generation and verification for highly sequential circuitsabstractA novel test procedure that exploits the structure of the combinational logic in the circuit as well as the sequential behavior of the circuit is presented. Initially, before test generation, separate sum-of-product representations of the complete or partial ON-sets and OFF-sets of each of the flip-flop inputs and primary outputs of the sequential circuit are extracted using the PODEM algorithm. Fast algorithms for state justification and state differentiation based on this representation are described. The algorithm developed for test generation is extended to verification of finite-state machines (FSMs). The algorithm for state differentiation based on the ON- and OFF-set representation is modified for verification purposes. The authors present experimental results that illustrate the superior performance of this approach as compared to previous approaches to FSM verification. They are able to verify examples with significantly more memory elements than previous approaches.> Abhijit Ghosh, Srini Devadas, A. Richard Newton |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 2 |
| 1990 | A Unified Approach to the Decomposition and Re-Decomposition of Sequential MachinesabstractWe present a unified framework and associated algorithms for the optimal decomposition and re-decomposition of sequential machines. This framework allows for a uniform treatment of arbitrary decomposition topologies operating at the State Transition Graph (STG) level, while targeting a cost function that is close to the eventual logic implementation. Previous work has targeted specific decomposition topologies via the formulation of decomposition as implicant covering with associated constraints. It is shown that this formulation can be used to target arbitrary desired topologies merely by customizing the constraints during implicant covering. It is shown how this work relates to preserved partitions and covers traditionally used in parallel and cascade decomposition, and how this formulation establishes the relationship between state assignment and FSM decomposition.In many cases, an initial decomposition is specified as a starting point. Attempting to flatten a set of interacting circuits into a single lumped STG in order to modify the decomposition structure could require astronomical amounts of CPU time and memory. Memory and CPU time efficient re-decomposition algorithms that operate on distributed-style specifications and which are more global than those presented in the past have been developed. These algorithms have been implemented in the sequential logic synthesis system, FLAMES, that is being developed at UCB/MIT. Pranav Ashar, Srini Devadas, A. Richard Newton |
DAC | 2 |
| 1990 | Synthesis and Optimization Procedures for Robustly Delay-Fault Testable Combinational Logic CircuitsabstractIn this paper we apply recently developed necessary and sufficient conditions for robust path-delay-fault testability to develop synthesis procedures which produce two-level and multilevel circuits with high degrees of robust path delay fault testability. For circuits which can be flattened to two levels, we give a covering procedure which optimizes for robust path delay fault testability. These two-level circuits can then be algebraically factored to produce robustly path-delay-fault testable multilevel circuits. For regular structures which cannot be flattened to two levels, we give a composition procedure which allows for the construction of robustly path-delay-fault testable regular structures. Finally, we show how these two techniques can be combined to produce cascaded combinational logic blocks that are robustly path-delay-fault testable. We demonstrate these techniques on a variety of examples. It is possible to produce entire chips that are fully path delay testable using these techniques. Srini Devadas, Kurt Keutzer |
DAC | 1 |
| 1990 | Verification of Interacting Sequential CircuitsabstractThe problem of verifying the equivalence of interacting finite state machines (FSMs) described at the logic level is addressed. The problem is formulated as that of checking for the equivalence of the reset/starting states of the two FSMs. First, separate sum-of-product representations of the ON-sets and OFF-sets of each of the flip-flop inputs and primary outputs of the sequential circuit, are extracted using the PODEM algorithm. We describe a fast algorithm for state differentiation based on this representation. The input as well as the state space is implicitly enumerated through a process of repeated cube intersections to generate the State Transition Graph (STG).In contrast to previous approaches, this algorithm can be efficiently generalized for verifying distributed-style specifications of interacting sequential circuits, exploiting the nature of the interconnection topology. Pipeline latches in a distributed-style specification typically do not add complexity to the sequential behavior of a circuit, but greatly add to the complexity of traditional approaches to verifying sequential circuits. Pipeline latches are easily incorporated into our generalized, hierarchical verification strategy whereby the states of pipeline latches can be implicitly enumerated.Experimental results indicate the superior efficiency of this approach as compared to previous approaches for FSM verification. It is possible to verify examples with more than 1050 states. Abhijit Ghosh, Srini Devadas, A. Richard Newton |
DAC | 2 |
| 1990 | Sequential Test Generation at the Register-Transfer and Logic LevelsabstractThe problem of test generation for non-scan sequential VLSI circuits is addressed. A novel method of test generation that efficiently generates test sequences for stuck-at faults in the logic circuit by exploiting register-transfer-level (RTL) design information is presented. Our approach is targeted at chips with data-path like STG. Abhijit Ghosh, Srini Devadas, A. Richard Newton |
DAC | 2 |
| 1990 | Implicit State Transition Graphs: Applications to Sequential Logic Synthesis and TestabstractImplicit state enumeration is used in developing strategies to solve key problems in sequential logic synthesis and test. It is shown that it is possible to extract implicit state transition graphs (ISTGs) from logic-gate and flip-flop descriptions of sequential circuits that allow equivalent states to be represented by cubes, and edges from different states to be coalesced into one, thereby decreasing significantly the CPU time and memory requirements of the extraction process. Coupled with the enumeration technique, synthesis strategies are proposed for FSMs (finite state machines) described at the logic level. As is illustrated, these synthesis strategies allow the authors to optimize large FSMs. The authors apply an ISTG traversal algorithm for verifying equivalence and detecting redundancies in logic-level sequential circuits. This algorithm is more efficient than previously developed sequential test generation algorithms when used to detect equivalent-state redundancies present in some classes of circuits.> Pranav Ashar, Abhijit Ghosh, Srini Devadas, A. Richard Newton |
ICCAD | 3 |
| 1990 | Testability-Preserving Circuit TransformationsabstractConsideration is given to the synthesis of robustly path-delay-fault testable circuits and it is shown that a single property, ENF reducibility, unifies previous results on robust delay fault testability and multifault testability and proves new ones. The notion of ENF reducibility is used to show that a constrained version of a common area improving transformation, namely, algebraic resubstitution with complement, retains robust path-delay-fault testability. Thus, a more efficient means of synthesizing fully robustly path-delay-fault testable networks is given. The same property of ENF reducibility is used to show that constrained algebraic resubstitution with complement retains multifault irredundancy. Necessary and sufficient conditions are presented for transistor stuck-open fault testability in arbitrary, multilevel networks. It is shown that algebraic factorization, including the constrained use of the complement, can be used to synthesize fully stuck-open fault testable multilevel networks.> Michael J. Bryan, Srini Devadas, Kurt Keutzer |
ICCAD | 2 |
| 1990 | An Automata-Theoretic Approach to Behavioral EquivalenceabstractThe problem of verifying the equivalence of a behavioral description against a logic-level implementation is addressed. One major hindrance toward a precise notion of behavioral verification has been that parallel, serial or pipelined implementations of the same behavioral description can be implemented in finite-state automata with different input/output behaviors. The authors use nondeterminism to model the degree of freedom that is afforded by parallelism in a behavioral description that also contains complex control. Given some assumptions, they show how the set of finite automata derivable from a behavioral description can be represented compactly as an input-programmed automaton (p-Automaton), i.e., an automaton with programmed meta-input variables. The logic-level implementation is deemed to be equivalent to the behavioral description if and only if the p-Automaton is equivalent to the logic-level finite automaton under some assignment to the meta-input variables. The method allows for extending the use of finite-state automata equivalence-checking algorithms to the problem of behavioral verification.> Srini Devadas, Kurt Keutzer |
ICCAD | 1 |
| 1990 | Testability driven synthesis of interacting finite state machinesabstractSequential testability aspects in the decomposition of finite state machines (FSMs) are addressed. It is shown that the sequential testability of an FSM can be enhanced more easily when the machine is recognized to be, or is synthesized as, an interconnection of smaller machines. An exhaustive classification of redundant faults that can occur in a single FSM embedded in an interacting sequential circuit is presented. Associating each class of these redundant faults with a don't care set, a synthesis procedure is described that exploits the don't cares optimally to obtain an irredundant interacting sequential circuit with no area overhead. The synthesis procedure operates on a distributed-style representation of interacting state transition graphs (STGs), carrying out a series of local analyses. Insights into sequential logic synthesis improving on current optimization techniques for interacting sequential circuits are presented.> Pranav Ashar, Srini Devadas, A. Richard Newton |
ICCD | 2 |
| 1990 | Heuristic minimization of Boolean relations using testing techniquesabstractMinimization of Boolean relations is important from the point of view of synthesis, especially in synthesis for testability. A very fast heuristic procedure for finding an optimal sum-of-products representation for a Boolean relation is described. Starting with a function compatible with the relation, a process of iterative logic improvement based on test generation techniques is used to derive a minimal function compatible with the Boolean relation.> Abhijit Ghosh, Srini Devadas, A. Richard Newton |
ICCD | 2 |
| 1990 | Design of integrated circuits fully testable for delay-faults and multifaultsabstractIt is shown how a sophisticated orchestration of combinational synthesis-for-testability approaches can result in logic-level implementations of large integrated-circuit designs that are completely robustly path-delay fault and multifault testable. For control portions of VLSI circuits, synthesis procedures that guarantee path-delay-fault or multifault testability, starting from a sum-of-products representation of a function, are used. Hierarchical composition rules are used in the synthesis of regular structures occurring in data path portions such as parity generators and arithmetic units. It is shown how test vectors for detecting all path-delay faults and multifaults can be obtained as a by-product of the synthesis process. These techniques were successfully used on circuits with over 5000 gates. Preliminary experimental results on a data encryption chip, a small microprocessor, and a speech recognition chip are presented.> Srini Devadas, Kurt Keutzer |
ITC | 1 |
| 1990 | Sequential logic synthesis for testability using register-transfer level descriptionsabstractA synthesis-for-testability approach that uses a register-transfer level (RTL) specification of a sequential circuit to derive a fully testable implementation of the circuit is presented. Emphasis is placed on the development of a synthesis strategy of don t care exploitation and logic partitioning that results in a fully testable implementation of the sequential machine. Preliminary experimental results indicate that large sequential circuits (e.g., finite-state-machine controllers, data paths) with a large number of latches and gates can be synthesized to be fully nonscan testable by use of these techniques.> Abhijit Ghosh, Srini Devadas, A. Richard Newton |
ITC | 2 |
| 1990 | Redundancies and don't cares in sequential logic synthesis
Srini Devadas, Hi-Keung Tony Ma, A. Richard Newton |
J. Electron. Test. | 1 |
| 1990 | Easily testable PLA-based finite state machinesabstractAn outline is presented of a synthesis procedure that, beginning from a state transition graph (STG) description of a sequential machine, produces an optimized easily testable programmable logic array (PLA) based logic implementation. Previous approaches to synthesizing easily testable sequential machines have concentrated on the stuck-at-fault model; for PLAs, an extended fault model called the crosspoint fault model has been used. The authors propose a procedure of constrained state assignment and logic optimization which guarantees testability for all combinationally irredundant crosspoint faults in a PLA-based finite-state machine. No direct access to the flip-flops is required. The test sequences to detect these faults can be obtained using combinational test generation techniques alone. This procedure thus represents an alternative to a scan design methodology. Results are presented which show that the area/performance penalties in return for easy testability are small.> Srini Devadas, Hi-Keung Tony Ma |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 1 |
| 1990 | Irredundant sequential machines via optimal logic synthesisabstractIt is shown that optimal sequential logic synthesis can produce irredundant, fully testable finite-state machines. Synthesizing a sequential circuit from a state transition graph description involves the steps of state minimization, state assignment, and logic optimization. Previous approaches to producing fully and easily testable sequential circuits have involved the use of extra logic and constraints on state assignments and logic optimization. Here it is shown that 100% testability can be ensured without the addition of extra logic and without constraints on the state assignment and logic optimization. Unlike previous synthesis approaches to ensuring fully testable machines, there is no area/performance penalty associated with this approach. This technique can be used in conjunction with previous approaches to ensure that the synthesized machine is easily testable. Given a state-transition-graph specification, a logic-level automaton that is fully testable for all single stuck-at faults in the combinational logic without access to the memory elements is synthesized.> Srini Devadas, Hi-Keung Tony Ma, A. Richard Newton, Alberto L. Sangiovanni-Vincentelli |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 1 |
| 1989 | Approaches to Multi-level Sequential Logic SynthesisabstractIn this paper, we present approaches to multi-level sequential logic synthesis — algorithms and techniques for the area and performance optimization of interconnected finite state machine descriptions. Srini Devadas |
DAC | 1 |
| 1989 | General Decomposition of Sequential Machines: Relationships to State AssignmentabstractIn this paper, we present new techniques for state assignment of finite state machines based on state machine decomposition algorithms. Srini Devadas |
DAC | 1 |
| 1989 | Optimum and heuristic algorithms for finite state machine decomposition and partitioningabstractThe authors formulate the problem of optimum two-way finite-sole-machine (FSM) decomposition as one of symbolic-output partitioning and show that this is an easier problem than optimum state assignment. They describe a procedure of constrained prime-implicant generation and covering that represents an optimum FSM decomposition algorithm under the specified cost function. Exact procedures are not viable for large problem instances. The authors give a novel iterative optimization strategy of symbolic-implicant expansion and reduction, modified from two-level Boolean minimizers, that represents a heuristic algorithm based on their exact procedure. Reduction and expansion are performed on functions with symbolic, rather than binary-valued, outputs. Preliminary experimental results that illustrate both the efficacy of the proposed algorithms and the validity of the selected cost function.> Pranav Ashar, Srini Devadas, A. Richard Newton |
ICCAD | 2 |
| 1989 | Optimal layout via Boolean satisfiabilityabstractThe author transforms various NP-complete problems in layout, namely, two- and multilayer dogleg channel routing, two-way partitioning, one-dimensional and two-dimensional placement, into Boolean satisfiability problems. The transformations are efficient in that the number of inputs to the Boolean function, for which he has to find a satisfying assignment, only grows linearly or quasilinearly with the layout problem size. These transformations also produce a minimal-size Boolean function in order to speed up satisfiability check performance.> Srini Devadas |
ICCAD | 1 |
| 1989 | Boolean minimization and algebraic factorization procedures for fully testable sequential machinesabstractThe authors present a novel Boolean minimization procedure of prime-implicant generation and constrained covering based on the Quine-McCluskey algorithm. On completion, it guarantees a prime and irredundant, fully testable Moore or Mealy finite state machine. Given a two-level circuit with these properties, constrained algebraic factorization techniques are used that retain the invariant that no single fault can both produce an invalid state and corrupt the distinguishing sequence by which that invalid state is detected. Besides offering a more detailed understanding of the sources of untestability in sequential circuits than previous approaches, this approach offers significant practical advantages as well. It is applicable to a wider range of circuits than optimal synthesis procedures whose utility is often limited by prohibitively high CPU requirements, and its less restrictive synthesis constraints result in lower area overhead than other constrained synthesis approaches. These observations are supported by experimental results.> Srini Devadas, Kurt Keutzer |
ICCAD | 1 |
| 1989 | Test generation for highly sequential circuitsabstractThe authors address the problem of generating test sequences for stuck-at faults in nonscan synchronous sequential circuits. They present a novel test procedure that exploits both the structure of the combinational logic in the circuit as well as the sequential behavior of the circuit. In contrast to previous approaches, the authors decompose the problem of sequential test generation into three subproblems of combinational test generation, fault-free state justification, and fault-free state differentiation. They describe fast algorithms for state justification and state differentiation using the ON sets and OFF sets of flip-flop inputs and primary outputs. The decomposition of the testing problem into three subproblems rather than the traditional two, performing the justification and differentiation steps on the fault-free rather than the faulty machine, and the use of efficient techniques for cube intersection result in significant performance improvements over previous approaches.> Abhijit Ghosh, Srini Devadas, A. Richard Newton |
ICCAD | 2 |
| 1989 | Delay Test Generation for Synchronous Sequential CircuitsabstractThe author presents a method for generating test sequences to detect delay faults in sequential circuits using the stuck-at-fault sequential test generator STALLION. The method is complete in that it will generate a delay test sequence for a targeted fault given sufficient CPU time, if such a sequence exists. Faults for which no delay test sequence exists are termed sequentially delay redundant. The author describes means of eliminating sequential delay redundancies in logic circuits. He presents a partial-scan methodology for enhancing the testability of difficult-to-test or untestable sequential circuits, wherein a small number of flip-flops are selected and made controllable/observable. The selection process guarantees the elimination of all sequential delay redundancies. It is shown that an intimate relationship exists between state assignment and delay testability of a sequential machine. A state assignment algorithm for the synthesis of sequential machines with maximal delay fault testability is described. Preliminary experimental results using the test generation, partial-scan, and synthesis algorithms are presented.> Srini Devadas |
ITC | 1 |
| 1989 | Redundancies and Don't Cares in Sequential Logic SynthesisabstractThe authors explore the relationships between redundant logic and don't care conditions in sequential circuits. Stuck-at faults in a sequential circuit may be testable in the combinational sense but may be redundant because they do not alter the terminal behavior of a nonscan sequential machine. These sequential redundancies result in a faulty state transition graph (STG) that is equivalent to the STG of the true machine. The authors present a classification of redundant faults in sequential circuits composed of single or interacting finite-state machines. Don't care sets can be defined for each class of redundancy, and optimally exploiting these don't care conditions results in the implicit elimination of any such redundancies in a given circuit. In cascaded and interconnected sequential circuits, sequential don't cares are required to eliminate redundancies. The authors present preliminary experimental results which indicate that by exploiting these don't cares medium-sized irredundant sequential circuits can be synthesized with no area overhead and within reasonable CPU times.> Srini Devadas, Hi-Keung Tony Ma, A. Richard Newton |
ITC | 1 |
| 1989 | A synthesis and optimization procedure for fully and easily testable sequential machinesabstractThe authors outline a synthesis procedure which beginning from a state transition graph (STG) description of a sequential machine produces an optimized fully and easily testable logic implementation. This logic-level implementation is guaranteed to be testable for all single stuck-at faults in the combinational logic and the test sequences for these faults can be obtained using combinational test generation techniques alone. The sequential machine is assumed to have a reset state and be R-reachable. All single stuck-at faults in the combinational logic and the input and output stuck-at faults of the memory elements in the synthesized logic-level automaton can be tested without access to the memory elements using these test sequences. Thus this procedure represents an alternative to a scan design methodology. The area penalty incurred due to the constraints on the optimization are small. The performance of the synthesized design is usually better than that of an unconstrained design optimized for area alone. The authors show that an intimate relationship exists between state assignment and the testability of a sequential machine. They propose a procedure of constrained state assignment and logic optimization which guarantees testability for both Moore and Mealy machines.> Srini Devadas, Hi-Keung Tony Ma, A. Richard Newton, Alberto L. Sangiovanni-Vincentelli |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 1 |
| 1989 | Algorithms for hardware allocation in data path synthesisabstractNovel algorithms for the simultaneous cost/resource-constrained allocation of registers, arithmetic units, and interconnect in a data path have been developed. The entire allocation process can be formulated as a two-dimensional placement problem of microinstructions in space and time. This formulation readily lends itself to the use of a variety of heuristics for solving the allocation problem. The authors present simulated-annealing-based algorithms which provide excellent solutions to this formulation of the allocation problem. These algorithms operate under a variety of user-specifiable constraints on hardware resources and costs. They also incorporate conditional resource sharing and simultaneously address all aspects of the allocation problem, namely register, arithmetic unit, and interconnect allocation, while effectively exploring the existing tradeoffs in the design space.> Srini Devadas, A. Richard Newton |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 1 |
| 1989 | Decomposition and factorization of sequential finite state machinesabstractAlgorithms are proposed for decomposing a finite-state machine into smaller interacting machines so as to optimize area and performance of the eventual logic implementation. Cascade decomposition algorithms, which decompose a given machine into independent and dependent components, have been proposed in the past. The authors propose a more powerful form of decomposition where both components of the decomposed machine interact with each other. Experimental results indicate that this decomposition technique for state machine decomposition is superior to cascade decomposition techniques. It is the premise of this study that optimal state assignment corresponds to finding an optimal multiple general decomposition of a finite-state machine. State assignment techniques that target two-level and multilevel implementations based on state machine factorization algorithms followed by state assignment algorithms are presented. It is rigorously proved that one-hot encoding a nontrivially factored machine is guaranteed to produce a better result than one-hot encoding the original machine for the two-level case.> Srini Devadas, A. Richard Newton |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 1 |
| 1989 | Logic verification algorithms and their parallel implementationabstractLOgic VERification (LOVER) incorporates a novel approach to combinational logic verification and obtains excellent results when compared to existing techniques. The authors describe a new verification algorithm, LOVER-PODEM, whose enumeration phase is based on PODEM. A variant of LOVER-PODEM, called PLOVER, is presented. Parallel logic verification schemes have been developed for the first time. Issues in efficiently parallelizing both general and specific LOVER-based approaches to logic verification over a large number of processors are addressed. The parallelism inherent in the LOVER framework regardless of what enumeration and simulation algorithms are used is discussed. Since the enumeration phase is the efficiency bottleneck in parallelizing LOVER-based approaches, parallel versions of PODEM-based enumeration algorithms have been developed.> Hi-Keung Tony Ma, Srini Devadas, Ruey-Sing Wei, Alberto L. Sangiovanni-Vincentelli |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 2 |
| 1988 | Decomposition and factorization of sequential finite state machinesabstractAlgorithms for decomposing a finite-state machine into smaller interacting machines so as to optimize area and performance of the eventual logic implementation are presented. Cascade decomposition algorithms, which decompose a given machine into an independent and dependent component, have been proposed in the past. However, good cascade decompositions rarely exist in finite-state machine designs. A more powerful form of decomposition whereby both components of the decomposed machine interact with each other is proposed. This form of decomposition involves identifying subroutines or factors in the original machine, extracting these factors, and representing them as a separate factoring machine. The occurrences of these factors become calls to the factoring machine from the factored machine. Given a state-transition-graph description of a machine, algorithms which can identify factors in the machine that produce good decompositions have been developed. Experimental results indicate that this factoring technique is superior to cascade decomposition techniques.> Srini Devadas, A. Richard Newton |
ICCAD | 1 |
| 1988 | Boolean decomposition in multi-level logic optimizationabstractMultiple-valued Boolean minimization is proposed as a technique for identifying and extracting good Boolean factors which can be used as strong divisors to minimize the literal count and the area of a multilevel logic network. Given a two-level logic function, a subset of inputs to the function is selected such that the number of good Boolean factors contained in this subset of inputs is large. If the targeted implementation is a set of interconnected PLAs, the different cube combinations given by the subset of inputs are re-encoded to reduce the number of product terms in the logic function. A novel algorithm for the re-encoding is given that is based on the notion of partial satisfaction of constraints. Algorithms have been developed that identify a set of factors which maximally decrease the literal count of the logic network when they are used as strong divisors. Results obtained on several benchmark examples that illustrate the efficacy of the techniques are presented.> Srini Devadas, Albert R. Wang, A. Richard Newton, Alberto L. Sangiovanni-Vincentelli |
ICCAD | 1 |
| 1988 | Synthesis and Optimization Procedures for Fully and Easily Testable Sequential MachinesabstractA synthesis procedure is described that produces an optimized fully and easily testable logic implementation of a sequential machine from a state transition graph description of the machine. This logic-level implementation is guaranteed to be testable for all single stuck-at faults in the combinational logic. No access to the memory elements is required. The test sequences for these faults can be obtained using combinational test generation techniques alone. It is shown that an intimate relationship exists between state assignment and the testability of a sequential machine. A technique is also presented of don't-care minimization and added observability which ensures fully testable machines.> Srini Devadas, Hi-Keung Tony Ma, A. Richard Newton, Alberto L. Sangiovanni-Vincentelli |
ITC | 1 |
| 1988 | An Incomplete Scan Design Approach to Test Generation for Sequential MachinesabstractAn incomplete scan design approach to sequential test generation is presented. This approach represents a significant departure from previous methods. First, using an efficient sequential testing algorithm, test sequences are generated for a large number of possible faults in the given sequential circuit. A minimal subset of memory elements is then found, which if made observable and controllable will result in easy detection of the sequentially redundant and irredundant but difficult-to-defect faults. The deterministic test generation algorithm is again used to generate tests for these faults in the modified circuit (the circuit with the identified memory elements made scannable). Detection of all irredundant faults can be guaranteed as in the complete scan design case, but at significantly less area and performance cost.> Hi-Keung Tony Ma, A. Richard Newton, Srini Devadas, Alberto L. Sangiovanni-Vincentelli |
ITC | 3 |
| 1988 | Techniques for multilayer channel routingabstractThe techniques described have been implemented in a multilayer channel router called Chameleon. Chameleon consists of two stages: a partitioner and a detailed router. The partitioner divides the problems into two-layer and three-layer subproblems such that global channel area is minimized. The detailed router then implements the connections using generalizations of the algorithms used in YACR2 (see ibid., vol.CAD-4, no.3, p.208-19, 1985). In particular, a three-dimensional maze router is used for the vertical connections; this methodology is effective even when cycle constraints are present. Chameleon has produced optimal results on a wide range of industrial and academic examples for a variety of layer and pitch combinations, and can handle a variety of technology constraints.> Douglas Braun, Jeffrey L. Burns, Fabio Romeo, Alberto L. Sangiovanni-Vincentelli, Kartikeya Mayaram, Srini Devadas, Hi-Keung Tony Ma |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 6 |
| 1988 | On the verification of sequential machines at differing levels of abstractionabstractAn algorithm is presented for the verification of the equivalence of two sequential circuit descriptions at the same of differing levels of abstraction, namely, at the register-transfer (RT) level and the logic level. The descriptions represent general finite automata at the differing levels. A finite automaton can be described in ISP-like language and its equivalence to a logic level implementation can be verified using this algorithm. Two logic-level automata can be similarly verified for equivalence. The technique is shown to be computationally efficient for complex circuits. The efficiency of the algorithm lies in the exploitation of don't care information derivable from the RT or logic-level description during the verification process. Using efficient cube enumeration procedures at the logic level, the equivalence of finite automata with a large number of states in small amounts of CPU time was verified. A two-phase enumeration-simulation algorithm for verifying the equivalence of two logic-level finite automata with the same or differing number of latches is also presented.> Srini Devadas, Hi-Keung Tony Ma, A. Richard Newton |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 1 |
| 1988 | MUSTANG: state assignment of finite state machines targeting multilevel logic implementationsabstractThe problem of state assignment for synchronous finite-state machines (FSM), targeted towards multilevel combinational logic and feedback register implementations, are addressed. The authors present state-assignment algorithms that heuristically maximize the number of common cubes in the encoded network to maximize the number of literals in the resulting combinational logic network after multilevel logic optimization. Results over a wide range of benchmarks which prove the efficacy of the proposed techniques are presented. Literal counts averaging 20%-40% less than other state-assignment programs have been obtained.> Srini Devadas, Hi-Keung Tony Ma, A. Richard Newton, Alberto L. Sangiovanni-Vincentelli |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 1 |
| 1988 | Test generation for sequential circuitsabstractAn approach to test-pattern generation for synchronous sequential circuits is presented. The deterministic sequential test-generation algorithm, based on extensions to the PODEM justification algorithm, is effective for midsized sequential circuits and can be used in conjunction with an incomplete scan design approach to generate tests for very large sequential circuits. Tests for finite-state machines with a large number of states have been successfully generated using reasonable amounts of CPU time and close-to-maximum possible fault coverages have been obtained. For very large sequential circuits, an incomplete scan-design approach to test generation has been developed. The deterministic test generation algorithm is again used to generate test for faults in the modified circuit. All irredundant faults can be detected as in the complete scan design case, but at significantly less area and performance cost. The length of the test sequences for the faults can be bounded by a prescribed value-in general, a tradeoff exists between the number of memory elements required to be made scannable and the maximum allowed length of the test sequence.> Hi-Keung Tony Ma, Srini Devadas, A. Richard Newton, Alberto L. Sangiovanni-Vincentelli |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 2 |
| 1987 | On the Verification of Sequential Machines at Differing Levels of AbstractionabstractIn this paper, an algorithm is presented for the verification of the equivalence of two sequential circuit descriptions at the same or differing levels of abstraction, namely at the register-transfer (RT) level and the logic level. The descriptions represent general finite automata at the differing levels - a finite automaton can be described in a ISP-like language and its equivalence to a logic level implementation can be verified using our algorithm. Two logic level automatons can be similarly verified for equivalence. Previous approaches to sequential circuit verification have been restricted to verifying relatively simple descriptions with small amounts of memory. Unlike these approaches, our technique is shown to be computationally efficient for much more complex circuits. The efficiency of our algorithm lies in the exploitation of don't care information derivable from the RTL or logic level description (e.g. invalid input and output sequences) during the verification process. Using efficient cube enumeration procedures at the logic level we have been able to verify the equivalence of finite automata with a large number of states in small amounts of CPU-time. Srini Devadas, Hi-Keung Tony Ma, A. Richard Newton |
DAC | 1 |
| 1987 | Logic Verification Algorithms and Their Parallel ImplementationabstractLOVER incorporates a novel approach to combinational logic verification and obtains good results when compared to existing techniques. In this paper we describe a new verification algorithm, LOVER-PODEM, whose enumeration phase is based on PODEM. A variant of LOVER-PODEM, called PLOVER, is presented. We have developed, for the first time, parallel logic verification schemes. Issues in efficiently parallelizing both general and specific LOVER-based approaches to logic verification over a large number of processors are addressed. We discuss parallelism inherent in the LOVER framework regardless of what enumeration and simulation algorithms are used. Since the enumeration phase is the efficiency bottleneck in parallelizing LOVER-based approaches, we have developed parallel versions of PODEM-based enumeration algorithms. Experimental results are presented to show that high processor utilization can be achieved when these parallelisms are exploited. Speed-up factors of over 7.8 have been achieved with 8 processor configurations. Hi-Keung Tony Ma, Srini Devadas, Alberto L. Sangiovanni-Vincentelli, Ruey-Sing Wei |
DAC | 2 |
| 1987 | Topological Optimization of Multiple-Level Array LogicabstractA generalized topological optimization tool for array-based layout styles is presented. This tool can be used for automated layout synthesis of logic networks in a variety of technologies and design styles, including static CMOS, static NMOS and dynamic MOS domino structures. Results obtained compare favorably with technology and design-style-specific synthesis systems. The topological optimization tool is a generalized array optimizer which can be used for the multiple constrained folding of programmable logic array, gate matrix, Weinberger array, multilevel matrix, and storage/logic array structures. The optimizer uses simulated-annealing-based algorithms and performs as well as or better than existing specialized PLA folding programs and gate matrix folders. The different layout style alternatives allow area-efficient synthesis of logic circuits in various technologies. Layout for sequential logic in the form of storage/logic arrays has been automated for the first time. A multiprocessor implementation of the simulated-annealing-based algorithms for generalized array optimization has been developed on the Sequent Balance 8000 multiprocessor. Dynamic windowing and dynamic partitioning techniques have resulted in an efficient parallel implementation of simulated annealing. Srini Devadas, A. Richard Newton |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 1 |
| 1986 | Chameleon: a new multi-layer channel routerabstractNew techniques for routing general multi-layer channels are introduced. These techniques can handle a variety of technology constraints. For example, linewidth and line-to-line spacing can be specified independently for each layer, and contact stacking can be allowed or forbidden. These techniques have been implemented in a new multi-layer channel router called Chameleon. Chameleon consists of two stages: a partitioner and a detailed router. The partitioner divides the problem into two and three-layer subproblems such that global channel area is minimized. The detailed router then implements the connections using generalizations of the algorithms used in YACR2. In particular a three-dimensional maze router is used which guarantees that any problem can be routed even when cyclic constraints are present. Chameleon produces optimal results on a wide range of industrial and academic examples for any number of layers and pitch combinations. Douglas Braun, Jeffrey L. Burns, Srini Devadas, Hi-Keung Tony Ma, Kartikeya Mayaram, Fabio Romeo, Alberto L. Sangiovanni-Vincentelli |
DAC | 3 |
| 1986 | GENIE: a generalized array optimizer for VLSI synthesisabstractA new generalized array optimization scheme is presented which solves the problem of efficient automatic layout of multi-level CMOS and NMOS logic circuits. The new approach has been implemented in the program GENIE which can be used for the multiple folding of PLAS, as well as for compacting gate matrix layouts, SLAs, and Weinberger arrays. The cells in the array can be of non-uniform sizes and any form of constraint can be placed on the input and output terminals. The generalized array optimizer uses the combinatorial optimization technique called Simulated Annealing. Results obtained are uniformly better than existing specialized array optimizers and folding programs, particularly when the inputs locations are constrained. GENIE is the first program to produce high-quality, automated SLA implementations. Srini Devadas, A. Richard Newton |
DAC | 1 |