Our research spans ML for EDA, LLM-assisted verification, high-level synthesis, formal verification, hardware security, ML and Compiler Security.
Dedicated hardware accelerators are increasingly important as conventional scaling slows. Our objective is to develop an efficient HLS-based platform and enabling technologies for faster, efficient hardware accelerator design from behavioral specifications.
HLS enables rapid development of accelerators from C/C++-level specifications, but practical adoption is limited by optimization challenges, slow RTL simulation, formal verification gaps, and security concerns. Our work addresses these limitations across the HLS flow.
FastSim automatically extracts concise, well-indented and debug-friendly C behavior from synthesized RTL. It provides cycle accuracy and performance estimation, with an average simulation speedup of around 300× compared with existing commercial RTL simulators.
HOST obfuscates designs at the end of HLS to protect ICs from IP theft early in the design cycle. The proposed obfuscations are HLS-tool agnostic and designed to resist known attacks.
We study application-specific HLS optimizations and characteristics such as array-to-BRAM mapping, loop synthesis, array access, initialization, and computation redundancies to help developers generate better accelerators.
Formal verification of HLS remains an open problem. We developed DEEQ, an automated C-to-RTL equivalence-checking framework that uses data-driven approaches to reduce verification complexity.
Formal equivalence between behavioral C specifications and generated RTL.
Equivalence checking across compiler optimizations and RTL transformations.
Loop and arithmetic transformations of array-intensive behaviors, sequential-to-parallel transformations, and parallel code transformations.
We investigate both protection mechanisms and attacks for secure hardware, with particular emphasis on logic locking and power side-channel-secure RTL design.
Fab-less IC design outsources fabrication, testing, and packaging to untrusted third parties, exposing designs to IP piracy, reverse engineering, overproduction, and IP violation. Logic locking counters this by embedding a secret key in the design: a locked netlist accepts a key input alongside its primary inputs and reproduces the original circuit's function only when the correct key is supplied.
Evaluated eFPGA-based redaction, where critical logic is hidden in reconfigurable fabric. A compound SAT plus statistical attack recovered keys up to 15,000 bits — the first attack to scale this far, showing key count alone doesn't guarantee security. The attack targets the eFPGA's configuration bits directly, combining structural SAT solving with statistical inference to prune the search space at scale. This work also won the HeLLO:CTF 2023 competition, validating the practical strength of the attack against real hardware-redaction challenges.
Logic locking at the RTL secures designs at an early stage of development. Existing SMT-based RTL attacks handle the combinational and sequential parts of a design through a unified abstraction but don't scale. SMACK is a scalable SMT-based attack that recovers keys through an improved distinguishing-input-pattern (DIP) formulation for faster termination, timeout-aware remaining-key analysis, heuristics that simplify SMT formulas involving arrays and bitvectors, and faster DIP identification by fixing a subset of primary inputs to constants. SMACK was validated on designs with up to 40K combinational cells and 4K sequential cells, locked with keys up to 810 bits.
VALOR (Vulnerability Assessment of Logic Locking using ROBDD) evaluates the robustness of logic locking across the pre-SAT, post-SAT, and machine-learning-resilient eras. The ROBDD representation inherently exposes a previously unexplored relationship between primary inputs and keys in pre-SAT and ML-resilient techniques, letting VALOR break them directly. Against post-SAT techniques, VALOR represents the functionality-stripped circuit as a ROBDD to find protected input patterns (PIPs) rather than searching for structural vulnerabilities — making it the first attack to break the recently proposed Structurally Robust SFLL (SR-SFLL). The work also gives a new theoretical view of the Boolean SAT attack: the input space partitions into disjoint equivalence classes, the number of distinguishing input patterns (DIPs) the SAT attack needs is upper-bounded by the number of such classes, and this links VALOR directly to SAT attack behavior around wrong-key pruning.
MaskedHLS is a domain-specific high-level synthesis tool that automates the generation of secure, optimized gadget-based masked cryptographic hardware directly from masked C implementations. It converts high-level masked designs into RTL, minimizing registers through low-hanging latency optimizations while verifying that the generated design is register balanced. It also supports simulation-based functional verification, a TVLA-based security-analysis pipeline, and AST/DFG visualization for debugging — reducing the manual effort of designing secure S-boxes and other masked cryptographic hardware (AES, PRESENT, and beyond).
For a fixed security order, gadget-based masked hardware faces a structural trade-off between randomness and latency that prior work has not exploited for efficient search. TETRIS introduces two dual design-space-exploration algorithms — MLRC (Minimize Latency under Randomness Constraints) and MRLC (Minimize Randomness under Latency Constraints) — that use the masking-order-dependent costs of PINI gadgets to heuristically find a latency- or randomness-optimal gadget assignment in under a millisecond, matching or beating the area of prior SAT-based state-of-the-art tools by orders of magnitude in speed. The accompanying artifact (CHES 2026) reproduces the paper's MRLC/MLRC results, including a full gadget library (HPC1/2/3, HPC2o, HPC3o, COMAR, DOMAND), asymmetric-gadget transforms, AES/SKINNY S-box benchmarks, MaskedHLS integration for RTL generation, and functional, TVLA, and VERICA-based security verification.
We explore learning-assisted techniques to replace or augment expensive heuristics in EDA and to assist verification engineers with complex assertion-generation tasks.
LEAP is a machine learning-guided framework for ASIC technology mapping that replaces traditional cut-selection heuristics with learned models to identify high-quality cuts. It uses a Cut Classifier to filter non-implementable cuts and a Delay Predictor with a sweep algorithm to select the top cuts for mapping. Experimental results on 21 designs show that LEAP reduces the number of cuts by 51% while improving delay by 2% compared to ABC, with no area penalty, and also achieves better area-delay performance than SLAP in most cases.
FedTM is a federated learning-based framework for ASIC technology mapping that enables multiple design houses to collaboratively train ML models without sharing proprietary design data. It builds on the LEAP framework, which uses a cut classifier and delay predictor to identify high-quality cuts and reduce the computational overhead of Boolean matching. Experimental results show that FedTM improves QoR by reducing delay by 2% and the number of cuts used by 23% compared with the centralized LEAP framework.
Assertion-Based Verification (ABV) is critical to design verification, but manually writing SystemVerilog Assertions (SVAs) from specifications is complex and time-consuming. Recent works use LLMs to enable automated SVA generation, and we introduced ChIRAAG as an early SVA generation framework that uses the design’s Natural Language Specification (NLS) as the primary source. Building on this, LAAG-RV and SANGAM further improve assertion quality. Our studies also highlight key challenges such as signal inconsistency, vacuity, redundancy, and coverage metric issues.
Modern compiler optimizations are designed to preserve functional correctness, but functional equivalence alone does not guarantee preservation of security properties. Our research investigates how information leakage and security properties can be systematically analyzed and verified across compiler transformations and optimization stages.
Our research focuses on verifying whether compiler optimizations preserve the security characteristics of the original program. We investigate quantitative information flow to measure information leakage and develop techniques for verifying relative security between source and optimized programs. Our approach combines static information-flow and taint analysis, information-leakage quantification, model checking, and translation validation to identify security violations introduced during compilation and optimization.
A major research direction is the security analysis of LLVM compiler transformations, including optimization passes and register allocation. In particular, we study how register allocation, spilling, splitting, and register reuse can introduce unintended information leakage under realistic attacker models. This work aims to develop security-aware compiler analyses and secure optimization techniques that preserve both program functionality and confidentiality.
Translation Validation for Relative Security Verification
Information Leakage and Relative Security Verification using CBMC
To develop efficient scheduling mechanisms that enable secure, energy-efficient, thermally sustainable, and reliable execution of real-time cyber-physical applications while satisfying stringent timing constraints.
Modern Real-Time Cyber-Physical Systems (RT-CPS) integrate sensing, computation, communication, and control to perform safety- and mission-critical operations under stringent timing constraints. Their applications are increasingly executed on distributed and heterogeneous computing platforms, where limited resources, dynamic workloads, and multiple competing objectives make efficient scheduling a challenging problem.
FastSim automatically extracts concise, well-indented and debug-friendly C behavior from synthesized RTL. It provides cycle accuracy and performance estimation, with an average simulation speedup of around 300× compared with existing commercial RTL simulators.
HOST obfuscates designs at the end of HLS to protect ICs from IP theft early in the design cycle. The proposed obfuscations are HLS-tool agnostic and designed to resist known attacks.
We study application-specific HLS optimizations and characteristics such as array-to-BRAM mapping, loop synthesis, array access, initialization, and computation redundancies to help developers generate better accelerators.
Machine learning models are increasingly deployed across diverse domains, including computer vision and natural language processing. However, these models remain vulnerable to attacks that can degrade their performance and computational efficiency. Our research investigates such vulnerabilities, develops attacks to characterize and understand these threats, and explores lightweight defenses to improve the security and robustness of ML systems.
In this work, we study adversarial patches that manipulate Vision Transformers (ViTs) by hijacking their attention and causing confident misclassifications. We observe that image tokens affected by adversarial patches exhibit distinct statistical characteristics compared to unaffected tokens. Based on this insight, we propose STRAP-ViT, a lightweight, training-free defense that detects anomalous tokens and selectively transforms them to neutralize adversarial perturbations. STRAP-ViT can be integrated into pre-trained ViTs as a plug-and-play module with minimal computational overhead, while maintaining performance close to clean-image accuracy.
Modern AI systems increasingly rely on adaptive computation and hardware-aware optimization to meet demanding requirements for latency, energy, and resource efficiency. However, optimization mechanisms that dynamically adjust computation can also create new vulnerabilities, allowing adversarial inputs to manipulate the computational behavior of AI systems. We are currently exploring efficiency degradation attacks that exploit adaptive AI systems to increase computational cost, energy consumption, and latency without affecting accuracy. Our work focuses on developing black-box attacks, lightweight defenses, and robust AI systems across vision-language, cloud, edge, and resource-constrained platforms.
Our broader work also includes scheduling for heterogeneous systems and formal modeling and verification of networks-on-chip.
Heuristic scheduling strategies targeting generic penalty minimization, schedule-length minimization, security-aware real-time DAG scheduling, and temperature-aware scheduling.
A formal simulator for NoC with applications in formal verification and security-flaw detection, along with a generic framework for developing deadlock-free routing algorithms.