EDBT 2026 Demo / reviewers in the wild / expert
Prabhat Mishra 0001
dblp:m/PrabhatMishra
· DBLP profile ↗
136ranked-venue papers
10as first author
44since 2021 · last 2026
0000-0003-3653-6221ORCID · verified
Domains — the database's venue-derived domains; a paper can count in several
Systems, architecture and hardware · 129 · 10 first-author · 39 since 2021Software engineering, systems software and programming languages · 27 · 3 first-author · 8 since 2021Security and privacy · 4 · 2 since 2021Applied, interdisciplinary, general and emerging computing · 3 · 2 since 2021Theory of computation · 1 · 1 since 2021
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2026 | TroLL: Exploiting Structural Similarities Between Logic Locking and Hardware TrojansabstractLogic locking and hardware Trojans are two fields in hardware security that have been mostly developed independently from each other. In this paper, we identify the relationship between these two fields. We find that a common structure that exists in many logic locking techniques has desirable properties of hardware Trojans (HWT). We then construct a novel type of HWT, called Trojans based on Logic Locking (TroLL), in a way that can evade state-of-the-art ATPG-based HWT detection techniques. In an effort to detect TroLL, we propose customization of existing state-of-the-art ATPG-based HWT detection approaches as well as adapting the SAT-based attacks on logic locking to HWT detection. In our experiments, we use random sampling as reference. It is shown that the customized ATPG-based approaches are the best performing but only offer limited improvement over random sampling. Moreover, their efficacy also diminishes as TroLL’s triggers become longer (i. e. have more bits specified). We thereby highlight the need to find a scalable HWT detection approach for TroLL. Yuntao Liu 0001, Aruna Jayasena, Prabhat Mishra 0001, Ankur Srivastava 0001 |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 3 |
| 2025 | Security Assertions for Trusted Execution EnvironmentsabstractTrusted Execution Environment (TEE) provides a secure and isolated execution environment for sensitive applications. In order to design secure and trustworthy TEE-based systems, it is crucial to verify the trustworthiness of TEE implementations. Property checking is a promising avenue to guarantee that the TEE implementation satisfies the security properties. In the presence of a vulnerability, property checking will fail and provide a counterexample that can be utilized to fix the vulnerability. A major challenge in TEE property checking is that it relies on manual definition of the security properties, which can be cumbersome and error-prone. In this paper, we propose an efficient framework for automated generation and verification of TEE specific properties. Specifically, we leverage Finite State Machine (FSM) analysis to automatically derive and validate security properties utilizing templates. The effectiveness of the proposed method is demonstrated through experimental evaluation of Intel Trust Domain Extension (TDX), highlighting its potential for verifying security and trustworthiness of modern trusted execution environments. Hasini Witharana, Hansika Weerasena, Prabhat Mishra 0001 |
DATE | 3 |
| 2025 | Formal verification of bioinformatics software using model checking and theorem provingabstractWhile there is explosive growth in the creation of biological data, researchers rely on ad hoc verification methods such as testing with small simulated datasets. Due to their importance in biology and biomedicine, there is a critical need to verify these algorithms as well as their implementations to ensure that the results and conclusions are trustworthy. In this paper, we explore an effective combination of model checking and theorem proving of bioinformatics software, including BiopLib, BWA, Jellyfish, SDSL, Dashing, SPAdes, and MUMmer. We provide results for model checking for bioinfomatics software libraries and theorem proving for specific properties. Our model checking framework found several potential flaws in the two tools (BiopLib and BWA). We have also detected several failing cases in Succinct Data Structures Library (SDSL). Hansika Weerasena, Aruna Jayasena, Christina Boucher 0001, Prabhat Mishra 0001 |
Briefings Bioinform. | 4 |
| 2025 | AI Trojan Attack for Evading Machine Learning-Based Detection of Hardware TrojansabstractThe globalized semiconductor supply chain significantly increases the risk of exposing System-on-Chip (SoC) designs to hardware Trojans. While machine learning (ML) based Trojan detection approaches are promising due to their scalability as well as detection accuracy, ML-based methods themselves are vulnerable from Trojan attacks. In this paper, we propose a robust backdoor attack on ML-based Trojan detection algorithms to demonstrate this serious vulnerability. The proposed framework is able to design an AI Trojan and implant it inside the ML model that can be triggered by specific inputs. Experimental results demonstrate that the proposed AI Trojans can bypass state-of-the-art defense algorithms. Moreover, our approach provides a fast and cost-effective solution in achieving 100% attack success rate that outperforms state-of-the art methods based on adversarial attacks. Zhixin Pan, Prabhat Mishra 0001 |
IEEE Trans. Computers | 2 |
| 2025 | FuSS: Coverage-Directed Hardware Fuzzing with Selective Symbolic Execution
Aruna Jayasena, Sai Suprabhanu Nallapaneni, Prabhat Mishra 0001 |
ACM Trans. Embed. Comput. Syst. | 3 |
| 2025 | CiseLeaks: Information Leakage Assessment of Cryptographic Instruction Set Extension PrototypesabstractSoftware based cryptographic implementations provide flexibility but they face performance limitations. In contrast, hardware based cryptographic accelerators utilize application-specific customization to provide real-time security solutions. Cryptographic instruction-set extensions (CISE) combine the advantages of both hardware and software based solutions to provide higher performance combined with the flexibility of atomic-level cryptographic operations. While CISE is widely used to develop security solutions, side-channel analysis of CISE-based devices is in its infancy. Specifically, it is important to evaluate whether the power usage and electromagnetic emissions of CISE-based devices have any correlation with its internal operations, which an adversary can exploit to deduce cryptographic secrets. In this paper, we propose a test vector leakage assessment framework to evaluate the pre-silicon prototypes at the early stages of the design life-cycle. Specifically, we first identify functional units with the potential for leaking information through power side-channel signatures and then evaluate them on system prototypes by generating the necessary firmware to maximize the side-channel signature. Our experimental results on two RISC-V based cryptographic extensions, RISCV-CRYPTO and XCRYPTO, demonstrated that seven out of eight prototype AES- and SHA-related functional units are vulnerable to leaking cryptographic secrets through their power side-channel signature even in full system mode with a statistical significance of$\alpha = 0.05$. Aruna Jayasena, Richard Bachmann, Prabhat Mishra 0001 |
IEEE Trans. Inf. Forensics Secur. | 3 |
| 2025 | FirmWall: Directed Symbolic Execution of Firmware Binaries for Defending Against Unauthorized System CallsabstractModern computing devices rely on root-of-trust (RoT) to ensure confidentiality and integrity of both application code and data while satisfying a wide variety of user requirements. The RoT provides essential cryptographic and security functions as services (implemented as system calls) to the host system, supporting the execution of both trusted and untrusted applications. It also enables a secure boot process for the host operating system and other functionalities to establish a trusted execution environment for user applications. The complexity of RoT implementation often introduces vulnerabilities, such as privilege escalation and code injection risks, which affect the security of user data during execution. In this paper, we propose a RoT firmware verification framework that acts as a firmware firewall (FirmWall) to enhance the overall security of the system. Specifically, we perform directed symbolic execution focused on system calls to verify RoT firmware binaries against security specifications, facilitating targeted patching to mitigate potential vulnerabilities. Our framework demonstrated significantly better coverage compared to state-of-the-art symbolic execution. It also confirmed the presence of multiple vulnerabilities (CVEs) in recent versions of ARM Trusted Firmware-M implementations. Aruna Jayasena, Prabhat Mishra 0001 |
IEEE Trans. Inf. Forensics Secur. | 2 |
| 2025 | Information Leakage Through Physical Layer Supply Voltage Coupling VulnerabilityabstractPower side-channel attacks are widely known for extracting information from data processed within a device while assuming that an attacker has physical access or the ability to modify the device. In this article, we introduce a novel side-channel vulnerability that leaks data-dependent power variations through physical layer supply voltage coupling (PSVC). Unlike traditional power side-channel attacks, the proposed vulnerability allows an adversary to mount an attack and extract information without modifying the device. In addition, unlike existing power-based remote attacks on field-programmable gate arrays (FPGAs), the PSVC vulnerability applies to both on-chip and on-board attacks. We assess the effectiveness of the PSVC vulnerability through three case studies, demonstrating several end-to-end attacks on general-purpose microcontrollers with varying adversary capabilities. These case studies provide evidence for the existence of the PSVC vulnerability, its applicability to on-chip as well as on-board side-channel attacks, and how it can eliminate the need for physical access to the target device, making it applicable to any off-the-shelf hardware. Our experiments also reveal that designing devices to operate at the lowest operational voltage significantly reduces the risk of PSVC side-channel vulnerability. Sahan Sanjaya, Aruna Jayasena, Prabhat Mishra 0001 |
IEEE Trans. Very Large Scale Integr. Syst. | 3 |
| 2024 | QcAssert: Quantum Device Testing with Concurrent AssertionsabstractQuantum devices are extremely noisy due to its inherent architecture. This can introduce errors or completely erase the information stored in qubits. High noise levels in a quantum device can lead to errors even when the quantum circuit is not buggy. Therefore, it is essential to verify that the noise level of the device is tolerable while running the quantum circuit. In this paper, we propose a quantum device testing framework using concurrent assertions. Specifically, we introduce a new type of assertion “QcAssert”, which has the ability to run concurrently with the quantum circuit to ensure that the quantum device is working as expected. We demonstrate the effectiveness of the QcAssert in dynamic device testing using a suite of popular quantum benchmarks, including Shor’s factoring algorithm and Grover’s search algorithm. Hasini Witharana, Daniel Volya, Prabhat Mishra 0001 |
ASPDAC | 3 |
| 2024 | EvilCS: An Evaluation of Information Leakage through Context Switching on Security EnclavesabstractSecurity enclaves provide isolated execution environments for trusted applications. However, modern processors utilize diverse performance enhancement methods (e.g., branch prediction and parallel execution) that can introduce security vulnerabilities. Specifically, if a processor leaks any information, an adversary can monitor and recover secrets from trusted applications. This paper makes a connection between context switching and information leakage in security enclaves. We present an evaluation framework that analyzes the potential channels through which context switching can expose sensitive information across the security enclave boundaries as a physical side-channel signature. Specifically, we propose a statistical information leakage assessment technique to evaluate the side-channel leakage of a security enclave during the pre-silicon design stage. Experimental evaluation on multiple RISC-V security enclaves reveals that context switching introduces power side channels that an adversary can exploit to infer the execution sequences as well as register values of trusted applications. Aruna Jayasena, Richard Bachmann, Prabhat Mishra 0001 |
DATE | 3 |
| 2024 | Breaking On-Chip Communication Anonymity Using Flow Correlation AttacksabstractNetwork-on-chip (NoC) is widely used to facilitate communication between components in sophisticated system-on-chip (SoC) designs. Security of the on-chip communication is crucial because exploiting any vulnerability in shared NoC would be a goldmine for an attacker that puts the entire computing infrastructure at risk. We investigate the security strength of existing anonymous routing protocols in NoC architectures, making two pivotal contributions. Firstly, we develop and perform a machine learning (ML)-based flow correlation attack on existing anonymous routing techniques in NoC systems, revealing that they provide only packet-level anonymity. Secondly, we propose a novel, lightweight anonymous routing protocol featuring outbound traffic tunneling and traffic obfuscation. This protocol is designed to provide robust defense against ML-based flow correlation attacks, ensuring both packet-level and flow-level anonymity. Experimental evaluation using both real and synthetic traffic demonstrates that our proposed attack successfully deanonymizes state-of-the-art anonymous routing in NoC architectures with high accuracy (up to 99%) for diverse traffic patterns. It also reveals that our lightweight anonymous routing protocol can defend against ML-based attacks with minor hardware and performance overhead. Hansika Weerasena, Prabhat Mishra 0001 |
ACM J. Emerg. Technol. Comput. Syst. | 2 |
| 2024 | HIVE: Scalable Hardware-Firmware Co-Verification Using Scenario-Based Decomposition and Automated Hint ExtractionabstractHardware-firmware co-verification is critical to design trustworthy systems. While formal methods can provide verification guarantees, due to the complexity of firmware and hardware, it can lead to state space explosion. There are promising avenues to reduce the state space during firmware verification through manual abstraction of hardware or manual generation of hints. Manual development of abstraction or hints requires domain expertise and can be time-consuming and error-prone, leading to incorrect proofs or inaccurate results. In this paper, we effectively combine the scalability of simulation-based validation and the completeness of formal verification. Our proposed approach is applicable to actual firmware and hardware implementations without requiring any manual intervention during formal model generation or hint extraction. To reduce the state space complexity, we utilize both static module-level analysis and dynamic execution of verification scenarios to automatically generate system-level hints. These hints guide the underlying solver to perform scalable equivalence checking using proofs. The extracted hints are validated against the implementation before using them in the proofs. Experimental evaluation on RISC-V based systems demonstrates that our proposed framework is scalable due to scenario-based decomposition and automated hint extraction. Moreover, our fully automated framework can identify complex bugs in actual firmware-hardware implementations. Aruna Jayasena, Prabhat Mishra 0001 |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 2 |
| 2024 | TD-Zero: Automatic Golden-Free Hardware Trojan Detection Using Zero-Shot LearningabstractSupply chain vulnerability provides the opportunity for the attackers to implant hardware Trojans in System-on-Chip (SoC) designs. While machine learning (ML) based Trojan detection is promising, it suffers from three practical limitations: (i) golden model may not be available, (ii) lack of human expertise for Trojan feature selection, and (iii) limited learning transferability can lead to unacceptable performance in new benchmarks with unseen Trojans. While recent approach based on transfer learning addresses some of these concerns, it still requires re-training for fine-tuning the model using domain-specific (e.g., hardware Trojan features) knowledge. In this paper, we propose a Trojan detection framework utilizing zero-shot learning to address the above challenges. The proposed framework adopts the idea of self-supervised learning, where a pre-trained graph convolutional network (GCN) is utilized to extract underlined common sense about hardware Trojans, and a metric learning task is used to measure the similarity between test inputs and malicious samples to make classification. Extensive experimental evaluation demonstrates that our approach has four major advantages compared to state-of-the-art techniques: (i) does not require any golden model during Trojan detection, (ii) can handle both unknown Trojans and unseen benchmarks without any changes to the network, (iii) drastic reduction in training time, and (iv) significant improvement in detection efficiency (10.5% on average). Zhixin Pan, Prabhat Mishra 0001 |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 2 |
| 2024 | Formal Verification of Virtualization-Based Trusted Execution EnvironmentsabstractTrusted execution environments (TEEs) provide a secure environment for computation, ensuring that the code and data inside the TEE are protected with respect to confidentiality and integrity. Virtual machine (VM)-based TEEs extend this concept by utilizing virtualization technology to create isolated execution spaces that can support a complete operating system or specific applications. As the complexity and importance of VM-based TEEs grow, ensuring their reliability and security through formal verification becomes crucial. However, these technologies often operate without formal assurances of their security properties. Our research introduces a formal framework for representing and verifying VM-based TEEs. This approach provides a rigorous foundation for defining and verifying key security attributes for safeguarding execution environments. To demonstrate the applicability of our verification framework, we conduct an analysis of real-world TEE platforms, including Intel’s trust domain extensions (TDX). This work not only emphasizes the necessity of formal verification in enhancing the security of VM-based TEEs but also provides a systematic approach for evaluating the resilience of these platforms against sophisticated adversarial models. Hasini Witharana, Hansika Weerasena, Prabhat Mishra 0001 |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 3 |
| 2024 | Revealing CNN Architectures via Side-Channel Analysis in Dataflow-based Inference AcceleratorsabstractConvolutional Neural Networks (CNNs) are widely used in various domains, including image recognition, medical diagnosis and autonomous driving. Recent advances in dataflow-based CNN accelerators have enabled CNN inference in resource-constrained edge devices. These dataflow accelerators utilize inherent data reuse of convolution layers to process CNN models efficiently. Concealing the architecture of CNN models is critical for privacy and security. This article evaluates memory-based side-channel information to recover CNN architectures from dataflow-based CNN inference accelerators. The proposed attack exploits spatial and temporal data reuse of the dataflow mapping on CNN accelerators and architectural hints to recover the structure of CNN models. Experimental results demonstrate that our proposed side-channel attack can recover the structures of popular CNN models, namely, Lenet, Alexnet, VGGnet16, and YOLOv2. Hansika Weerasena, Prabhat Mishra 0001 |
ACM Trans. Embed. Comput. Syst. | 2 |
| 2024 | Assertion-Based Validation using Clustering and Dynamic Refinement of Hardware CheckersabstractPost-silicon validation is a vital step in System-on-Chip (SoC) design cycle. A major challenge in post-silicon validation is the limited observability of internal signal states using trace buffers. Hardware assertions are promising to improve observability during post-silicon debug. Unfortunately, we cannot synthesize thousands (or millions) of pre-silicon assertions as hardware checkers (coverage monitors) due to hardware overhead constraints. Therefore, we need to select the most profitable assertions based on design constraints. However, the design constraints can also change dynamically during the device lifetime due to changes in use-case scenarios as well as input variations. Therefore, assertion selection needs to dynamically adapt based on changing circumstances. In this article, we propose an assertion-based post-silicon validation framework to address the above challenges. Specifically, this article makes two important contributions. We propose a clustering-based assertion selection technique that can select the most profitable pre-silicon assertions to maximize the fault coverage. We also present a cost-aware dynamic refinement technique that can select beneficial hardware checkers during runtime based on changing design constraints. Experimental evaluation demonstrates that our proposed pre-silicon assertion selection can outperform state-of-the-art assertion ranking methods (Goldmine and HARM). The results also highlight that our proposed post-silicon dynamic refinement can accurately predict area (less than 5% error) and power consumption (less than 3% error) of hardware checkers at runtime. This accurate prediction enables the identification of the most profitable hardware checkers based on design constraints. Sahan Sanjaya, Hasini Witharana, Prabhat Mishra 0001 |
ACM Trans. Design Autom. Electr. Syst. | 3 |
| 2024 | Security of Electrical, Optical, and Wireless On-chip Interconnects: A SurveyabstractThe advancement of manufacturing technologies has enabled the integration of more intellectual property (IP) cores on the same system-on-chip (SoC). Scalable and high throughput on-chip communication architecture has become a vital component in today’s SoCs. Diverse technologies such as electrical, wireless, optical, and hybrid are available for on-chip communication with different architectures supporting them. On-chip communication sub-system is shared across all the IPs and continuously used throughout the lifetime of the SoC. Therefore, the security of the on-chip communication is crucial, because exploiting any vulnerability would be a goldmine for an attacker. In this survey, we provide a comprehensive review of threat models, attacks, and countermeasures over diverse on-chip communication technologies as well as sophisticated architectures. Hansika Weerasena, Prabhat Mishra 0001 |
ACM Trans. Design Autom. Electr. Syst. | 2 |
| 2024 | Incremental Concolic Testing of Register-Transfer Level DesignsabstractConcolic testing is a scalable solution for automated generation of directed tests for validation of hardware designs. Unfortunately, concolic testing fails to cover complex corner cases such as hard-to-activate branches. In this article, we propose an incremental concolic testing technique to cover hard-to-activate branches in register-transfer level (RTL) models. We show that a complex branch condition can be viewed as a sequence of easy-to-activate events. We map the branch coverage problem to the coverage of a sequence of events. We propose an efficient algorithm to cover the sequence of events using concolic testing. Specifically, the test generated to activate the current event is used as the starting point to activate the next event in the sequence. Experimental results demonstrate that our approach can be used to generate directed tests to cover complex corner cases in RTL models while state-of-the-art methods fail to activate them. Hasini Witharana, Aruna Jayasena, Prabhat Mishra 0001 |
ACM Trans. Design Autom. Electr. Syst. | 3 |
| 2024 | Quantum Measurement Classification Using Statistical LearningabstractInterpreting the results of a quantum computer can pose a significant challenge due to inherent noise in these mesoscopic quantum systems. Quantum measurement, a critical component of quantum computing, involves determining the probabilities linked with quantum states post-multiple circuit computations based on quantum readout values provided by hardware. While there are promising classification-based solutions, they can either misclassify or necessitate excessive measurements, thereby proving to be costly. This article puts forth an efficient method to discern the quantum state by analyzing the probability distributions of data post-measurement. Specifically, we employ cumulative distribution functions to juxtapose the measured distribution of a sample against the distributions of basis states. The efficacy of our approach is demonstrated through experimental results on a superconducting transmon qubit architecture, which shows a substantial decrease (88%) in single qubit readout error compared to state-of-the-art measurement techniques. Moreover, we report additional error reduction (12%) compared to state-of-the-art measurement techniques when our technique is applied to enhance existing multi-qubit classification techniques. We also demonstrate the applicability of our proposed method for higher dimensional quantum systems, including classification of single qutrits as well as multiple qutrits. Zachery Utt, Daniel Volya, Prabhat Mishra 0001 |
ACM Trans. Quantum Comput. | 3 |
| 2023 | Hardware Trojan Detection Using Shapley Ensemble BoostingabstractDue to globalized semiconductor supply chain, there is an increasing risk of exposing system-on-chip designs to hardware Trojans (HT). While there are promising machine Learning based HT detection techniques, they have three major limitations: ad-hoc feature selection, lack of explainability, and vulnerability towards adversarial attacks. In this paper, we propose a novel HT detection approach using an effective combination of Shapley value analysis and boosting framework. Specifically, this paper makes two important contributions. We use Shapley value (SHAP) to analyze the importance ranking of input features. It not only provides explainable interpretation for HT detection, but also serves as a guideline for feature selection. We utilize boosting (ensemble learning) to generate a sequence of lightweight models that significantly reduces the training time while provides robustness against adversarial attacks. Experimental results demonstrate that our approach can drastically improve both detection accuracy (up to 24.6%) and time efficiency (up to 5.1x) compared to state-of-the-art HT detection techniques. Zhixin Pan, Prabhat Mishra 0001 |
ASP-DAC | 2 |
| 2023 | Quantum Data Compression for Efficient Generation of Control PulsesabstractIn order to physically realize a robust quantum gate, a specifically tailored laser pulse needs to be derived via strategies such as quantum optimal control. Unfortunately, such strategies face exponential complexity with quantum system size and become infeasible even for moderate-sized quantum circuits. In this paper, we propose an automated framework for effective utilization of these quantum resources. Specifically, this paper makes three important contributions. First, we utilize an effective combination of register compression and dimensionality reduction to reduce the area of a quantum circuit. Next, due to the properties of an autoencoder, the compressed gates produced are robust even in the presence of noise. Finally, our proposed compression reduces the computation time of quantum control. Experimental evaluation using popular quantum algorithms demonstrates that our proposed approach can enable efficient generation of noise-resilient control pulses while state-of-the-art fails to handle large-scale quantum systems. Daniel Volya, Prabhat Mishra 0001 |
ASP-DAC | 2 |
| 2023 | Quantum Measurement Discrimination using Cumulative Distribution FunctionsabstractQuantum measurement is one of the critical steps in quantum computing that determines the probabilities associated with qubit states after conducting several circuit ex-ecutions and measurements. As a mesoscopic quantum system, real quantum computers are prone to noise. Therefore, a major challenge in quantum measurement is how to correctly inter-pret the noisy results of a quantum computer. While there are promising classification based solutions, they either produce incorrect results (misclassify) or require many measurements (expensive). In this paper, we present an efficient technique to estimate a qubit's state through analysis of probability distributions of post-measurement data. Specifically, we estimate the state of a qubit using cumulative distribution functions to compare the measured distribution of a sample with the distributions of basis states$\vert 0\rangle$and$\vert 1\rangle$. Our experimental results demonstrate a drastic reduction (78%) in single qubit readout error. It also provides significant reduction (12%) when used to boost existing multi-qubit discriminator models. Zachery Utt, Daniel Volya, Prabhat Mishra 0001 |
DATE | 3 |
| 2023 | Dynamic Refinement of Hardware Assertion CheckersabstractPost-silicon validation is a vital step in System-on-Chip (SoC) design cycle. A major challenge in post-silicon validation is the limited observability of internal signal states using trace buffers. Hardware assertions are promising to improve the observability during post-silicon debug. Unfortunately, we cannot synthesize thousands (or millions) of pre-silicon assertions as hardware checkers (coverage monitors) due to hardware overhead constraints. Prior efforts considered synthesis of a small set of checkers based on design constraints. However, these design constraints can change dynamically during the device lifetime due to changes in use-case scenarios as well as input variations. In this paper, we explore dynamic refinement of hardware checkers based on changing design constraints. Specifically, we propose a cost-based assertion selection framework that utilizes non-linear optimization as well as machine learning. Experimental results demonstrate that our machine learning model can accurately predict area (less than 5% error) and power consumption (less than 3% error) of hardware checkers at runtime. This accurate prediction enables close-to-optimal dynamic refinement of checkers based on design constraints. Hasini Witharana, Sahan Sanjaya, Prabhat Mishra 0001 |
DATE | 3 |
| 2023 | Automated Generation of Security Assertions for RTL ModelsabstractSystem-on-Chip (SoC) security is vital in designing trustworthy systems. Detecting and fixing a vulnerability in the early stages is easier and cost-effective. Assertion-based verification is widely used for functional validation of Register-Transfer Level (RTL) designs. Assertions can improve the controllability and observability that can lead to faster error detection and localization. Although assertions are widely used for functional validation of RTL models, there is limited effort in applying assertions to detect SoC security vulnerabilities. Specifically, a fundamental challenge in SoC security and trust validation is how to develop high-quality security assertions. In this article, we perform automated vulnerability analysis of RTL models to generate security assertions for six classes of vulnerabilities. Experimental results show that the generated security assertions can detect a wide variety of vulnerabilities. Our automated framework can drastically reduce the overall security validation effort compared to the manual development of security assertions. Automated generation of security assertions will enable assertion-based verification to be one of the most promising pre-silicon security sign-off solutions. Hasini Witharana, Aruna Jayasena, Andrew Whigham, Prabhat Mishra 0001 |
ACM J. Emerg. Technol. Comput. Syst. | 4 |
| 2023 | Scalable Detection of Hardware Trojans Using ATPG-Based Activation of Rare EventsabstractSemiconductor supply chain vulnerability is a major concern in designing trustworthy systems. Malicious implants, popularly known as hardware Trojans (HTs), can get introduced at different stages in the system-on-chip (SoC) design cycle. While there are promising test generation techniques for HT detection, they have two practical limitations: 1) these approaches are designed to activate rare states while ignoring rare transitions and 2) these approaches are not scalable for large designs. In this article, we propose a scalable test generation framework to address the above challenges. Our threat model assumes that an adversary may exploit rare events consisting of rare signals (states) as well as rare branches (transitions). We show that the rare branch coverage problem can be mapped to the rare signal coverage problem. We propose a scalable framework for detecting HTs using automated test pattern generation (ATPG)-based activation of rare events. Specifically, we utilize the complementary abilities of N-detection and maximal clique activation of rare events to generate efficient test patterns. Experimental evaluation shows that our ATPG-based framework is scalable and significantly outperforms the state-of-the-art test generation-based Trojan detection techniques. Aruna Jayasena, Prabhat Mishra 0001 |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 2 |
| 2023 | TVLA*: Test Vector Leakage Assessment on Hardware Implementations of Asymmetric Cryptography AlgorithmsabstractTest vector leakage assessment (TVLA*) evaluates the side-channel leakage of sensitive information from the hardware implementation of a design. While TVLA* for symmetric cryptography has been well studied, it is not applicable to asymmetric cryptography algorithms. Asymmetric-key algorithms involve complex computations in multiple stages that can lead to varying trace lengths depending on input parameters and associated constraints. In this article, we design an effective TVLA* technique for asymmetric-key cryptosystems that can compare lengthy trace data with a good statistical resolution and generate valid input (test) patterns to satisfy specific constraints. Specifically, this article makes the following major contributions. The proposed test generation algorithm can produce valid test patterns to maximize the power signature differences. Our proposed partition-based differential power analysis can significantly improve the TVLA* accuracy. Extensive evaluation using elliptic curve cryptography algorithms demonstrates that the proposed TVLA* framework can handle type 1 and type 2 statistical errors and evaluate hardware implementations of asymmetric cryptography algorithms with a statistical confidence of 99.999%. Aruna Jayasena, Emma Andrews, Prabhat Mishra 0001 |
IEEE Trans. Very Large Scale Integr. Syst. | 3 |
| 2022 | Design of AI Trojans for Evading Machine Learning-based Detection of Hardware TrojansabstractThe globalized semiconductor supply chain significantly increases the risk of exposing System-on-Chip (SoC) designs to malicious implants, popularly known as hardware Trojans. Traditional simulation-based validation is unsuitable for detection of carefully-crafted hardware Trojans with extremely rare trigger conditions. While machine learning (ML) based Trojan detection approaches are promising due to their scalability as well as detection accuracy, ML-based methods themselves are vulnerable from Trojan attacks. In this paper, we propose a robust backdoor attack on ML-based Trojan detection algorithms to demonstrate this serious vulnerability. The proposed framework is able to design an AI Trojan and implant it inside the ML model that can be triggered by specific inputs. Experimental results demonstrate that the proposed AI Trojans can bypass state-of-the-art defense algorithms. Moreover, our approach provides a fast and cost-effective solution in achieving 100% attack success rate that significantly outperforms state-of-the art approaches based on adversarial attacks. Zhixin Pan, Prabhat Mishra 0001 |
DATE | 2 |
| 2022 | Hardware Acceleration of Explainable Machine LearningabstractMachine learning (ML) is successful in achieving human-level performance in various fields. However, it lacks the ability to explain an outcome due to its black-box nature. While recent efforts on explainable ML has received significant attention, the existing solutions are not applicable in real-time systems since they map interpretability as an optimization problem, which leads to numerous iterations of time-consuming complex computations. To make matters worse, existing implementations are not amenable for hardware-based acceleration. In this paper, we propose an efficient framework to enable acceleration of explainable ML procedure with hardware accelerators. We explore the effectiveness of both Tensor Processing Unit (TPU) and Graphics Processing Unit (GPU) based architectures in accelerating explainable ML. Specifically, this paper makes three important contributions. (1) To the best of our knowledge, our proposed work is the first attempt in enabling hardware acceleration of explainable ML. (2) Our proposed solution exploits the synergy between matrix convolution and Fourier transform, and therefore, it takes full advantage of TPU's inherent ability in accelerating matrix computations. (3) Our proposed approach can lead to real-time outcome interpretation. Extensive experimental evaluation demonstrates that proposed approach deployed on TPU can provide drastic improvement in interpretation time (39x on average) as well as energy efficiency (69x on average) compared to existing acceleration techniques. Zhixin Pan, Prabhat Mishra 0001 |
DATE | 2 |
| 2022 | Speculative Load Forwarding Attack on Modern ProcessorsabstractModern processors deliver high performance by utilizing advanced features such as out-of-order execution, branch prediction, speculative execution, and sophisticated buffer management. Unfortunately, these techniques have introduced diverse vulnerabilities including Spectre, Meltdown, and microarchitectural data sampling (MDS). Although Spectre and Meltdown can leak data via memory side channels, MDS has shown to leak data from the CPU internal buffers in Intel architectures. AMD has reported that its processors are not vulnerable to MDS/Meltdown type attacks. In this paper, we present a Meltdown/MDS type of attack to leak data from the load queue in AMD Zen family architectures. To the best of our knowledge, our approach is the first attempt in developing an attack on AMD architectures using speculative load forwarding to leak data through the load queue. Experimental evaluation demonstrates that our proposed attack is successful on multiple machines with AMD processors. We also explore a lightweight mitigation to defend against speculative load forwarding attack on modern processors. Hasini Witharana, Prabhat Mishra 0001 |
ICCAD | 2 |
| 2022 | Efficient Finite State Machine Encoding for Defending Against Laser Fault Injection AttacksabstractFinite State Machines (FSMs) are widely used to implement complex computation sequences and communication protocols. An FSM may consist of different states with different privilege levels, such as protected and non-protected. Ideally, switching from a non-protected state to a protected state should involve an authorization transition. However, with Laser-based Fault injection (LFI), an attacker can bypass authorization by flipping bits in the FSM’s state vector. In order to mitigate LFI vulnerability, one can encode the FSM states with the objective of maintaining a large Hamming Distance (HD) between each pair of states. The existing FSM encoding algorithms are either very slow, rely on the user’s mathematical ability to manually generate certain state encodings, or lead to unacceptable area overhead. In this paper, we propose an automated framework for generating FSM encodings to defend against LFI attacks. The proposed technique is a fast linear code-based heuristic to produce area-efficient results. We also propose an application-specific simplification to further reduce the area overhead. Experimental results demonstrate that our proposed method is several orders-of-magnitude faster than the state-of-the-art approaches. Our approach also significantly reduces the state code length (50% on average) compared to state-of-the-art approaches. Aruna Jayasena, Khushboo Rani, Prabhat Mishra 0001 |
ICCD | 3 |
| 2022 | Modeling of Noisy Quantum Circuits using Random Matrix TheoryabstractA major challenge in exploiting the principles of quantum information is the influence of noise which tends to work against the quantum features of a system. The traditional quantum gate error model provides a general framework to study noisy quantum circuits, but may fail to capture intricate microscopic interactions between qubits in addition to the environment. This can significantly overestimate the feasibility of implementing useful quantum algorithms on physical quantum hardware. In this paper, we study a noise model driven by random matrix theory that captures an effective microscopic interaction, and assess the suitability of the quantum gate error model. Our approach assumes noise arises due to interactions with many physical sources, and modeled using random matrix theory and applied to the quantum circuit model. Daniel Volya, Prabhat Mishra 0001 |
ICCD | 2 |
| 2022 | Hardware-Assisted Malware Detection and Localization Using Explainable Machine LearningabstractMalicious software, popularly known as malware, is widely acknowledged as a serious threat to modern computing systems. Software-based solutions, such as anti-virus software (AVS), are not effective since they rely on matching patterns that can be easily fooled by carefully crafted malware with obfuscation or other deviation capabilities. While recent malware detection methods provide promising results through an effective utilization of hardware features, the detection results cannot be interpreted in a meaningful way. In this paper, we propose a hardware-assisted malware detection framework using explainable machine learning. This paper makes three important contributions. First, we theoretically establish that our proposed method can provide an interpretable explanation of classification results to address the challenge of transparency. Next, we show that the explainable outcome through effective utilization of hardware performance counters and embedded trace buffer can lead to accurate localization of malicious behavior. Finally, we have performed efficiency versus accuracy trade-off analysis using decision tree and recurrent neural networks. Extensive evaluation using a wide variety of real-world malware dataset demonstrates that our framework can produce accurate and human-understandable malware detection results with provable guarantees. Zhixin Pan, Jennifer Sheldon, Prabhat Mishra 0001 |
IEEE Trans. Computers | 3 |
| 2022 | Data Perturbation and Recovery of Time Series Gene Expression DataabstractCells, in order to regulate their activities, process transcripts by controlling which genes to transcribe and by what amount. The transcription level of genes often change over time. Rate of change of gene transcription varies between genes. It can even change for the same gene across different members of a population. Thus, for a given gene, it is important to study the transcription level not only at a single time point, but across multiple time points to capture changes in patterns of gene expression which underlies several phenotypic or external factors. In such a dataset perturbation can happen due to which it may have missing transcription values for different samples at different time points. In this paper, we define three data perturbation models that are significant with respect to random deletion. We also define a recovery method that recovers data loss in the perturbed dataset such that the error is minimized. Our experimental results show that the recovery method compensates for the loss made by perturbation models. We show by means of two measures, namely, normalized distance and Pearson's correlation coefficient that the distance between the original and perturbed dataset is more than the distance between original and recovered dataset. Aisharjya Sarkar, Prabhat Mishra 0001, Tamer Kahveci |
IEEE ACM Trans. Comput. Biol. Bioinform. | 2 |
| 2022 | Digital Watermarking for Detecting Malicious Intellectual Property Cores in NoC ArchitecturesabstractSystem-on-chip (SoC) developers utilize intellectual property (IP) cores from third-party vendors due to increasing design complexity, cost, as well as time-to-market constraints. A typical SoC consists of a wide variety of IP cores [such as processor, memory, controller, and field-programmable gate array (FPGA)] that interact using a network-on-chip (NoC). This global trend of designing SoCs using third-party IPs raises serious concerns about security vulnerabilities. Since NoC facilitates communication between all IPs in an SoC, NoC is the ideal place for any hardware Trojans to hide and launch a plethora of attacks. Due to the resource-constrained nature of SoCs, developing security solutions against such attacks is a major challenge. In particular, in an eavesdropping attack, a Trojan-infected router copies packets transferred through the NoC and reroutes the duplicated packets to an accompanying malicious application running on another IP in an attempt to extract confidential information. While authenticated encryption can thwart such attacks, it incurs unacceptable overhead in resource-constrained SoCs. In this article, we propose a lightweight alternative defense based on digital watermarking techniques. We develop theoretical models to provide security guarantees. Experiments using realistic SoC models and diverse applications demonstrate that our approach can significantly outperform state-of-the-art methods. Subodha Charles, Vincent Bindschaedler, Prabhat Mishra 0001 |
IEEE Trans. Very Large Scale Integr. Syst. | 3 |
| 2021 | Automated Test Generation for Hardware Trojan Detection using Reinforcement LearningabstractDue to globalized semiconductor supply chain, there is an increasing risk of exposing System-on-Chip (SoC) designs to malicious implants, popularly known as hardware Trojans. Unfortunately, traditional simulation-based validation using millions of test vectors is unsuitable for detecting stealthy Trojans with extremely rare trigger conditions due to exponential input space complexity of modern SoCs. There is a critical need to develop efficient Trojan detection techniques to ensure trustworthy SoCs. While there are promising test generation approaches, they have serious limitations in terms of scalability and detection accuracy. In this paper, we propose a novel logic testing approach for Trojan detection using an effective combination of testability analysis and reinforcement learning. Specifically, this paper makes three important contributions. 1) Unlike existing approaches, we utilize both controllability and observability analysis along with rareness of signals to significantly improve the trigger coverage. 2) Utilization of reinforcement learning considerably reduces the test generation time without sacrificing the test quality. 3) Experimental results demonstrate that our approach can drastically improve both trigger coverage (14.5% on average) and test generation time (6.5 times on average) compared to state-of-the-art techniques. Zhixin Pan, Prabhat Mishra 0001 |
ASP-DAC | 2 |
| 2021 | Quantum Spectral Clustering of Mixed GraphsabstractSpectral graph partitioning is a well known technique to estimate clusters in undirected graphs. Recent approaches explored efficient spectral algorithms for directed and mixed graphs utilizing various matrix representations. Despite its success in clustering tasks, classical spectral algorithms suffer from a cubic growth in runtime. In this paper, we propose a quantum spectral clustering algorithm for discovering clusters and properties of mixed graphs. Our experimental results based on numerical simulations demonstrate that our quantum spectral clustering outperforms classical spectral clustering techniques. Specifically, our approach leads to a linear growth in complexity, while state-of-the-art classical counterpart leads to cubic growth. In a case study, we apply our proposed algorithm to preform unsupervised machine learning using both real and simulated quantum computers. This work opens an avenue for efficient implementation of machine learning algorithms on directed as well as mixed graphs by making use of the inherent potential quantum speedup. Daniel Volya, Prabhat Mishra 0001 |
DAC | 2 |
| 2021 | Real-Time Detection and Localization of Denial-of-Service Attacks in Heterogeneous Vehicular NetworksabstractVehicular communication has emerged as a powerful tool for providing a safe and comfortable driving experience for users. Long Term Evolution (LTE) supports and enhances the quality of vehicular communication due to its properties such as, high data rate, spatial reuse, and low delay. However, high mobility of vehicles introduces a wide variety of security threats, including Denial-of-Service (DoS) attacks. In this paper, we propose an effective solution for real-time detection and localization of DoS attacks in an LTE-based vehicular network with mobile network components (e.g., vehicles, femto access points, etc.). We consider malicious data transmission by vehicles in two ways - using real identification (unintentional) and using fake identification. Our attack detection technique is based on data packet counter and average packet delivery ratio which helps to efficiently detect attack faster than traditional approaches. We use triangulation method for localizing the attacker, and analyze average packet delay incurred by vehicles by modelling the system as an M/M/m queue. Simulation results demonstrate that our proposed technique significantly outperforms state-of-the-art techniques. Meenu Rani Dey, Moumita Patra, Prabhat Mishra 0001 |
DATE | 3 |
| 2021 | Hardware-Assisted Malware Detection using Machine LearningabstractMalicious software, popularly known as malware, is a serious threat to modern computing systems. A comprehensive cybercrime study by Ponemon Institute highlights that malware is the most expensive attack for organizations, with an average revenue loss of $2.6 million per organization in 2018 (11% increase compared to 2017). Recent high-profile malware attacks coupled with serious economic implications have dramatically changed our perception of threat from malware. Software-based solutions, such as anti-virus programs, are not effective since they rely on matching patterns (signatures) that can be easily fooled by carefully crafted malware with obfuscation or other deviation capabilities. Moreover, software-based solutions are not fast enough for real-time malware detection in safety-critical systems. In this paper, we investigate promising approaches for hardware-assisted malware detection using machine learning. Specifically, we explore how machine learning can be effective for malware detection utilizing hardware performance counters, embedded trace buffer as well as on-chip network traffic analysis. Zhixin Pan, Jennifer Sheldon, Chamika Sudusinghe, Subodha Charles, Prabhat Mishra 0001 |
DATE | 5 |
| 2021 | Denial-of-service attack detection using machine learning in network-on-chip architecturesabstractState-of-the-art System-on-Chip (SoC) designs consist of many Intellectual Property (IP) cores that interact using a Network-on-Chip (NoC) architecture. SoC designers increasingly rely on global supply chains for obtaining third-party IPs. In addition to inherent vulnerabilities associated with utilizing third-party IPs, NoC based SoCs enable attackers to exploit the distributed nature of NoC and its connectivity with various IPs to launch a plethora of attacks. Specifically, Denial-of-Service (DoS) attacks pose a serious threat in degrading the SoC performance by flooding the NoC with unnecessary packets. In this paper, we present a machine learning-based runtime monitoring mechanism to detect DoS attacks. The models are statically trained and used for runtime attack detection leading to minimum runtime performance overhead. Our approach is capable of detecting DoS attacks with high accuracy, even in the presence of unpredictable NoC traffic patterns caused by various application mappings. We extensively explore machine learning models and features to provide a comprehensive study on how to use machine learning for DoS attack detection in NoC-based SoCs. Chamika Sudusinghe, Subodha Charles, Prabhat Mishra 0001 |
NOCS | 3 |
| 2021 | Scalable Concolic Testing of RTL ModelsabstractSimulation is widely used for validation of Register-Transfer-Level (RTL) models. While simulating with millions of random or constrained-random tests can cover majority of the functional scenarios, the number of remaining scenarios can still be huge (hundreds or thousands) in case of today's industrial designs. Hard-to-activate branches are one of the major contributors for such remaining/untested scenarios. While directed test generation techniques using formal methods are promising in activating branches, it is infeasible to apply them on large designs due to state space explosion. In this article, we propose a fully automated and scalable approach to cover the hard-to-activate branches using concolic testing of RTL models. While application of concolic testing on hardware designs has shown some promising results in improving the overall coverage, they are not designed to activate specific targets such as uncovered corner cases and rare scenarios. In other words, existing concolic testing approaches address state space explosion problem but leads to path explosion problem while searching for the uncovered targets. Our proposed approach maps directed test generation problem to target search problem while avoiding overlapping searches involving multiple targets. This article makes two important contributions. (1) We propose a directed test generation technique to activate a target by effective utilization of concolic testing on RTL models. (2) We develop efficient learning and clustering techniques to minimize the overlapping searches across targets to drastically reduce the overall test generation effort. Experimental results demonstrate that our approach significantly outperforms the state-of-the-art methods in terms of test generation time (up to 205X, 69X on average) as well as memory requirements (up to 31X, 7X on average). Yangdi Lyu, Prabhat Mishra 0001 |
IEEE Trans. Computers | 2 |
| 2021 | Scalable Activation of Rare Triggers in Hardware Trojans by Repeated Maximal Clique SamplingabstractHardware Trojans are serious threat to security and reliability of computing systems. It is hard to detect these malicious implants using traditional validation methods since an adversary is likely to hide them under rare trigger conditions. While existing statistical test generation methods are promising for Trojan detection, they are not suitable for activating extremely rare trigger conditions in stealthy Trojans. To address the fundamental challenge of activating rare triggers, we propose a new test generation paradigm for trigger activation by repeated maximal clique sampling (TARMAC). The basic idea is to utilize a satisfiability modulo theories (SMTs) solver to construct a test corresponding to each maximal clique. This article makes three fundamental contributions: 1) it proves that the trigger activation problem can be mapped to clique cover problem, and the test vectors generated by covering maximal cliques are complete and compact; 2) it proposes efficient test generation algorithms to activate trigger conditions by repeated maximal clique sampling; and 3) it outlines an efficient mechanism to run the clique sampling in parallel to significantly improve the scalability of our test generation framework. The experimental results demonstrate that our proposed approach is scalable and it outperforms state-of-the-art approaches by several orders-of-magnitude in detecting stealthy Trojans. Yangdi Lyu, Prabhat Mishra 0001 |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 2 |
| 2021 | MaxSense: Side-channel Sensitivity Maximization for Trojan Detection Using Statistical Test PatternsabstractDetection of hardware Trojans is vital to ensure the security and trustworthiness of System-on-Chip (SoC) designs. Side-channel analysis is effective for Trojan detection by analyzing various side-channel signatures such as power, current, and delay. In this article, we propose an efficient test generation technique to facilitate side-channel analysis utilizing dynamic current. While early work on current-aware test generation has proposed several promising ideas, there are two major challenges in applying it on large designs: (i) The test generation time grows exponentially with the design complexity, and (ii) it is infeasible to detect Trojans, since the side-channel sensitivity is marginal compared to the noise and process variations. Our proposed work addresses both challenges by effectively exploiting the affinity between the inputs and rare (suspicious) nodes. The basic idea is to quickly find the profitable ordered pairs of test vectors that can maximize side-channel sensitivity. This article makes two important contributions: (i) It proposed an efficient test generation algorithm that can produce the first patterns in the test vectors to maximize activation of suspicious nodes using an SMT solver, and (ii) it developed a genetic-algorithm based test generation technique to produce the second patterns in the test vectors to maximize the switching in the suspicious regions while minimizing the switching in the rest of the design. Our experimental results demonstrate that we can drastically improve both the side-channel sensitivity (62× on average) and time complexity (13× on average) compared to the state-of-the-art test generation techniques. Yangdi Lyu, Prabhat Mishra 0001 |
ACM Trans. Design Autom. Electr. Syst. | 2 |
| 2021 | Directed Test Generation for Activation of Security Assertions in RTL ModelsabstractAssertions are widely used for functional validation as well as coverage analysis for both software and hardware designs. Assertions enable runtime error detection as well as faster localization of errors. While there is a vast literature on both software and hardware assertions for monitoring functional scenarios, there is limited effort in utilizing assertions to monitor System-on-Chip (SoC) security vulnerabilities. We have identified common SoC security vulnerabilities and defined several classes of assertions to enable runtime checking of security vulnerabilities. A major challenge in assertion-based validation is how to activate the security assertions to ensure that they are valid. While existing test generation using model checking is promising, it cannot generate directed tests for large designs due to state space explosion. We propose an automated and scalable mechanism to generate directed tests using a combination of symbolic execution and concrete simulation of RTL models. Experimental results on diverse benchmarks demonstrate that the directed tests are able to activate security assertions non-vacuously. Hasini Witharana, Yangdi Lyu, Prabhat Mishra 0001 |
ACM Trans. Design Autom. Electr. Syst. | 3 |
| 2021 | Data Criticality in Multithreaded Applications: An Insight for Many-Core SystemsabstractMultithreaded applications are capable of exploiting the full potential of many-core systems. However, network-on-chip (NoC)-based intercore communication in many-core systems is responsible for 60%-75% of the miss latency experienced by multithreaded applications. Delay in the arrival of critical data at the requesting core severely hampers performance. This brief presents some interesting insights about how critical data are requested from the memory by multithreaded applications. Then it investigates the cause of delay in NoC and how it affects the performance. Finally, this brief shows how NoC-aware memory access optimizations can significantly improve performance. Our experimental evaluation considers Early Restart memory access optimization and demonstrates that by exploiting available NoC resources, critical data can be prioritized to reduce miss penalty by 11% and improve overall system performance by 9%. Abhijit Das 0002, John Jose, Prabhat Mishra 0001 |
IEEE Trans. Very Large Scale Integr. Syst. | 3 |
| 2020 | Automated Test Generation for Activation of Assertions in RTL ModelsabstractA major challenge in assertion-based validation is how to activate the assertions to ensure that they are valid. While existing test generation using model checking is promising, it cannot generate directed tests for large designs due to state space explosion. We propose an automated and scalable mechanism to generate directed tests using a combination of symbolic execution and concrete simulation of RTL models. Experimental results show that the directed tests are able to activate assertions non-vacuously. Yangdi Lyu, Prabhat Mishra 0001 |
ASP-DAC | 2 |
| 2020 | Automated Trigger Activation by Repeated Maximal Clique SamplingabstractHardware Trojans are serious threat to security and reliability of computing systems. It is hard to detect these malicious implants using traditional validation methods since an adversary is likely to hide them under rare trigger conditions. While existing statistical test generation methods are promising for Trojan detection, they are not suitable for activating extremely rare trigger conditions in stealthy Trojans. To address the fundamental challenge of activating rare triggers, we propose a new test generation paradigm by mapping trigger activation problem to clique cover problem. The basic idea is to utilize a satisfiability solver to construct a test corresponding to each maximal clique. This paper makes two fundamental contributions: 1) it proves that the trigger activation problem can be mapped to clique cover problem, 2) it proposes an efficient test generation algorithm to activate trigger conditions by repeated maximal clique sampling. Experimental results demonstrate that our approach is scalable and it outperforms state-of-the-art approaches by several orders-of-magnitude in detecting stealthy Trojans. Yangdi Lyu, Prabhat Mishra 0001 |
ASP-DAC | 2 |
| 2020 | Lightweight Anonymous Routing in NoC based SoCsabstractSystem-on-Chip (SoC) supply chain is widely acknowledged as a major source of security vulnerabilities. Potentially malicious third-party IPs integrated on the same Network-on-Chip (NoC) with the trusted components can lead to security and trust concerns. While secure communication is a well studied problem in computer networks domain, it is not feasible to implement those solutions on resource-constrained SoCs. In this paper, we present a lightweight anonymous routing protocol for communication between IP cores in NoC based SoCs. Our method eliminates the major overhead associated with traditional anonymous routing protocols while ensuring that the desired security goals are met. Experimental results demonstrate that existing security solutions on NoC can introduce significant (1.5X) performance degradation, whereas our approach provides the same security features with minor (4%) impact on performance. Subodha Charles, Megan Logan, Prabhat Mishra 0001 |
DATE | 3 |
| 2020 | Automated Test Generation for Trojan Detection using Delay-based Side Channel AnalysisabstractSide-channel analysis is widely used for hardware Trojan detection in integrated circuits by analyzing various side-channel signatures, such as timing, power and path delay. Existing delay-based side-channel analysis techniques have two major bottlenecks: (i) they are not suitable in detecting Trojans since the delay difference between the golden design and a Trojan inserted design is negligible, and (ii) they are not effective in creating robust delay signatures due to reliance on random and ATPG based test patterns. In this paper, we propose an efficient test generation technique to detect Trojans using delay-based side channel analysis. This paper makes two important contributions. (1) We propose an automated test generation algorithm to produce test patterns that are likely to activate trigger conditions, and change critical paths. Compared to existing approaches where delay difference is solely based on extra gates from a small Trojan, the change of critical paths by our approach will lead to significant difference in path delay. (2) We propose a fast and efficient reordering technique to maximize the delay deviation between the golden design and Trojan inserted design. Experimental results demonstrate that our approach significantly outperforms state-of-the-art approaches that rely on ATPG or random test patterns for delay-based side-channel analysis. Yangdi Lyu, Prabhat Mishra 0001 |
DATE | 2 |
| 2020 | Test Generation using Reinforcement Learning for Delay-based Side-Channel AnalysisabstractReliability and trustworthiness are dominant factors in designing System-on-Chips (SoCs) for a variety of applications. Malicious implants, such as hardware Trojans, can lead to undesired information leakage or system malfunction. To ensure trustworthy computing, it is critical to develop efficient Trojan detection techniques. While existing delay-based side-channel analysis is promising, it is not effective due to two fundamental limitations: (i) The difference in path delay between the golden design and Trojan inserted design is negligible compared with environmental noise and process variations. (ii) Existing approaches rely on manually crafted rules for test generation, and require a large number of simulations, making it impractical for industrial designs. In this paper, we propose a novel test generation method using reinforcement learning for delay-based Trojan detection. This paper makes three important contributions. Zhixin Pan, Jennifer Sheldon, Prabhat Mishra 0001 |
ICCAD | 3 |
| 2020 | Hardware-Assisted Malware Detection using Explainable Machine LearningabstractMalicious software, popularly known as malware, is widely acknowledged as a serious threat to modern computing systems. Software-based solutions, such as anti-virus software, are not effective since they rely on matching patterns that can be easily fooled by carefully crafted malware with obfuscation or other deviation capabilities. While recent malware detection methods provide promising results through effective utilization of hardware features, the detection results cannot be interpreted in a meaningful way. In this paper, we propose a hardware-assisted malware detection framework using explainable machine learning. This paper makes three important contributions. First, we theoretically establish that our proposed method can provide interpretable explanation of classification results to address the challenge of transparency. Next, we show that the explainable outcome can lead to accurate localization of malicious behaviors. Finally, experimental evaluation using a wide variety of realworld malware benchmarks demonstrates that our framework can produce accurate and human-understandable malware detection results with provable guarantees. Zhixin Pan, Jennifer Sheldon, Prabhat Mishra 0001 |
ICCD | 3 |
| 2020 | Special Session: Impact of Noise on Quantum Algorithms in Noisy Intermediate-Scale Quantum SystemsabstractA major challenge in realizing efficient and powerful quantum algorithms is quantum noise. Quantum noise itself is a sophisticated topic that is not seen in the classical domain. In this paper, we explore the impact of noise on quantum algorithms in Noisy Intermediate-Scale Quantum (NISQ) systems. This paper first introduces the origins of quantum noise. Next, it proposes a common treatment to simplify the view of quantum noise. Finally, it presents a case study to investigate the impact of noise on quantum Fourier transform algorithm. Daniel Volya, Prabhat Mishra 0001 |
ICCD | 2 |
| 2020 | SECTAR: Secure NoC using Trojan Aware RoutingabstractSystem-on-Chips (SoCs) are designed using different Intellectual Property (IP) blocks from multiple third-party vendors to reduce design cost while meeting aggressive time-to-market constraints. Designing trustworthy SoCs need to address the increasing concerns related to supply-chain security vulnerabilities. Malicious implants on IPs, such as Hardware Trojans (HTs) are one of the significant security threats in designing trustworthy SoCs. It is a major challenge to detect Trojans in complex multi-processor SoCs using conventional pre- and post-silicon validation methodologies. Packet-based Network-on-Chip (NoC) is a widely used solution for on-chip communication between IPs in complex SoCs. The focus of this paper is to enable trusted NoC communication in the presence of potentially untrusted IPs. This paper makes three key contributions. (1) We model an HT in NoC router that activates misrouting of the packets to initiate a denial of service, delay of service, and injection suppression. (2) We propose a dynamic shielding technique that isolates the identified HT infected IP. (3) We present a secure routing algorithm to bypass the HT infected NoC router. Experimental results on HT infected NoC demonstrate that the proposed method reduces effective average packet latency by 38% in real benchmarks and 48% in synthetic traffic patterns. Our method also increases throughput and reduces effective average deflected packet latency by 62% in real benchmarks and 97% in synthetic traffic patterns. Manju Rajan, Abhijit Das 0002, John Jose, Prabhat Mishra 0001 |
NOCS | 4 |
| 2020 | Real-Time Detection and Localization of Distributed DoS Attacks in NoC-Based SoCsabstractNetwork-on-chip (NoC) is widely employed by multicore system-on-chip (SoC) architectures to cater to their communication requirements. Increasing NoC complexity coupled with its widespread usage has made it a focal point of potential security attacks. Distributed denial-of-service (DDoS) is one such attack that is caused by malicious intellectual property (IP) cores flooding the network with unnecessary packets causing significant performance degradation through NoC congestion. In this article, we propose an efficient framework for real-time detection and localization of DDoS attacks. This article makes three important contributions. We propose a real-time and lightweight DDoS attack detection technique for NoC-based SoCs by monitoring packets to detect any violations. Once a potential attack has been flagged, our approach is also capable of localizing the malicious IPs using the latency data in the NoC routers. The applications are statically profiled during design time to determine communication patterns. These patterns are then used for real-time detection and localization of DDoS attacks. We have evaluated the effectiveness of our approach against different NoC topologies and architecture models using both real benchmarks and synthetic traffic patterns. Our experimental results demonstrate that our proposed approach is capable of real-time detection and localization of DDoS attacks originating from multiple malicious IPs in NoC-based SoCs. Subodha Charles, Yangdi Lyu, Prabhat Mishra 0001 |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 3 |
| 2020 | Reconfigurable Network-on-Chip Security ArchitectureabstractGrowth of the Internet-of-things has led to complex system-on-chips (SoCs) being used in the edge devices in IoT applications. The increased complexity is demanding designers to consider several critical factors, such as dynamic requirement changes, long application life, mass production, and tight time-to-market deadlines. These requirements lead to more complex security concerns. SoC manufacturers outsource some of the intellectual property cores integrated on the SoC to untrusted third-party vendors. The untrusted intellectual properties can contain malicious implants, which can launch attacks using the resources provided by the on-chip interconnection network, commonly known as the network-on-chip (NoC). Existing efforts on securing NoC have considered lightweight encryption, authentication, and other attack detection mechanisms such as denial-of-service and buffer overflows. Unfortunately, these approaches focus on designing statically optimized security solutions. As a result, they are not suitable for many IoT systems with long application life and dynamic requirement changes. There is a critical need to design reconfigurable security architectures that can be dynamically tuned based on changing requirements. In this article, we propose a tier-based reconfigurable security architecture that can adapt to different use-case scenarios. We explore how to design an efficient reconfigurable architecture that can support three popular NoC security mechanisms (encryption, authentication, and denial-of-service attack detection and localization) and implement suitable dynamic reconfiguration techniques. We evaluate our proposed framework by running standard benchmarks enabling different tiers of security and provide a comprehensive analysis of how different levels of security can affect application performance, energy efficiency, and area overhead. Subodha Charles, Prabhat Mishra 0001 |
ACM Trans. Design Autom. Electr. Syst. | 2 |
| 2019 | The Metric Matters: The Art of Measuring Trust in ElectronicsabstractElectronic hardware trust is an emerging concern for all stakeholders in the semiconductor industry. Trust issues in electronic hardware span all stages of its life cycle - from creation of intellectual property (IP) blocks to manufacturing, test and deployment of hardware components and all abstraction levels - from chips to printed circuit boards (PCBs) to systems. The trust issues originate from a horizontal business model that promotes reliance of third-party untrusted facilities, tools, and IPs in the hardware life cycle. Today, designers are tasked with verifying the integrity of third-party IPs before incorporating them into system-on-chip (SoC) designs. Existing trust metric frameworks have limited applicability since they are not comprehensive. They capture only a subset of vulnerabilities such as potential vulnerabilities introduced through design mistakes and CAD tools, or quantify features in a design that target a particular Trojan model. Therefore, current practice uses ad-hoc security analysis of IP cores. In this paper, we propose a vector-based comprehensive coverage metric that quantifies the overall trust of an IP considering both vulnerabilities and direct malicious modifications. We use a variable weighted sum of a design's functional coverage, structural coverage, and asset coverage to assess an IP's integrity. Designers can also effectively use our trust metric to compare the relative trustworthiness of functionally equivalent third-party IPs. To demonstrate the applicability and usefulness of the proposed metric, we utilize our trust metric on Trojan-free and Trojan-inserted variants of an IP. Our results demonstrate that we are able to successfully distinguish between trusted and untrusted IPs. Jonathan Cruz 0001, Prabhat Mishra 0001, Swarup Bhunia |
DAC | 2 |
| 2019 | Real-time Detection and Localization of DoS Attacks in NoC based SoCsabstractNetwork-on-Chip (NoC) is widely employed by multi-core System-on-Chip (SoC) architectures to cater to their communication requirements. The increased usage of NoC and its distributed nature across the chip has made it a focal point of potential security attacks. Denial-of-Service (DoS) is one such attack that is caused by a malicious intellectual property (IP) core flooding the network with unnecessary packets causing significant performance degradation through NoC congestion. In this paper, we propose a lightweight and real-time DoS attack detection mechanism. Once a potential attack has been flagged, our approach is also capable of localizing the malicious IP using latency data gathered by NoC components. Experimental results demonstrate the effectiveness of our approach with timely attack detection and localization while incurring minor area and power overhead (less than 6% and 4%, respectively). Subodha Charles, Yangdi Lyu, Prabhat Mishra 0001 |
DATE | 3 |
| 2019 | Automated Activation of Multiple Targets in RTL Models using Concolic TestingabstractSimulation is widely used for validation of Register-Transfer-Level (RTL) models. While simulating with millions of random (or constrained-random) tests can cover majority of the targets (functional scenarios), the number of remaining targets can still be huge (hundreds or thousands) in case of today's industrial designs. Prior work on directed test generation using concolic testing can cover only one target at a time. A naive extension of prior work to activate the remaining targets would be infeasible due to wasted effort in multiple overlapping searches. In this paper, we propose an automated test generation technique for activating multiple targets in RTL models using concolic testing. This paper makes three important contributions. First, it efficiently prunes the targets that can be covered by the tests generated for activating the other targets. Next, it minimizes the overlapping searches while trying to generate tests for activating multiple targets. Finally, our approach effectively utilizes clustering of related targets as well as common path sharing between the targets in the same cluster to drastically reduce the test generation time. Experimental results demonstrate that our approach significantly outperforms the existing methods in terms of overall coverage (up to 5X, 1.2X on average) as well as test generation time (up to 146X, 80X on average). Yangdi Lyu, Alif Ahmed, Prabhat Mishra 0001 |
DATE | 3 |
| 2019 | Efficient Test Generation for Trojan Detection using Side Channel AnalysisabstractDetection of hardware Trojans is vital to ensure the security and trustworthiness of System-on-Chip (SoC) designs. Side-channel analysis is effective for Trojan detection by analyzing various side-channel signatures such as power, current and delay. In this paper, we propose an efficient test generation technique to facilitate side-channel analysis utilizing dynamic current. While early work on current-aware test generation has proposed several promising ideas, there are two major challenges in applying it on large designs: (i) the test generation time grows exponentially with the design complexity, and (ii) it is infeasible to detect Trojans since the side-channel sensitivity is marginal compared to the noise and process variations. Our proposed work addresses both challenges by effectively exploiting the affinity between the inputs and rare (suspicious) nodes. We formalize the test generation problem as a searching problem and solve the optimization using genetic algorithm. The basic idea is to quickly find the profitable test patterns that can maximize switching in the suspicious regions while minimize switching in the rest of the circuit. Our experimental results demonstrate that we can drastically improve both the side-channel sensitivity (30x on average) and time complexity (4.6x on average) compared to the state-of-the-art test generation techniques. Yangdi Lyu, Prabhat Mishra 0001 |
DATE | 2 |
| 2019 | Automated Test Generation for Debugging Multiple Bugs in Arithmetic CircuitsabstractOptimized and custom arithmetic circuits are widely used in embedded systems such as multimedia applications, cryptography systems, signal processing and console games. Debugging of arithmetic circuits is a challenge due to increasing complexity coupled with non-standard implementations. Existing algebraic rewriting techniques produce a remainder to indicate the presence of a potential bug. However, bug localization remains a major bottleneck. Simulation-based validation using random or constrained-random tests are not effective for complex arithmetic circuits due to bit-blasting. In this paper, we present an automated test generation and bug localization technique for debugging arithmetic circuits. This paper makes four important contributions. We propose an automated approach for generating directed tests by suitable assignments of input variables to make the remainder non-zero. The generated tests are guaranteed to activate bugs. We also propose an automatic bug fixing technique by utilizing the patterns of the remainder terms as well as by analyzing the regions activated by the generated tests to detect and correct the error(s). We also propose an efficient debugging algorithm that can handle multiple dependent as well as independent bugs. Finally, our proposed framework, consisting of directed test generation, bug localization and bug correction, is fully automated. In other words, our framework is capable of producing a corrected implementation of arithmetic circuits without any manual intervention. Our experimental results demonstrate that the proposed approach can be used for automated debugging of large and complex arithmetic circuits. Farimah Farahmandi, Prabhat Mishra 0001 |
IEEE Trans. Computers | 2 |
| 2019 | Vulnerability-Aware Energy Optimization for Reconfigurable Caches in Multitasking SystemsabstractCache vulnerability due to soft errors is one of the reliability concerns in embedded systems. Dynamic reconfiguration techniques are widely studied for improving cache energy without considering the implications of cache vulnerability. Maintaining a useful data longer in the cache can be beneficial for energy improvement due to reduction in miss rates, however, longer data retention negatively impacts the vulnerability due to soft errors. This paper studies the tradeoff between energy efficiency improvement and reduction in cache vulnerability during cache reconfiguration. We propose a heuristic approach for both intertask and intratask cache reconfiguration in multitasking systems. Experimental results demonstrate that our proposed approach can significantly improve both vulnerability (25% on average) and energy efficiency (21% on average) for data cache without violating real-time constraints. Yuanwen Huang, Prabhat Mishra 0001 |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 2 |
| 2019 | Directed Test Generation for Validation of Cache Coherence ProtocolsabstractComputing systems utilize multicore processors with complex cache coherence protocols to meet the increasing need for performance and energy improvement. It is a major challenge to verify the correctness of a cache coherence protocol since the number of reachable states grows exponentially with the number of cores. In this paper, we propose an efficient test generation technique, which can be used to achieve full state and transition coverage in simulation-based verification for a wide variety of cache coherence protocols. Based on effective analysis of the state space structure, our method can generate more efficient test sequences (50% shorter) on-the-fly compared with tests generated by BFS. While our on-the-fly method can reduce the numbers of required tests by half, it can still be impractical to verify all possible transitions in the presence of large number of cores. We propose scalable on-the-fly test generation techniques using quotient state space. The proposed approach guarantees selection of important transitions by utilizing equivalence classes, and omits only similar transitions. Our experimental results demonstrate that our proposed approaches can efficiently tradeoff between transition coverage and validation effort. Yangdi Lyu, Xiaoke Qin, Mingsong Chen 0001, Prabhat Mishra 0001 |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 4 |
| 2019 | Security-Aware FSM Design Flow for Identifying and Mitigating Vulnerabilities to Fault AttacksabstractThe security of a system-on-chip (SoC) can be compromised by exploiting the vulnerabilities of the finite state machines (FSMs) in the SoC controller modules through fault injection attacks. These vulnerabilities may be unintentionally introduced by traditional FSM design practices or by CAD tools during synthesis. In this paper, we first analyze how the vulnerabilities in an FSM can be exploited by fault injection attacks. Then, we propose a security-aware FSM design flow for ASIC designs to mitigate them and prevent fault attacks on FSM. Our proposed FSM design flow starts with a security-aware encoding scheme which makes the FSM resilient against fault attacks. However, the vulnerabilities introduced by the CAD tools cannot be addressed by encoding schemes alone. To analyze for such vulnerabilities, we develop a novel technique named analyzing vulnerabilities in FSM. If any vulnerability exists, we propose a secure FSM architecture to address the issue. In this paper, we mainly focus on setup-time violation-based fault attacks which pose a serious threat on FSMs; though our proposed flow works for advanced laser-based fault attacks as well. We compare our proposed secure FSM design flow with traditional FSM design practices in terms of cost, performance, and security. We show that our FSM design flow ensures security while having a negligible impact on cost and performance. Adib Nahiyan, Farimah Farahmandi, Prabhat Mishra 0001, Domenic Forte, Mark Tehranipoor |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 3 |
| 2019 | Cache Reconfiguration Using Machine Learning for Vulnerability-aware Energy OptimizationabstractDynamic cache reconfiguration has been widely explored for energy optimization and performance improvement for single-core systems. Cache partitioning techniques are introduced for the shared cache in multicore systems to alleviate inter-core interference. While these techniques focus only on performance and energy, they ignore vulnerability due to soft errors. In this article, we present a static profiling based algorithm to enable vulnerability-aware energy-optimization for real-time multicore systems. Our approach can efficiently search the space of cache configurations and partitioning schemes for energy optimization while task deadlines and vulnerability constraints are satisfied. A machine learning technique has been employed to minimize the static profiling time without sacrificing the accuracy of results. Our experimental results demonstrate that our approach can achieve 19.2% average energy savings compared with the base configuration, while drastically reducing the vulnerability (49.3% on average) compared to state-of-the-art techniques. Furthermore, the machine learning technique enabled more than 10x speedup in static profiling time with a negligible prediction error of 3%. Alif Ahmed, Yuanwen Huang, Prabhat Mishra 0001 |
ACM Trans. Embed. Comput. Syst. | 3 |
| 2019 | Efficient Cache Reconfiguration Using Machine Learning in NoC-Based Many-Core CMPsabstractDynamic cache reconfiguration (DCR) is an effective technique to optimize energy consumption in many-core architectures. While early work on DCR has shown promising energy saving opportunities, prior techniques are not suitable for many-core architectures since they do not consider the interactions and tight coupling between memory, caches, and network-on-chip (NoC) traffic. In this article, we propose an efficient cache reconfiguration framework in NoC-based many-core architectures. The proposed work makes three major contributions. First, we model a distributed directory based many-core architecture similar to Intel Xeon Phi architecture. Next, we propose an efficient cache reconfiguration framework that considers all significant components, including NoC, caches, and main memory. Finally, we propose a machine learning--based framework that can reduce the exploration time by an order of magnitude with negligible loss in accuracy. Our experimental results demonstrate 18.5% energy savings on average compared to base cache configuration. Subodha Charles, Alif Ahmed, Ümit Y. Ogras, Prabhat Mishra 0001 |
ACM Trans. Design Autom. Electr. Syst. | 4 |
| 2019 | Editorial TVLSI Positioning - Continuing and Accelerating an Upward TrajectoryabstractI. VLSI Systems: A Glance Into The Last Decades Since their inception in 1970s, VLSI systems have enabled several new technological capabilities and made them accessible to an unceasingly wider range of users, reaching a scale that has been exponentially increasing over the decades[1](seeFig. 1). Relentless integration of more complex systems has driven such remarkable evolution, as made possible by the inexorable miniaturization. As shown inFig. 1, more functionality has been crammed in a consistently smaller form factor, as exemplified by the physical volume shrinking of computers by 100 X/decade[2],[3]. At the same time, the energy per task has been decreasing at 10–100 X/decade, as shown inFig. 2, for several systems and system-on-chip subsystems[4]. This allowed packing more capabilities into the same power envelope, as generally observed in the electronic systems, even before the advent of the integrated circuit[5]. Massimo Alioto, Magdy S. Abadir, Tughrul Arslan, Chirn Chye Boon, Andreas Peter Burg, Chip-Hong Chang, Meng-Fan Chang, Yao-Wen Chang, Poki Chen, Pasquale Corsonello, Paolo Crovetti, Shiro Dosho, Rolf Drechsler, Ibrahim M. Elfadel, Ruonan Han 0001, Masanori Hashimoto, Chun-Huat Heng, Deuk Hyoun Heo, Tsung-Yi Ho, Houman Homayoun, Yuh-Shyan Hwang, Ajay Joshi, Rajiv V. Joshi, Tanay Karnik, Chulwoo Kim, Tony Tae-Hyoung Kim, Jaydeep P. Kulkarni, Volkan Kursun, Yoonmyung Lee, Hai Li 0001, Huawei Li 0001, Prabhat Mishra 0001, Baker Mohammad, Mehran Mozaffari Kermani, Makoto Nagata, Koji Nii, Partha Pratim Pande, Bipul Chandra Paul, Vasilis F. Pavlidis, José Pineda de Gyvez, Ioannis Savidis, Patrick Schaumont, Fabio Sebastiano, Anirban Sengupta 0003, Mingoo Seok, Mircea R. Stan, Mark Tehranipoor, Aida Todri, Marian Verhelst, Valerio Vignoli, Xiaoqing Wen, Jiang Xu 0001, Wei Zhang 0012, Zhengya Zhang, Jun Zhou 0017, Mark Zwolinski, Stacey Weber |
IEEE Trans. Very Large Scale Integr. Syst. | 32 |
| 2019 | Guest Editorial: Special Section on Autonomous Intelligence for Security and Privacy AnalyticsabstractWe interact with a wide variety of computing systems in our daily life. These computing systems are often connected through a network to provide a wide array of services. Depending on our specific circumstances, our interactions can be with embedded and cyber-physical systems (CPSs) or Internet-of-Things (IoT) devices. While these devices vary in terms of form factors, hardware–software integration, and energy constraints, they have one commonality—security and privacy are the primary design considerations. These systems collect and analyze sensitive data, which may include our personal, financial, as well as health information on a regular basis. As a result, the existing academic and industrial efforts have focused on designing systems with security and privacy in mind. Given the complexity of these systems and the diversity of the potential attacks, machine learning (ML) has become an attractive solution for security and privacy analytics. Prabhat Mishra 0001, Debdeep Mukhopadhyay, Swarup Bhunia |
IEEE Trans. Very Large Scale Integr. Syst. | 1 |
| 2018 | Directed test generation using concolic testing on RTL modelsabstractFunctional validation is one of the most time consuming steps in System-on-Chip (SoC) design methodology. In today's industrial practice, simulating designs using billions of random or constrained-random tests can lead to high functional coverage. However, it is hard to cover the remaining small fraction of corner cases and rare functional scenarios. While formal methods are promising in such cases, it is infeasible to apply them on large designs. In this paper, we propose a fully automated and scalable approach for generating directed tests using concolic testing of RTL models. While application of concolic testing on hardware designs has shown some promising results, existing approaches are tuned for improving overall coverage, rather than covering a specific target. We developed a Control Flow Graph (CFG) assisted directed test generation method that can efficiently generate a test to activate a given target. Our experimental results demonstrate that our approach is both efficient and scalable compared to the state-of-the-art test generation methods. Alif Ahmed, Farimah Farahmandi, Prabhat Mishra 0001 |
DATE | 3 |
| 2018 | An automated configurable Trojan insertion framework for dynamic trust benchmarksabstractMalicious hardware modification, also known as hardware Trojan attack, has emerged as a serious security concern for electronic systems. Such attacks compromise the basic premise of hardware root of trust. Over the past decade, significant research efforts have been directed to carefully analyze the trust issues arising from hardware Trojans and to protect against them. This vast body of work often needs to rely on well-defined set of trust benchmarks that can reliably evaluate the effectiveness of the protection methods. In recent past, efforts have been made to develop a benchmark suite to analyze the effectiveness of pre-silicon Trojan detection and prevention methodologies. However, there are only a limited number of Trojan inserted benchmarks available. Moreover, there is an inherent bias as the researcher is aware of Trojan properties such as location and trigger condition since the current benchmarks are static. In order to create an unbiased and robust benchmark suite to evaluate the effectiveness of any protection technique, we have developed a comprehensive framework of automatic hardware Trojan insertion. Given a netlist, the framework will automatically generate a design with single or multiple Trojan instances based user-specified Trojan properties. It allows a wide variety of configurations, such as the type of Trojan, Trojan activation probability, number of triggers, and choice of payload. The tool ensures that the inserted Trojan is a valid one and allow for provisions to optimize the Trojan footprint (area and switching). Experiments demonstrate that a state-of-the-art Trojan detection technique provides poor efficacy when using benchmarks generated by our tool. This tool is available for download from http://www.trust-hub.org/. Jonathan Cruz 0001, Yuanwen Huang, Prabhat Mishra 0001, Swarup Bhunia |
DATE | 3 |
| 2018 | Scalable Hardware Trojan Activation by Interleaving Concrete Simulation and Symbolic ExecutionabstractIntellectual Property (IP) based System-on-Chip (SoC) design is a widely used practice today. The IPs gathered from third-party vendors may not be trustworthy since they may contain malicious implants (hardware Trojans). To avoid the detection of the Trojan, adversaries usually hide it under rare branches or rare assignments triggered under extremely rare input sequences. Due to exponential input space complexity, state-of-the-art constrained-random test generation methods are not suitable for activating these rare scenarios. While existing model checking based directed test generation approaches are promising, they are not capable of generating tests for large RTL designs due to the capacity restrictions of formal methods. In this paper, we propose an automated and scalable test generation approach for activation of hardware Trojans in RTL designs. This paper makes three important contributions. First, it provides a scalable test generation framework by effective utilization of symbolic execution and concrete simulation. Next, it is a fully automated approach for generating directed tests for activating rare branches and rare assignments. Finally, our experimental results demonstrate that the generated tests are able to activate hard-to-cover Trojans in large and complex RTL benchmarks. Alif Ahmed, Farimah Farahmandi, Yousef Iskander, Prabhat Mishra 0001 |
ITC | 4 |
| 2018 | Exploration of Memory and Cluster Modes in Directory-Based Many-Core CMPsabstractNetworks-on-chip have become the standard interconnect solution to address the communication requirements of many-core chip multiprocessors. It is well-known that network performance and power consumption depend critically on the traffic load. The network traffic itself is a function of not only the application, but also the cache coherence protocol, and memory controller/directory locations. Communication between the distributed directory to memory can introduce hotspots, since the number of memory controllers is much smaller than the number of cores. Therefore, it is critical to account for directorymemory communication, and model them accurately in architecture simulators. This paper analyzes the impact of directorymemory traffic and different memory and cluster modes on the NoC traffic and system performance. We demonstrate that unrealistic models in a widely used multiprocessor simulator produce misleading power and performance predictions. Finally, we evaluate different memory and cluster modes supported by Intel Xeon-Phi processors, and validate our models on four different cache coherence protocols. Subodha Charles, Chetan Arvind Patil, Ümit Y. Ogras, Prabhat Mishra 0001 |
NOCS | 4 |
| 2018 | Scalable Test Generation for Trojan Detection Using Side Channel AnalysisabstractHardware Trojan detection has emerged as a critical challenge to ensure security and trustworthiness of integrated circuits. A vast majority of research efforts in this area has utilized side-channel analysis for Trojan detection. Functional test generation for logic testing is a promising alternative but it may not be helpful if a Trojan cannot be fully activated or the Trojan effect cannot be propagated to the observable outputs. Side-channel analysis, on the other hand, can achieve significantly higher detection coverage for Trojans of all types/sizes, since it does not require activation/propagation of an unknown Trojan. However, they have often limited effectiveness due to poor detection sensitivity under large process variations and small Trojan footprint in side-channel signature. In this paper, we address this critical problem through a novel side-channel-aware test generation approach, based on a concept of multiple excitation of rare switching (MERS), that can significantly increase Trojan detection sensitivity. This paper makes several important contributions: 1) it presents in detail a scalable statistical test generation method, which can generate high-quality test set for creating high relative activity in arbitrary Trojan instances; 2) it analyzes the effectiveness of generated test set in terms of Trojan coverage; and 3) it describes two judicious reordering methods that can further tune the test set and greatly improve the side channel sensitivity. Simulation results demonstrate that the tests generated by MERS can significantly increase the Trojans sensitivity, thereby making Trojan detection effective using side-channel analysis. Yuanwen Huang, Swarup Bhunia, Prabhat Mishra 0001 |
IEEE Trans. Inf. Forensics Secur. | 3 |
| 2017 | Trojan localization using symbolic algebraabstractGrowing reliance on reusable hardware Intellectual Property (IP) blocks, severely affects the security and trustworthiness of System-on-Chips (SoCs) since untrusted third-party vendors may deliberately insert malicious components to incorporate undesired functionality. Malicious implants may also work as hidden backdoor and leak protected information. In this paper, we propose an automated approach to identify untrustworthy IPs and localize malicious functional modifications (if any). The technique is based on extracting polynomials from gate-level implementation of the untrustworthy IP and comparing them with specification polynomials. The proposed approach is applicable when the specification is available. Our approach is scalable due to manipulation of polynomials instead of BDD-based analysis used in traditional equivalence checking techniques. Experimental results using Trust-HUB benchmarks demonstrate that our approach improves both localization and test generation efficiency by several orders of magnitude compared to the state-of-the-art Trojan detection techniques. Farimah Farahmandi, Yuanwen Huang, Prabhat Mishra 0001 |
ASP-DAC | 3 |
| 2017 | Cost-effective analysis of post-silicon functional coverage eventsabstractPost-silicon validation is a major challenge due to the combined effects of debug complexity and observability constraints. Assertions as well as a wide variety of checkers are used in pre-silicon stage to monitor certain functional scenarios. Pre-silicon checkers can be synthesized to coverage monitors in order to capture the coverage of certain events and improve the observability during post-silicon debug. Synthesizing thousands of coverage monitors can introduce unacceptable area and energy overhead. On the other hand, absence of coverage monitors would negatively impact post-silicon coverage analysis. In this paper, we propose a framework for cost-effective post-silicon coverage analysis by identifying hard-to-detect events coupled with trace-based coverage analysis. This paper makes three major contributions. We propose a method to utilize existing debug infrastructure to enable coverage analysis in the absence of synthesized coverage monitors. This analysis enables us to identify a small percentage of coverage monitors that need to be synthesized in order to provide a trade-off between observability and design overhead. To improve the observability further, we also present an observability-aware trace signal selection algorithm that gives priority to signals associated with important coverage monitors. Our experimental results demonstrate that an effective combination of coverage monitor selection and trace analysis can maintain the debugging observability with drastic reduction (up to 10 times) in the required coverage monitors. Farimah Farahmandi, Ronny Morad, Avi Ziv, Ziv Nevo, Prabhat Mishra 0001 |
DATE | 5 |
| 2017 | QUEBS: Qualifying Event Based Search in Concolic Testing for Validation of RTL ModelsabstractInput vector generation is an important step during validation and debugging of hardware designs. Validation using random and directed random tests are widely used today. However, these methods can lead to unacceptable functional coverage under tight deadlines. Concolic testing is a semi-formal method to address this issue. It combines concrete simulation guided by symbolic execution. Application of concolic testing in hardware domain is still in its infancy due to the lack of effective traversal strategies. In this paper, we present Qualifying Event Based Search (QUEBS) heuristic for concolic testing. During exhaustive concolic testing, same branch may be selected many times for traversal. Our heuristic limits the number of times a branch can be selected. By preventing repeated selection, it facilitates wider coverage within limited time. Also, whenever a previously uncovered branch is encountered, this limit is relaxed to permit thorough exploration of the newly reached area. Our experimental results demonstrate that this approach provides better branch coverage than state-of-the-art test generation methods in a given time budget. To further improve the performance of QUEBS, we provide two optimization techniques - unsolvable branch elimination and incremental solving by context reuse. Alif Ahmed, Prabhat Mishra 0001 |
ICCD | 2 |
| 2017 | Automated Debugging of Arithmetic Circuits Using Incremental Gröbner Basis ReductionabstractSymbolic algebra is a promising approach to verify large and complex arithmetic circuits. Existing algebraic-based verification methods generate a remainder to indicate buggy implementation. The remainder is beneficial for debugging of the faulty implementation since it can be used for automated test generation, bug localization, and bug correction. However, existing equivalence checking approaches are not scalable and lead to explosion in size of the remainder when the design is faulty. To make the matters worse, the location of the bug can also lead to the explosion in the number of remainder terms. In this paper, we propose an incremental equivalence checking method to address the scalability challenges by solving the verification problem in the increasing order of design's input complexity. Our proposed approach makes two important contributions. It is able to generate smaller and compact remainders for large designs. Our proposed incremental debugging is capable of localizing and correcting hard-to-detect bugs irrespective of their location in the design. Experimental results demonstrate that our approach can efficiently debug most difficult bugs in large arithmetic circuits when the state-of-the-art methods fail. Farimah Farahmandi, Prabhat Mishra 0001 |
ICCD | 2 |
| 2017 | FSM Anomaly Detection Using Formal AnalysisabstractFinite state machines (FSMs) control the functionality of the overall design. Any deviation from the specified FSM behavior can endanger the trustworthiness of the design. This is a critical concern when an FSM is responsible for controlling the usage or propagation of protected information (e.g. secret keys) in a secure component. FSM vulnerabilities can be created by a rogue designer or an attacker by inserting hardware Trojans in the FSM implementation. The vulnerability can also be introduced unintentionally by a CAD tool (e.g., when a synthesis tool is trying to optimize a gate-level netlist). In this paper, we present an efficient formal analysis framework based on symbolic algebra to find FSM vulnerabilities. The proposed method tries to find inconsistencies between the specification and FSM implementation through manipulation of respective polynomials. Security properties (such as a safe transition to a protected state) are derived using specification polynomials and verified against implementation polynomials. In a case of a failure, the vulnerability is reported. While existing methods can verify legal transitions, our approach tries to solve the important and non-trivial problem of detecting illegal accesses to the design states (e.g., protected states). We demonstrated the merit of our proposed method by detecting the vulnerabilities in various FSM designs, while state-of-the-approaches failed to identify the security flaws. Farimah Farahmandi, Prabhat Mishra 0001 |
ICCD | 2 |
| 2017 | Vulnerability-Aware Energy Optimization Using Reconfigurable Caches in Multicore SystemsabstractDynamic cache reconfiguration has been widely explored for energy optimization and performance improvement for single-core systems. Cache partitioning techniques are introduced for the shared cache in multicore systems to alleviate inter-core interference. While these techniques focus only on performance and energy, they ignore vulnerability due to soft errors. In this paper, we present a static profiling based algorithm to enable vulnerability-aware energy-optimization for real-time multicore systems. Our approach can efficiently search the space of cache configurations and partitioning schemes for energy optimization while task deadlines and vulnerability constraints are satisfied. Our experimental results demonstrate that our approach can achieve 19.2% average energy savings compared with the base configuration, while drastically reduce the vulnerability (49.3% on average) compared to state-of-the-art techniques. Yuanwen Huang, Prabhat Mishra 0001 |
ICCD | 2 |
| 2017 | DyPO: Dynamic Pareto-Optimal Configuration Selection for Heterogeneous MpSoCsabstractModern multiprocessor systems-on-chip (MpSoCs) offer tremendous power and performance optimization opportunities by tuning thousands of potential voltage, frequency and core configurations. As the workload phases change at runtime, different configurations may become optimal with respect to power, performance or other metrics. Identifying the optimal configuration at runtime is infeasible due to the large number of workloads and configurations. This paper proposes a novel methodology that can find the Pareto-optimal configurations at runtime as a function of the workload. To achieve this, we perform an extensive offline characterization to find classifiers that map performance counters to optimal configurations. Then, we use these classifiers and performance counters at runtime to choose Pareto-optimal configurations. We evaluate the proposed methodology by maximizing the performance per watt for 18 single- and multi-threaded applications. Our experiments demonstrate an average increase of 93%, 81% and 6% in performance per watt compared to the interactive, ondemand and powersave governors, respectively. Ujjwal Gupta, Chetan Arvind Patil, Ganapati Bhat, Prabhat Mishra 0001, Ümit Y. Ogras |
ACM Trans. Embed. Comput. Syst. | 4 |
| 2017 | EditorialabstractAs I start my second two-year term (2017–2018) as the Editor-in-Chief (EIC) of the IEEE Transactions on Very Large Scale Integration Systems (TVLSI), I wish the TVLSI readership a very happy new year and continued professional success. It gives me great pleasure to report on the state of the journal and our performance metrics. Over the past two years, TVLSI has seen a healthy increase in the number of submissions—from 687 in 2014 to 770 in 2015, and at the time of writing of this editorial, we are at 760 submissions for 2016. We expect the number of submissions for 2016 to cross 800 before the end of the year. TVLSI, therefore, continues to be the premier archival journal for university researchers and industry practitioners in the broad area of VLSI system design. Krishnendu Chakrabarty, Massimo Alioto, Bevan M. Baas, Chirn Chye Boon, Meng-Fan Chang, Naehyuck Chang, Yao-Wen Chang, Chip-Hong Chang, Shih-Chieh Chang 0001, Poki Chen, Masud H. Chowdhury, Pasquale Corsonello, Ibrahim M. Elfadel, Said Hamdioui, Masanori Hashimoto, Tsung-Yi Ho, Houman Homayoun, Yuh-Shyan Hwang, Rajiv V. Joshi, Tanay Karnik, Mehran Mozaffari Kermani, Chulwoo Kim, Jaydeep P. Kulkarni, Eren Kursun, Erik Larsson, Hai Li 0001, Huawei Li 0001, Patrick P. Mercier, Prabhat Mishra 0001, Makoto Nagata, Arun Natarajan 0001, Koji Nii, Partha Pratim Pande, Ioannis Savidis, Mingoo Seok, Sheldon X.-D. Tan, Mark Tehranipoor, Aida Todri, Miroslav N. Velev, Xiaoqing Wen, Jiang Xu 0001, Wei Zhang 0012, Zhengya Zhang, Stacey Weber |
IEEE Trans. Very Large Scale Integr. Syst. | 30 |
| 2017 | Automatic Code Converter Enhanced PCH Framework for SoC Trust VerificationabstractThe wide usage of hardware intellectual property cores from untrusted vendors has raised security concerns for system designers. Existing solutions for functionality testing and verification do not usually consider the presence of malicious logic in hardware. Formal methods provide powerful solutions for detecting malicious behaviors in hardware. However, they suffer from scalability issues and cannot be easily used for large-scale computing systems. To alleviate the scalability challenge, we propose a new integrated formal verification framework to evaluate the trust of system-on-chip (SoC) constructed from untrusted third-party hardware resources. This framework combines an automated model checker with an interactive theorem prover to reduce the time for proving the system-level security properties of SoCs. Another factor contributing to the scalability issue is the effort required for manual conversion of the hardware design from register transfer level (RTL) code to a domain-specific language prior to verification. Consequently, we develop an automatic code converter for translating VHSIC hardware description language (VHDL) to Formal-HDL, which is a domain specific language for representing hardware designs in the language of Coq. To demonstrate the effectiveness of our integrated verification framework and automated code conversion tool, we evaluate a vulnerable program executed on a bare metal LEON3 SPARC V8 processor and prove system security with considerable reduction in verification effort. Xiaolong Guo 0001, Raj Gautam Dutta, Prabhat Mishra 0001, Yier Jin |
IEEE Trans. Very Large Scale Integr. Syst. | 3 |
| 2017 | Postsilicon Trace Signal Selection Using Machine Learning TechniquesabstractA key problem in postsilicon validation is to identify a small set of traceable signals that are effective for debug during silicon execution. Structural analysis used by traditional signal selection techniques leads to a poor restoration quality. In contrast, simulation-based selection techniques provide superior restorability but incur significant computation overhead. In this paper, we propose an efficient signal selection technique using machine learning to take advantage of simulation-based signal selection while significantly reducing the simulation overhead. The basic idea is to train a machine learning framework with a few simulation runs and utilize its effective prediction capability (instead of expensive simulation) to identify beneficial trace signals. Specifically, our approach uses: (1) bounded mock simulations to generate training vectors for the machine learning technique and (2) a compound search-space exploration approach to identify the most profitable signals. Experimental results indicate that our approach can improve restorability by up to 143.1% (29.2% on average) while maintaining or improving runtime compared with the state-of-the-art signal selection techniques. Kamran Rahmani, Sandip Ray, Prabhat Mishra 0001 |
IEEE Trans. Very Large Scale Integr. Syst. | 3 |
| 2016 | MERS: Statistical Test Generation for Side-Channel Analysis based Trojan DetectionabstractHardware Trojan detection has emerged as a critical challenge to ensure security and trustworthiness of integrated circuits. A vast majority of research efforts in this area has utilized side-channel analysis for Trojan detection. Functional test generation for logic testing is a promising alternative but it may not be helpful if a Trojan cannot be fully activated or the Trojan effect cannot be propagated to the observable outputs. Side-channel analysis, on the other hand, can achieve significantly higher detection coverage for Trojans of all types/sizes, since it does not require activation/propagation of an unknown Trojan. However, they have often limited effectiveness due to poor detection sensitivity under large process variations and small Trojan footprint in side-channel signature. In this paper, we address this critical problem through a novel side-channel-aware test generation approach, based on a concept of Multiple Excitation of Rare Switching (MERS), that can significantly increase Trojan detection sensitivity. The paper makes several important contributions: i) it presents in detail the statistical test generation method, which can generate high-quality testset for creating high relative activity in arbitrary Trojan instances; ii) it analyzes the effectiveness of generated testset in terms of Trojan coverage; and iii) it describes two judicious reordering methods can further tune the testset and greatly improve the side channel sensitivity. Simulation results demonstrate that the tests generated by MERS can significantly increase the Trojans sensitivity, thereby making Trojan detection effective using side-channel analysis. Yuanwen Huang, Swarup Bhunia, Prabhat Mishra 0001 |
CCS | 3 |
| 2016 | Automated test generation for Debugging arithmetic circuits
Farimah Farahmandi, Prabhat Mishra 0001 |
DATE | 2 |
| 2016 | Exploiting transaction level models for observability-aware post-silicon test generation
Farimah Farahmandi, Prabhat Mishra 0001, Sandip Ray |
DATE | 2 |
| 2016 | Efficient Resource Constrained Scheduling Using Parallel Structure-Aware Pruning TechniquesabstractBranch-and-bound approaches are promising in pruning fruitless search space during the resource constrained scheduling. However, such approaches only compare the estimated upper and lower bounds of an incomplete schedule to the length of the best feasible schedule at that iteration, which does not fully exploit the potential of the pruning during the search. Aiming to improve the performance of resource constrained scheduling, this paper proposes a parallel structure-aware pruning approach that can traverse the search space significantly faster than state-of-the-art branch-and-bound techniques. This paper makes three major contributions: i) it proposes an efficient pruning technique using the structural scheduling information of the obtained best feasible schedules; ii) it investigates how to perform parallel search to enable efficient multi-directional search and generation of effective fences by tuning the operation enumeration order; and iii) it presents a framework that supports the sharing of minimum upper-bound and fence information among different search tasks to enable efficient parallel structure-aware pruning. The experimental results demonstrate that our parallel pruning approach can drastically reduce the overall resource constrained scheduling time under a wide variety of resource constraints. Mingsong Chen 0001, Xinqian Zhang, Geguang Pu, Xin Fu 0001, Prabhat Mishra 0001 |
IEEE Trans. Computers | 5 |
| 2016 | Efficient Selection of Trace and Scan Signals for Post-Silicon DebugabstractPost-silicon validation is a critical part of integrated circuit design methodology. The primary objective is to detect and eliminate the bugs that have escaped pre-silicon validation phase. One of the key challenges in post-silicon validation is the limited observability of internal signals in manufactured chips. A promising direction to improve observability is to combine trace and scan signals-a small set of trace signals are stored in every cycle, whereas a large set of scan signals are dumped across multiple cycles. Existing techniques are not very effective, since they explore a coarse-grained combination of trace and scan signals. In this paper, we propose a fine-grained architecture that addresses this issue using various scan chains with different dumping periods. We also propose efficient algorithms to select beneficial signals based on this architecture. Our experimental results demonstrate that our approach can improve restoration ratio up to 127% (36% on average) compared with existing trace-only techniques. Our approach also shows up to 125% improvement (61.7% on average) compared with techniques that allow a combination of trace and scan signals with minor (<;1%) area and power overhead. Kamran Rahmani, Sudhi Proch, Prabhat Mishra 0001 |
IEEE Trans. Very Large Scale Integr. Syst. | 3 |
| 2015 | Pre-silicon security verification and validation: a formal perspectiveabstractReusable hardware Intellectual Property (IP) based System-on-Chip (SoC) design has emerged as a pervasive design practice in the industry today. The possibility of hardware Trojans and/or design backdoors hiding in the IP cores has raised security concerns. As existing functional testing methods fall short in detecting unspecified (often malicious) logic, formal methods have emerged as an alternative for validation of trustworthiness of IP cores. Toward this direction, we discuss two main categories of formal methods used in hardware trust evaluation: theorem proving and equivalence checking. Specifically, proof-carrying hardware (PCH) and its applications are introduced in detail, in which we demonstrate the use of theorem proving methods for providing high-level protection of IP cores. We also outline the use of symbolic algebra in equivalence checking, to ensure that the hardware implementation is equivalent to its design specification, thus leaving little space for malicious logic insertion. Xiaolong Guo 0001, Raj Gautam Dutta, Yier Jin, Farimah Farahmandi, Prabhat Mishra 0001 |
DAC | 5 |
| 2015 | Variation-aware evaluation of MPSoC task allocation and scheduling strategies using statistical model checking
Mingsong Chen 0001, Daian Yue, Xiaoke Qin, Xin Fu 0001, Prabhat Mishra 0001 |
DATE | 5 |
| 2015 | Trace Buffer Attack: Security versus observability study in post-silicon debugabstractSince the standardization of AES/Rijndael symmetric-key cipher by NIST in 2001, it gained widespread acceptance in various protocols and withstood intense scrutiny from the theoretical cryptanalysts. From the physical implementation point of view, however, AES remained vulnerable. Practical attacks on AES via fault injection, differential power analysis, scan-chain and cache-access timing have been demonstrated so far. Along this line, in this paper, we propose a novel and effective attack, termed Trace Buffer Attack. Trace buffers are extensively used for post-silicon debug of digital designs. We identify this as a source of information leakage and show that, unless proper countermeasure is taken, Trace Buffer Attack is capable of partially recovering the secret keys of different AES implementations. We report the detailed process of trace-buffer attack with experimental results. We also propose a countermeasure in order to avoid such attack. Yuanwen Huang, Anupam Chattopadhyay, Prabhat Mishra 0001 |
VLSI-SoC | 3 |
| 2014 | Learning-oriented Property Decomposition for Automated Generation of Directed Tests
Mingsong Chen 0001, Xiaoke Qin, Prabhat Mishra 0001 |
J. Electron. Test. | 3 |
| 2013 | Scalable trace signal selection using machine learningabstractA key problem in post-silicon validation is to identify a small set of traceable signals that are effective for debug during silicon execution. Structural analysis used by traditional signal selection techniques leads to poor restoration quality. In contrast, simulation-based selection techniques provide superior restorability but incur significant computation overhead. In this paper, we propose an efficient signal selection technique using machine learning to take advantage of simulation-based signal selection while significantly reducing the simulation overhead. Our approach uses (1) bounded mock simulations to generate training vectors set for the machine learning technique, and (2) an elimination approach to identify the most profitable signals set. Experimental results indicate that our approach can improve restorability by up to 63.3% (17.2% on average) with a faster or comparable runtime. Kamran Rahmani, Prabhat Mishra 0001, Sandip Ray |
ICCD | 2 |
| 2013 | Bitmask aware compression of NISC control words
Kanad Basu, Chetan Murthy, Prabhat Mishra 0001 |
Integr. | 3 |
| 2013 | RATS: Restoration-Aware Trace Signal Selection for Post-Silicon ValidationabstractPost-silicon validation is one of the most important and expensive tasks in modern integrated circuit design methodology. The primary problem governing post-silicon validation is the limited observability due to storage of a small number of signals in a trace buffer. The signals to be traced should be carefully selected in order to maximize restoration of the remaining signals. Existing approaches have two major drawbacks. They depend on partial restorability computations that are not effective in restoring maximum signal states. They also require long signal selection time due to inefficient computation as well as operating on gate-level netlist. We have proposed a signal selection approach based on total restorability at gate-level, which is computationally more efficient (10 times faster) and can restore up to three times more signals compared to existing methods. We have also developed a register transfer level signal selection approach, which reduces both memory requirements and signal selection time by several orders-of-magnitude. Kanad Basu, Prabhat Mishra 0001 |
IEEE Trans. Very Large Scale Integr. Syst. | 2 |
| 2012 | Automated generation of directed tests for transition coverage in cache coherence protocolsabstractProcessors with multiple cores and complex cache coherence protocols are widely employed to improve the overall performance. It is a major challenge to verify the correctness of a cache coherence protocol since the number of reachable states grows exponentially with the number of cores. In this paper, we propose an efficient test generation technique, which can be used to achieve full state and transition coverage in simulation based verification for a wide variety of cache coherence protocols. Based on effective analysis of the state space structure, our method can generate more efficient test sequences (50% shorter) compared with tests generated by breadth first search. Moreover, our proposed approach can generate tests on-the-fly due to its space efficient design. Xiaoke Qin, Prabhat Mishra 0001 |
DATE | 2 |
| 2012 | Synergistic integration of code encryption and compression in embedded systemsabstractCode encryption is a promising approach that encrypts the application binary to protect it from reverse engineering and tampering, and decrypts the instructions during runtime. A major challenge is to trade-off between the security level and runtime decryption overhead. In this paper, we explore a synergistic combination of various code compression algorithms with code encryption techniques to reduce this overhead. Since decryption overhead (time) is linearly dependent on code size, it is promising to employ compression to reduce code size, and thereby achieve the advantages of both compression and encryption. Experimental results demonstrate that our proposed scheme can employ efficient encryption techniques while significantly improve the performance up to 2.3X (1.5X on average) and reduce energy consumption up to 57% (26% on average), compared to using encryption alone. Kamran Rahmani, Hadi Hajimiri, Kartik Shrivastava, Prabhat Mishra 0001 |
ACM Great Lakes Symposium on VLSI | 4 |
| 2012 | Memory-based computing for performance and energy improvement in multicore architecturesabstractMemory-based computing (MBC) is promising for improving performance and energy efficiency in both data- and compute-intensive applications. In this paper, we propose a novel reconfigurable MBC framework for multicore architectures where each core uses caches for computation using Look Up Tables (LUTs). Experimental results demonstrate that on-demand memory-based computing in each core can significantly improve performance (up to 4.7X, 3.3X on average) as well as reduce energy consumption (up to 4.7X, 2X on average) in multicore architectures. Kamran Rahmani, Prabhat Mishra 0001, Swarup Bhunia |
ACM Great Lakes Symposium on VLSI | 2 |
| 2012 | TCEC: Temperature and Energy-Constrained Scheduling in Real-Time Multitasking SystemsabstractThe ongoing scaling of semiconductor technology is causing severe increase of on-chip power density and temperature in microprocessors. This urgently requires both power and thermal management during system design. In this paper, we propose a model checking-based technique using extended timed automata to solve the processor frequency assignment problem in a temperature and energy-constrained multitasking system. We also develop a polynomial time-approximation algorithm to address the state-space explosion problem caused by symbolic model checker. Our approximation scheme is guaranteed to not generate any false-positive answer, while it may return false-negative answer in rare cases. Our method is universally applicable since it is independent of any system and task characteristics. Experimental results demonstrate the usefulness of our approach. Xiaoke Qin, Weixun Wang, Prabhat Mishra 0001 |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 3 |
| 2012 | Automatic RTL Test Generation from SystemC TLM SpecificationsabstractSystemC transaction-level modeling (TLM) is widely used to enable early exploration for both hardware and software designs. It can reduce the overall design and validation effort of complex system-on-chip (SOC) architectures. However, due to lack of automated techniques coupled with limited reuse of validation efforts between abstraction levels, SOC validation is becoming a major bottleneck. This article presents a novel top-down methodology for automatically generating register transfer-level (RTL) tests from SystemC TLM specifications. It makes two important contributions: i) it proposes a method that can automatically generate TLM tests using various coverage metrics, and (ii) it develops a test refinement specification for automatically converting TLM tests to RTL tests in order to reduce overall validation effort. We have developed a tool which incorporates these activities to enable automated RTL test generation from SystemC TLM specifications. Case studies using a router example and a 64-bit Alpha AXP pipelined processor demonstrate that our approach can achieve intended functional coverage of the RTL designs, as well as capture various functional errors and inconsistencies between specifications and implementations. Mingsong Chen 0001, Prabhat Mishra 0001, Dhrubajyoti Kalita |
ACM Trans. Embed. Comput. Syst. | 2 |
| 2012 | Dynamic Cache Reconfiguration for Soft Real-Time SystemsabstractIn recent years, efficient dynamic reconfiguration techniques have been widely employed for system optimization. Dynamic cache reconfiguration is a promising approach for reducing energy consumption as well as for improving overall system performance. It is a major challenge to introduce cache reconfiguration into real-time multitasking systems, since dynamic analysis may adversely affect tasks with timing constraints. This article presents a novel approach for implementing cache reconfiguration in soft real-time systems by efficiently leveraging static analysis during runtime to minimize energy while maintaining the same service level. To the best of our knowledge, this is the first attempt to integrate dynamic cache reconfiguration in real-time scheduling techniques. Our experimental results using a wide variety of applications have demonstrated that our approach can significantly reduce the cache energy consumption in soft real-time systems (up to 74%). Weixun Wang, Prabhat Mishra 0001, Ann Gordon-Ross |
ACM Trans. Embed. Comput. Syst. | 2 |
| 2012 | Directed test generation for validation of multicore architecturesabstractFunctional validation is widely acknowledged as a major challenge for multicore architectures. Directed tests are promising since a significantly smaller number of directed tests can achieve the same coverage goal compared to constrained-random tests. SAT-based bounded model checking is effective for automated generation of directed tests (counterexamples). While existing approaches focus on clause forwarding between different bounds to reduce the test generation time, this article proposes a novel technique that exploits temporal, structural, and spatial symmetry in multicore designs at the same time. Our proposed technique enables the reuse of the knowledge learned from one core to the remaining cores in multicore architectures (structural symmetry), from one bound to the next for a give property (temporal symmetry), as well as from one property to other properties (spatial symmetry). The experimental results demonstrate that our approach can significantly (3--10 times) reduce overall test generation time compared to existing approaches. Xiaoke Qin, Prabhat Mishra 0001 |
ACM Trans. Design Autom. Electr. Syst. | 2 |
| 2012 | System-Wide Leakage-Aware Energy Minimization Using Dynamic Voltage Scaling and Cache Reconfiguration in Multitasking SystemsabstractSystem optimization techniques are widely used to improve energy efficiency as well as overall performance. Dynamic voltage scaling (DVS) is well studied and known to be successful in reducing processor energy consumption. Due to the increasing significance of the memory subsystem's energy consumption, dynamic cache reconfiguration (DCR) techniques are recently proposed at the aim of improving cache subsystem's energy efficiency. As the manufacturing technology scales into the order of nanometers, leakage current, which leads to static power consumption, becomes a significant contributor in the overall power dissipation. In this paper, we consider various system components and study their impact on system-wide energy consumption under different processor voltage levels as well as cache configurations. Based on the observation, we efficiently integrate DVS and DCR techniques together to make decisions judiciously so that the total energy consumption is minimized. Our studies show that considering only DVS or DCR and ignoring the impact from other system components may lead to incorrect conclusions in overall energy savings. Experimental results demonstrate that our approach outperforms existing leakage-aware DVS techniques by 47.6% and leakage-oblivious DVS + DCR technique by up to 23.5%. Weixun Wang, Prabhat Mishra 0001 |
IEEE Trans. Very Large Scale Integr. Syst. | 2 |
| 2011 | Dynamic cache reconfiguration and partitioning for energy optimization in real-time multi-core systemsabstractMulticore architectures, especially chip multi-processors, have been widely acknowledged as a successful design paradigm. Existing approaches primarily target application-driven partitioning of the shared cache to alleviate inter-core cache interference so that both performance and energy efficiency are improved. Dynamic cache reconfiguration is a promising technique in reducing energy consumption of the cache subsystem for uniprocessor systems. In this paper, we present a novel energy optimization technique which employs both dynamic reconfiguration of private caches and partitioning of the shared cache for multicore systems with real-time tasks. Our static profiling based algorithm is designed to judiciously find beneficial cache configurations (of private caches) for each task as well as partition factors (of the shared cache) for each core so that the energy consumption is minimized while task deadline is satisfied. Experimental results using real benchmarks demonstrate that our approach can achieve 29.29% energy saving on average compared to systems employing only cache partitioning. Weixun Wang, Prabhat Mishra 0001, Sanjay Ranka |
DAC | 2 |
| 2011 | Decision ordering based property decomposition for functional test generationabstractSAT-based BMC is promising for directed test generation since it can locate the reason of an error within a small bound. However, due to the state space explosion problem, BMC cannot handle complex designs and properties. Although various optimization methods are proposed to address a single complex property, the test generation process cannot be fully automated. This paper presents an efficient automated approach that can scale down the falsification complexity using property decomposition and learning techniques. Our experimental results using both software and hardware benchmarks demonstrate that our approach can drastically reduce the overall test generation effort. Mingsong Chen 0001, Prabhat Mishra 0001 |
DATE | 2 |
| 2011 | Efficient combination of trace and scan signals for post silicon validation and debugabstractPost-silicon validation is as an important aspect of any integrated circuit design methodology. The primary objective is to capture the bugs that have escaped the pre-silicon validation phase. A major challenge in post-silicon debug is the limited observability of internal signals in the circuit. Recent technological advances, such as embedded logic analysis, allow to store some signal states in a trace buffer. A promising direction to improve observability is to combine a small set of signals traced every cycle with a large set of scan signals stored across several cycles. The limited size of the trace buffer constrains the number of trace and scan signals that can be stored. In this paper, we propose an efficient algorithm to select a profitable combination of trace and scan signals to maximize the overall signal restoration performance. Our experimental results using ISCAS'89 benchmarks demonstrate that our approach can improve the signal restoration by 17% compared to the existing techniques. Kanad Basu, Prabhat Mishra 0001, Priyadarsan Patra |
ITC | 2 |
| 2011 | Efficient trace data compression using statically selected dictionaryabstractPost-silicon validation and debug have gained importance in recent years to track down errors that have escaped the pre-silicon phase. Limited observability of internal signals during post-silicon debug necessitates the storage of signal states in real time. Trace buffers are used to store these states. To increase the debug observation window, it is essential to compress these trace signals, so that trace data over larger number of cycles can be stored in the trace buffer while keeping its size constant. In this paper, we propose several dictionary based compression techniques for trace data compression that takes account of the fact that the difference between golden and erroneous trace data is small. Therefore, the static dictionary selected based on golden trace data can provide notably better compression performance than the dynamic dictionaries selected in the current approaches. This will also significantly reduce the hardware overhead by reducing the dictionary size. Our experimental results demonstrate that our approach can provide up to 60% better compression compared to existing approaches, while reducing the architecture overhead by 84%. Kanad Basu, Prabhat Mishra 0001 |
VTS | 2 |
| 2011 | Property Learning Techniques for Efficient Generation of Directed TestsabstractProperty falsification in model checking is widely used for automated generation of directed tests. Due to state space explosion problem, traditional model checking techniques cannot handle large scale designs. SAT-based bounded model checking is promising to address the prohibitively large time and resource requirements during the property falsification. This article presents several efficient learning techniques that can improve the overall test generation time for a single property as well as a cluster of similar properties. The goal is to exploit both variable assignments and common conflict clauses of the prechecked partial or similar SAT instances for property falsification. Our method makes three novel contributions: 1) investigates the decision ordering-based learnings for a single SAT instance; 2) applies the decision ordering learnings between similar SAT instances; and 3) exploits the relation between the decision ordering-based learning and conflict clauses-based learning. Our experimental results using both software and hardware benchmarks demonstrate that our approach can drastically reduce the overall test generation time. Mingsong Chen 0001, Prabhat Mishra 0001 |
IEEE Trans. Computers | 2 |
| 2011 | Decoding-Aware Compression of FPGA BitstreamsabstractBitstream compression is important in reconfigurable system design since it reduces the bitstream size and the memory requirement. It also improves the communication bandwidth and thereby decreases the reconfiguration time. Existing research in this field has explored two directions: efficient compression with slow decompression or fast decompression at the cost of compression efficiency. This paper proposes a novel decode-aware compression technique to improve both compression and de compression efficiencies. The three major contributions of this paper are: 1) smart placement of compressed bitstreams that can significantly decrease the overhead of decompression engine; 2) selection of profitable parameters for bitstream compression; and 3) efficient combination of bitmask-based compression and run length encoding of repetitive patterns. Our proposed technique outperforms the existing compression approaches by 15%, while our decompression hardware for variable-length coding is capable of operating at the speed closest to the best known field-programmable gate array-based decoder for fixed-length coding. Xiaoke Qin, Chetan Muthry, Prabhat Mishra 0001 |
IEEE Trans. Very Large Scale Integr. Syst. | 3 |
| 2010 | PreDVS: preemptive dynamic voltage scaling for real-time systems using approximation schemeabstractSystem optimization techniques based on dynamic voltage scaling (DVS) are widely used with the aim of reducing processor energy consumption. Inter-task DVS assigns the same voltage level to all the instances of each task. Its intra-task counterpart exploits more energy savings by assigning multiple voltage levels within each task. In this paper, we propose a voltage scaling technique, named PreDVS, which assigns voltage levels based on the task set's preemptive scheduling for hard real-time systems. Our approach is based on an approximation scheme hence can guarantee to generate solutions within a specified quality bound (e.g., within 1% of the optimal) and is different from any existing inter- or intratask DVS techniques. PreDVS exploits static time slack at a finer granularity and achieves more energy saving than inter-task scaling without introducing any extra voltage switching overhead. Moreover, it can be efficiently employed together with existing intra-task scaling techniques. Experimental results demonstrate that PreDVS can significantly reduce energy consumption and outperform the optimal inter-task voltage scaling techniques by up to 24%. Weixun Wang, Prabhat Mishra 0001 |
DAC | 2 |
| 2010 | Efficient decision ordering techniques for SAT-based test generationabstractModel checking techniques are promising for automated generation of directed tests. However, due to the prohibitively large time and resource requirements, conventional model checking techniques do not scale well when checking complex designs. In SAT-based BMC, many variable ordering heuristics have been investigated to improve counterexample (test) generation involving only one property. This paper presents efficient decision ordering techniques that can improve the overall test generation time of a cluster of similar properties. Our method exploits the assignments of previously generated tests and incorporates it in the decision ordering heuristic for current test generation. Our experimental results using both software and hardware benchmarks demonstrate that our approach can drastically reduce the overall test generation time. Mingsong Chen 0001, Xiaoke Qin, Prabhat Mishra 0001 |
DATE | 3 |
| 2010 | Temperature- and energy-constrained scheduling in multitasking systems: a model checking approachabstractThe ongoing scaling of semiconductor technology is causing severe increase of on-chip power density and temperature in microprocessors. This has raised urgent requirement for both power and thermal management during each level of system design. In this paper, we propose a formal technique based on model checking using extended timed automata to solve the processor frequency assignment problem in a temperature- and energy- constrained multitasking system. The state space explosion problem is alleviated by transforming and solving a Pseudo-Boolean satisfiability problem. Our approach is capable of finding efficient solutions under various constraints and applicable to other problem variants as well. Our method is independent of any system and task characteristics. Experimental results demonstrate the usefulness of our approach. Weixun Wang, Xiaoke Qin, Prabhat Mishra 0001 |
ISLPED | 3 |
| 2010 | Guest Editorial
Prabhat Mishra 0001 |
J. Electron. Test. | 1 |
| 2010 | Functional Test Generation Using Efficient Property Clustering and Learning TechniquesabstractFunctional verification is one of the major bottlenecks in system-on-chip design due to the combined effects of increasing complexity and lack of automated techniques for generating efficient tests. Several promising ideas using bounded model checking are proposed over the years to efficiently generate counterexamples (tests). The existing researchers have used incremental satisfiability to improve the counterexample generation, involving only one property by sharing knowledge across instances of the same property with incremental bounds. In this paper, we present a framework that can efficiently reduce the overall test generation time by exploiting the similarity among different properties. This paper makes two primary contributions: (1) it proposes novel methods to cluster similar properties; and (2) it develops efficient learning techniques that can significantly reduce the overall test generation time for the properties in a cluster by sharing knowledge across similar test generation instances. Our experimental results using both software and hardware benchmarks demonstrate that our approach can drastically reduce (on average three to five times) the overall test generation time compared to existing methods. Mingsong Chen 0001, Prabhat Mishra 0001 |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 2 |
| 2010 | Test Data Compression Using Efficient Bitmask and Dictionary Selection MethodsabstractHigher circuit densities in system-on-chip (SOC) designs have led to drastic increase in test data volume. Larger test data size demands not only higher memory requirements, but also an increase in testing time. Test data compression addresses this problem by reducing the test data volume without affecting the overall system performance. This paper proposes a novel test data compression technique using bitmasks which provides a substantial improvement in the compression efficiency without introducing any additional decompression penalty. The major contributions of this paper are as follows: 1) it develops an efficient bitmask selection technique for test data in order to create maximum matching patterns; 2) it develops an efficient dictionary selection method which takes into account the bitmask based compression; and 3) it proposes a test compression technique using efficient dictionary and bitmask selection to significantly reduce the testing time and memory requirements. We have applied our method on various test data sets and compared our results with other existing test compression techniques. Our algorithm outperforms existing dictionary-based approaches by up to 30%, giving a best possible test compression of 92%. Kanad Basu, Prabhat Mishra 0001 |
IEEE Trans. Very Large Scale Integr. Syst. | 2 |
| 2009 | Generating test programs to cover pipeline interactionsabstractFunctional validation of a processor design through execution of a suite of test programs is common industrial practice. In this paper, we develop a high-level architectural specification driven methodology for systematic test-suite generation. Our primary contribution is an automated test-suite generation methodology that covers all possible processor pipeline interactions. To accomplish this automation, we (1) develop a fully formal processor model based on communicating extended finite state machines, and (2) traverse the processor model for on-the-fly generation of short test programs covering all reachable states and transitions. Our test generation method achieves several orders of magnitude reduction in test-suite size compared to the previously proposed formal approaches for test generation, leading to drastic reduction in validation effort. Thanh Nga Dang, Abhik Roychoudhury, Tulika Mitra, Prabhat Mishra 0001 |
DAC | 4 |
| 2009 | Bitmask-based control word compression for NISC architecturesabstractImplementing a custom hardware is not always feasible due to cost and time considerations. No instruction set computer (NISC) architecture is one of the promising direction to design a custom datapath for each application using its execution characteristics. A major challenge with NISC control word is that they tend to be at least 4 to 5 times larger than regular instruction size, thereby imposing higher memory requirement. A promising approach is to compress these control words to reduce the code size of the application. This article proposes an efficient bitmask-based compression technique to drastically reduce the control word size while keeping the decompression overhead minimal. The main contributions of our approach are: i) efficient don't care resolution for maximum bitmask coverage using limited dictionary entries, ii) run length encoding to significantly reduce repetitive control words, and iii) smart encoding of constant and less frequently changing bits. Our experimental results demonstrate that our approach improves compression efficiency by an average of 20% over the best known control word compression, giving a compression ratio of 25% to 35%. Chetan Murthy, Prabhat Mishra 0001 |
ACM Great Lakes Symposium on VLSI | 2 |
| 2009 | A Universal Placement Technique of Compressed Instructions for Efficient Parallel DecompressionabstractInstruction compression is important in embedded system design since it reduces the code size (memory requirement) and thereby improves the overall area, power, and performance. Existing research in this field has explored two directions: efficient compression with slow decompression, or fast decompression at the cost of compression efficiency. This paper combines the advantages of both approaches by introducing a novel bitstream placement method. Our contribution in this paper is a novel compressed bitstream placement technique to support parallel decompression without sacrificing the compression efficiency. The proposed technique enables splitting a single bitstream (instruction binary) fetched from memory into multiple bitstreams, which are then fed into different decoders. As a result, multiple slow decoders can simultaneously work to produce the effect of high decode bandwidth. We prove that our approach is a close approximation of the optimal placement scheme. Our experimental results demonstrate that our approach can improve the decode bandwidth up to four times with minor impact (less than 3%) on the compression efficiency. Xiaoke Qin, Prabhat Mishra 0001 |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 2 |
| 2009 | Functional test generation using design and property decomposition techniquesabstractFunctional verification of microprocessors is one of the most complex and expensive tasks in the current system-on-chip design methodology. Simulation using functional test vectors is the most widely used form of processor validation. A significant bottleneck in the validation of such systems is the lack of automated techniques for directed test generation. While existing model checking--based approaches have proposed several promising ideas for automated test generation, many challenges remain in applying them to industrial microprocessors. The time and resources required for test generation using existing model checking--based techniques can be prohibitively large. This article presents an efficient test generation technique using decompositional model checking. The contribution of the article is the development of both property and design decomposition procedures for efficient test generation of pipelined processors. Our experimental results using a multi-issue MIPS processor and an industrial processor based on Power Architecture™ Technology demonstrate several orders-of-magnitude reduction in validation effort by drastically reducing both test generation time and test program length. Heon-Mo Koo, Prabhat Mishra 0001 |
ACM Trans. Embed. Comput. Syst. | 2 |
| 2009 | Hybrid-compiled simulation: An efficient technique for instruction-set architecture simulationabstractInstruction-set simulators are critical tools for the exploration and validation of new processor architectures. Due to the increasing complexity of architectures and time-to-market pressure, performance is the most important feature of an instruction-set simulator. Interpretive simulators are flexible but slow, whereas compiled simulators deliver speed at the cost of flexibility and compilation overhead. This article presents a hybrid instruction-set-compiled simulation (HISCS) technique for generation of fast instruction-set simulators that combines the benefit of both compiled and interpretive simulation. This article makes two important contributions: (i) it improves the interpretive simulation performance by applying compiled simulation at the instruction level using a novel template-customization technique to generate optimized decoded instructions during compile time; and (ii) it reduces the compile-time overhead by combining the benefits of both static and dynamic-compiled simulation. Our experimental results using two contemporary processors (ARM7 and SPARC) demonstrate an order-of-magnitude reduction in compilation time as well as a 70% performance improvement, on average, over the best-known published result in instruction-set simulation. Mehrdad Reshadi, Prabhat Mishra 0001, Nikil Dutt |
ACM Trans. Embed. Comput. Syst. | 2 |
| 2008 | A novel test-data compression technique using application-aware bitmask and dictionary selection methodsabstractHigher circuit densities in System-on-Chip (SOC) designs have led to enhancement in the test data volume. Larger test data size demands not only greater memory requirements, but also an increase in the testing time. Test data compression addresses this problem by reducing the test data volume without affecting the overall system performance. This paper proposes a novel test data compression technique using bitmasks which provides a significant enhancement in the compression efficiency without introducing any additional decompression penalty. The major contributions of this paper are as follows: i) it develops an efficient bitmask selection technique for test data in order to create maximum matching patterns; ii) it develops an efficient dictionary selection method which takes into account the speculated results of compressed codes and iii) it proposes a suitable code compression technique using dictionary and bitmask based code compression that can reduce the memory and time requirements. We have used our algorithm on various test data sets and compared our results with other existing test compression techniques. Our algorithm outperforms the best known existing compression technique up to 30%, giving a best possible compression of 92.2%. Kanad Basu, Prabhat Mishra 0001 |
ACM Great Lakes Symposium on VLSI | 2 |
| 2008 | Coverage-driven automatic test generation for uml activity diagramsabstractDue to the increasing complexity of today's embedded systems, the analysis and validation of such systems is becoming a major challenge. UML is gradually adopted in the embedded system design as a system level specification. One of the major bottlenecks in the validation of UML activity diagrams is the lack of automated techniques for directed test generation. This paper proposes an automated test generation approach for the UML activity diagrams. The contribution of this paper is the use of specification coverage to generate properties as well as design models to enable directed test generation using model checking. Our experimental results demonstrate that our approach can drastically reduce the validation effort in both specification and implementation levels. Mingsong Chen 0001, Prabhat Mishra 0001, Dhrubajyoti Kalita |
ACM Great Lakes Symposium on VLSI | 2 |
| 2008 | Bitmask-Based Code Compression for Embedded SystemsabstractEmbedded systems are constrained by the available memory. Code-compression techniques address this issue by reducing the code size of application programs. It is a major challenge to develop an efficient code-compression technique that can generate substantial reduction in code size without affecting the overall system performance. We present a novel code-compression technique using bitmasks, which significantly improves the compression efficiency without introducing any decompression penalty. This paper makes three important contributions. 1) It develops an efficient bitmask-selection technique that can create a large set of matching patterns. 2) It develops an efficient dictionary-selection technique based on bitmasks. 3) It proposes a dictionary-based code-compression algorithm using the bitmask- and dictionary-selection techniques that can significantly reduce the memory requirement. To demonstrate the usefulness of our approach, we have performed code compression using applications from various domains and compiled for a wide variety of architectures. Our approach outperforms the existing dictionary-based techniques by an average of 20%, giving a compression ratio of 55%-65%. Seok-Won Seong, Prabhat Mishra 0001 |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. | 2 |
| 2008 | Specification-driven directed test generation for validation of pipelined processorsabstractFunctional validation is a major bottleneck in pipelined processor design due to the combined effects of increasing design complexity and lack of efficient techniques for directed test generation. Directed test vectors can reduce overall validation effort, since shorter tests can obtain the same coverage goal compared to the random tests. This article presents a specification-driven directed test generation methodology. The proposed methodology makes three important contributions. First, a general graph model is developed that can capture the structure and behavior (instruction set) of a wide variety of pipelined processors. The graph model is generated from the processor specification. Next, we propose a functional fault model that is used to define the functional coverage for pipelined architectures. Finally, we propose two complementary test generation techniques: test generation using model checking, and test generation using template-based procedures. These test generation techniques accept the graph model of the architecture as input and generate test programs to detect all the faults in the functional fault model. Our experimental results on two pipelined processor models demonstrate several orders-of-magnitude reduction in overall validation effort by drastically reducing both test-generation time and number of test programs required to achieve a coverage goal. Prabhat Mishra 0001, Nikil Dutt |
ACM Trans. Design Autom. Electr. Syst. | 1 |
| 2007 | A Retargetable Software Timing Analyzer Using Architecture Description LanguageabstractWorst case execution time (WCET) is an essential input for performance and schedulability analysis of real-time systems. Static WCET analysis requires program path analysis and microarchitecture modeling. Despite almost two decades of research, WCET analysis has not enjoyed wide acceptance in industry. This is in part due to the difficulty in microarchitecture modeling of modern processors. Given the large number of embedded processors available in the market, retargetability of the WCET analysis framework is a serious issue. In this paper, we address it using architecture description language (ADL). Starting with the ADL of a target processor, the proposed framework automatically generates graph-based execution models to capture timing effects of instructions in the pipeline. This pipeline model coupled with parameterized models of cache and branch prediction lead to a WCET framework that is safe, accurate and retargetable. Abhik Roychoudhury, Tulika Mitra, Prabhat Mishra 0001, Xu Cheng 0001 |
ASP-DAC | 4 |
| 2007 | An efficient code compression technique using application-aware bitmask and dictionary selection methodsabstractMemory plays a crucial role in designing embedded systems. A larger memory can accommodate more and large applications but increases cost, area, as well as energy requirements. Code compression techniques address this problem by reducing the size of the applications. While early work on bitmask-based compression has proposed several promising ideas, many challenges remain in applying them to embedded system design. This paper makes two important contributions to address these challenges by developing application-specific bitmask selection and bitmask-aw are dictionary selection techniques. The authors applied these techniques for code compression of TI and MediaBench applications to demonstrate the usefulness of the approach Seok-Won Seong, Prabhat Mishra 0001 |
DATE | 2 |
| 2006 | Functional test generation using property decompositions for validation of pipelined processorsabstractFunctional validation is a major bottleneck in pipelined processor design. Simulation using functional test vectors is the most widely used form of processor validation. While existing model checking based approaches have proposed several promising ideas for efficient test generation, many challenges remain in applying them to realistic pipelined processors. The time and resources required for test generation using existing model checking based techniques can be extremely large. This paper presents an efficient test generation technique using decompositional model checking. The contribution of the paper is the development of both property and design decomposition procedures for efficient test generation of pipelined processors. Our experimental results using a multi-issue MIPS processor demonstrate several orders-of-magnitude reduction in memory requirement and test generation time Heon-Mo Koo, Prabhat Mishra 0001 |
DATE | 2 |
| 2006 | Test generation using SAT-based bounded model checking for validation of pipelined processorsabstractFunctional verification is one of the major bottlenecks in microprocessor design. Simulation-based techniques are the most widely used form of processor verification. Efficient test generation is crucial for the simulation-based verification. We present an efficient test generation methodology using SAT-based bounded model checking (BMC). This paper addresses two important challenges in test generation using SAT-based BMC: determination of bound for each property, and application of design and property decompositions to improve test generation time as well as memory requirement. Our experimental results using a MIPS processor demonstrate the feasibility and usefulness of our approach. Heon-Mo Koo, Prabhat Mishra 0001 |
ACM Great Lakes Symposium on VLSI | 2 |
| 2006 | A bitmask-based code compression technique for embedded systemsabstractEmbedded systems are constrained by the available memory. Code compression techniques address this issue by reducing the code size of application programs. Dictionary-based code compression techniques are popular because they offer both good compression ratio and fast decompression scheme. Recently proposed techniques [8, 9] improve standard dictionary-based compression by consideringmismatches. This paper makes two important contributions: i) it provides a cost-benefit analysis framework for improving the compression ratio by creating more matching patterns, and ii) it develops an efficient code compression technique using bitmasks to improve the compression ratio without introducing any decompression penalty. To demonstrate the usefulness of our approach we have used applications from various domains and compiled for a wide variety of architectures. Our approach outperforms the existing dictionary-based techniques by an average of 15%, giving a compression ratio of 55% - 65%. Seok-Won Seong, Prabhat Mishra 0001 |
ICCAD | 2 |
| 2006 | A retargetable framework for instruction-set architecture simulationabstractInstruction-set architecture (ISA) simulators are an integral part of today's processor and software design process. While increasing complexity of the architectures demands high-performance simulation, the increasing variety of available architectures makes retargetability a critical feature of an instruction-set simulator. Retargetability requires generic models while high-performance demands target specific customizations. To address these contradictory requirements, we have developed a generic instruction model and a generic decode algorithm that facilitates easy and efficient retargetability of the ISA-simulator for a wide range of processor architectures, such as RISC, CISC, VLIW, and variable length instruction-set processors. The instruction model is used to generate compact and easy to debug instruction descriptions that are very similar to that of architecture manual. These descriptions are used to generate high-performance simulators. Our retargetable framework combines the flexibility of interpretive simulation with the speed of compiled simulation. The generation of the simulator is completely separate from the simulation engine. Hence, we can incorporate any fast simulation technique in our retargetable framework without introducing any performance penalty. To demonstrate this, we have incorporated fast IS-CS simulation engine in our retargetable framework which has generated 70% performance improvement over the best known simulators in this category. We illustrate the retargetability of our approach using two popular, yet different, realistic architectures: the SPARC and the ARM. Mehrdad Reshadi, Nikil Dutt, Prabhat Mishra 0001 |
ACM Trans. Embed. Comput. Syst. | 3 |
| 2006 | Architecture description language (ADL)-driven software toolkit generation for architectural exploration of programmable SOCsabstractAdvances in semiconductor technology permit increasingly complex applications to be realized using programmable systems-on-chips (SOCs). Furthermore, shrinking time-to-market demands, coupled with the need for product versioning through software modification of SOC platforms, have led to a significant increase in the software content of these SOCs. However, designer productivity is greatly hampered by the lack of automated software generation tools for the exploration and evaluation of different architectural configurations. Traditional hardware-software codesign flows do not support effective exploration and customization of the embedded processors used in programmable SOCs. The inherently application-specific nature of embedded processors and the stringent area, power, and performance constraints in embedded systems design critically require a fast and automated architecture exploration methodology. Architecture description language (ADL)-Driven design space exploration and software toolkit generation strategies present a viable solution to this problem, providing a systematic mechanism for a top-down design and validation of complex systems. The heart of this approach lies in the ability to automatically generate a software toolkit that includes an architecture-sensitive compiler, a cycle-accurate simulator, assembler, debugger, and verification/validation tools. This article illustrates a software toolkit generation methodology using the EXPRESSION ADL. Our exploration studies demonstrate the need for and usefulness of this approach, using as an example the problem of compiler-in-the-loop design space exploration of reduced instruction-set embedded processor architectures. Prabhat Mishra 0001, Aviral Shrivastava, Nikil Dutt |
ACM Trans. Design Autom. Electr. Syst. | 1 |
| 2005 | Functional Coverage Driven Test Generation for Validation of Pipelined ProcessorsabstractFunctional verification of microprocessors is one of the most complex and expensive tasks in the current system-on-chip design process. A significant bottleneck in the validation of such systems is the lack of a suitable functional coverage metric. The paper presents a functional coverage based test generation technique for pipelined architectures. The proposed methodology makes three important contributions. First, a general graph-theoretic model is developed that can capture the structure and behavior (instruction-set) of a wide variety of pipelined processors. Second, we propose a functional fault model that is used to define the functional coverage for pipelined architectures. Finally, test generation procedures are presented that accept the graph model of the architecture as input and generate test programs to detect all the faults in the functional fault model. Our experimental results on two pipelined processor models demonstrate that the number of test programs generated by our approach to obtain a fault coverage is an order of magnitude less than those generated by traditional random or constrained-random test generation techniques. Prabhat Mishra 0001, Nikil Dutt |
DATE | 1 |
| 2004 | Graph-Based Functional Test Program Generation for Pipelined ProcessorsabstractFunctional verification is widely acknowledged as a major bottleneck in microprocessor design. While early work on specification driven functional test program generation has proposed several promising ideas, many challenges remain in applying them to realistic embedded processors. We present a graph coverage based functional test program generation approach for pipelined processors. The proposed methodology makes three important contributions. First, it automatically generates the graph model of the pipelined processor from the specification using functional abstraction. Second, it generates functional test programs based on the coverage of the pipeline behaviour. Finally, the test generation time is drastically reduced due to the use of module level property checking. We applied this methodology on the DLX processor to demonstrate the usefulness of our approach. Prabhat Mishra 0001, Nikil Dutt |
DATE | 1 |
| 2004 | Functional Validation of Programmable ArchitecturesabstractValidation of programmable architectures, consisting of processor cores, coprocessors, and memory subsystems, is one of the major bottlenecks in current system-on-chip design methodology. A critical challenge in validation of such systems is the lack of a golden reference model. Traditional validation techniques employ different reference models depending on the abstraction level and verification task (e.g., functional simulation or property checking), resulting in potential inconsistencies between multiple reference models. This paper presents a validation methodology that uses an architecture description language (ADL) based specification as a golden reference model for validation of programmable architectures, and generation of executable models such as simulators and hardware prototypes. We present a validation framework that uses the generated hardware as a reference model to verify the hand-written implementation using a combination of symbolic simulation and equivalence checking. We also present functional coverage based test generation techniques for validation of pipelined processor architectures. Finally, the generated simulator and hardware models are also used for early exploration of programmable architectures. Prabhat Mishra 0001, Nikil Dutt |
DSD | 1 |
| 2004 | Modeling and validation of pipeline specificationsabstractVerification is one of the most complex and expensive tasks in the current Systems-on-Chip design process. Many existing approaches employ a bottom-up approach to pipeline validation, where the functionality of an existing pipelined processor is, in essence, reverse-engineered from its RT-level implementation. Our validation technique is complementary to these bottom-up approaches. Our approach leverages the system architect's knowledge about the behavior of the pipelined architecture, through architecture description language (ADL) constructs, and thus allows a powerful top-down approach to pipeline validation. The most important requirement in top-down validation process is to ensure that the specification (reference model) is golden. This paper addresses automatic validation of processor, memory, and coprocessor pipelines described in an ADL. We present a graph-based modeling that captures both structure and behavior of the architecture. Based on this model, we present algorithms to ensure that the static behavior of the pipeline is well formed by analyzing the structural aspects of the specification. We applied our methodology to verify specification of several realistic architectures from different architectural domains to demonstrate the usefulness of our approach. Prabhat Mishra 0001, Nikil Dutt |
ACM Trans. Embed. Comput. Syst. | 1 |
| 2004 | Processor-memory coexploration using an architecture description languageabstractMemory represents a major bottleneck in modern embedded systems in terms of cost, power, and performance. Traditionally, memory organizations for programmable embedded systems assume a fixed cache hierarchy. With the widening processor--memory gap, more aggressive memory technologies and organizations have appeared, allowing customization of a heterogeneous memory architecture tuned for specific target applications. However, such a processor--memory coexploration approach critically needs the ability to explicitly capture heterogeneous memory architectures. We present in this paper a language-based approach to explicitly capture the memory subsystem configuration, generate a memory-aware software toolkit, and perform coexploration of the processor--memory architectures. We present a set of experiments using our memory-aware architectural description language (ADL) to drive the exploration of the memory subsystem for the TI C6211 processor architecture, demonstrating cost, performance, and energy trade-offs. Prabhat Mishra 0001, Mahesh Mamidipaka, Nikil Dutt |
ACM Trans. Embed. Comput. Syst. | 1 |
| 2003 | Instruction set compiled simulation: a technique for fast and flexible instruction set simulationabstractInstruction set simulators are critical tools for the exploration and validation of new programmable architectures. Due to increasing complexity of the architectures and time-to-market pressure, performance is the most important feature of an instruction-set simulator. Interpretive simulators are flexible but slow, whereas compiled simulators deliver speed at the cost of flexibility. This paper presents a novel technique for generation of fast instruction set simulators that combines the benefit of both compiled and interpretive simulation. We achieve fast instruction accurate simulation through two mechanisms. First, we move the time consuming decoding process from run-time to compile time while maintaining the flexibility of the interpretive simulation. Second, we use a novel instruction abstraction technique to generate aggressively optimized decoded instructions that further improves simulation performance. Our instruction set compiled simulation (IS-CS) technique delivers upto 40% performance improvement over the best known published result that has the flexibility of interpretive simulation. We illustrate the applicability of the IS-CS technique using the ARM7 embedded processor. Mehrdad Reshadi, Prabhat Mishra 0001, Nikil Dutt |
DAC | 2 |
| 2002 | Automatic Verification of In-Order Execution In Microprocessors with Fragmented Pipelines and Multicycle Functional UnitsabstractAs embedded systems continue to face increasingly higher performance requirements, deeply pipelined processor architectures are being employed to meet desired system performance. System architects critically need modeling techniques that allow exploration, evaluation, customization and validation of different processor pipeline configurations, tuned for a specific application domain. We propose a novel finite state machine (FSM) based modeling of pipelined processors and define a set of properties that can be used to verify the correctness of in-order execution in the presence of fragmented pipelines and multicycle functional units. Our approach leverages the system architect's knowledge about the behavior of the pipelined processor through architecture description language (ADL) constructs, and thus allows a powerful top-down approach to pipeline verification. We applied this methodology to the DLX processor to demonstrate the usefulness of our approach. Prabhat Mishra 0001, Nikil Dutt, Alexandru Nicolau, Hiroyuki Tomiyama |
DATE | 1 |