arXiv Science⌕ Search

arXiv subjects

Aman Kumar

Publications and source records attributed to Aman Kumar.

At least 37 records · Page 2Linked to original sources

Origin and stability of generalized Wigner crystallinity in triangular moiré systems

Generalized Wigner crystals (GWC) on triangular moiré superlattices, formed from stacking two layers of transition metal chalcogenides, have been observed at multiple fractional fillings [Nature 587, 214 - 218 (2020), Nat. Phys. 17, 715 - 719 (2021), Nature 597, 650 - 654 (2021)]. Motivated by these experiments, tied with the need for accurate microscopic descriptions of these materials, we explore the origins of GWC at $n=1/3$ and $2/3$ filling. We demonstrate the general limitations of theoretical descriptions relying on finite-range, versus long-range interactions, however, we clarify why some properties are captured by an effective nearest-neighbor model. We study both classical and quantum effects at zero and finite temperatures, discussing the role of charge frustration, identifying a ``pinball" phase, a partially quantum melted GWC, with no classical analog. Our work addresses several experimental observations and makes predictions for how many of the theoretical findings can be potentially realized in future experiments.

cond-mat.str-el↗

Hey AI, Generate Me a Hardware Code! Agentic AI-based Hardware Design & Verification

Modern Integrated Circuits (ICs) are becoming increasingly complex, and so is their development process. Hardware design verification entails a methodical and disciplined approach to the planning, development, execution, and sign-off of functionally correct hardware designs. This tedious process requires significant effort and time to ensure a bug-free tape-out. The field of Natural Language Processing has undergone a significant transformation with the advent of Large Language Models (LLMs). These powerful models, often referred to as Generative AI (GenAI), have revolutionized how machines understand and generate human language, enabling unprecedented advancements in a wide array of applications, including hardware design verification. This paper presents an agentic AI-based approach to hardware design verification, which empowers AI agents, in collaboration with Humain-in-the-Loop (HITL) intervention, to engage in a more dynamic, iterative, and self-reflective process, ultimately performing end-to-end hardware design and verification. This methodology is evaluated on five open-source designs, achieving over 95% coverage with reduced verification time while demonstrating superior performance, adaptability, and configurability.

cs.AI↗

NTIRE 2025 Challenge on Day and Night Raindrop Removal for Dual-Focused Images: Methods and Results

This paper reviews the NTIRE 2025 Challenge on Day and Night Raindrop Removal for Dual-Focused Images. This challenge received a wide range of impressive solutions, which are developed and evaluated using our collected real-world Raindrop Clarity dataset. Unlike existing deraining datasets, our Raindrop Clarity dataset is more diverse and challenging in degradation types and contents, which includes day raindrop-focused, day background-focused, night raindrop-focused, and night background-focused degradations. This dataset is divided into three subsets for competition: 14,139 images for training, 240 images for validation, and 731 images for testing. The primary objective of this challenge is to establish a new and powerful benchmark for the task of removing raindrops under varying lighting and focus conditions. There are a total of 361 participants in the competition, and 32 teams submitting valid solutions and fact sheets for the final testing phase. These submissions achieved state-of-the-art (SOTA) performance on the Raindrop Clarity dataset. The project can be found at https://lixinustc.github.io/CVPR-NTIRE2025-RainDrop-Competition.github.io/.

cs.CV↗

Saarthi: The First AI Formal Verification Engineer

Recently, Devin has made a significant buzz in the Artificial Intelligence (AI) community as the world's first fully autonomous AI software engineer, capable of independently developing software code. Devin uses the concept of agentic workflow in Generative AI (GenAI), which empowers AI agents to engage in a more dynamic, iterative, and self-reflective process. In this paper, we present a similar fully autonomous AI formal verification engineer, Saarthi, capable of verifying a given RTL design end-to-end using an agentic workflow. With Saarthi, verification engineers can focus on more complex problems, and verification teams can strive for more ambitious goals. The domain-agnostic implementation of Saarthi makes it scalable for use across various domains such as RTL design, UVM-based verification, and others.

cs.AI↗

Optimizing Coverage-Driven Verification Using Machine Learning and PyUVM: A Novel Approach

The escalating complexity of System-on-Chip (SoC) designs has created a bottleneck in verification, with traditional techniques struggling to achieve complete coverage. Existing techniques, such as Constrained Random Verification (CRV) and coverage-driven methodologies, rely on time-consuming and redundant simulation regression, leading to higher verification costs and longer time-to-market due to the manual effort required to adjust constraints and drive the stimuli to achieve coverage objectives. To address this challenge, we propose a novel methodology that leverages supervised Machine Learning (ML) to optimize simulation regressions, resulting in reduced simulation run-time and the number of test simulations required to achieve target coverage goals. We also investigate and compare the effectiveness of various supervised learning algorithms from scikit-learn. Our results demonstrate that these algorithms can achieve at least 99% coverage regain with significantly reduced simulation cycles. We utilize Python Universal Verification Methodology (PyUVM) over SystemVerilog-Universal Verification Methodology (SV-UVM) for testbench creation, enabling simpler constructs using Python and facilitating the reuse of existing ML libraries. Our methodology is applied to three diverse designs, and our results show that it can significantly reduce verification costs, manual efforts, and time-to-market, while enhancing verification productivity and completeness, by automating the testbench update process and achieving target coverage goals.

cs.AR↗

Microscopic theory of field-tuned topological transitions in the Kitaev honeycomb model

We microscopically construct an abelian mutual Chern-Simons lattice gauge theory for magnetic field-tuned topological transitions in the Kitaev model and obtain a complete characterization of the phases, including their quasiparticles. At low fields for both ferro and antiferromagnetic (FM(AFM)) Kitaev interactions, we demonstrate nonabelian Ising topological order (ITO), and explicitly construct the Majorana anyon as an intrinsic excitation -- a twist defect in our \textit{abelian} gauge theory. For the AFM case, an abelian chiral phase appears at intermediate fields with trivial topological order and fermionic bulk excitations. Remarkably, both the ITO phase and the intermediate phase have the same chiral central charge $c=1/2,$ implying no change in the quantized thermal Hall response across the transition. For the FM case, there is a direct transition from ITO to a partially polarized nontopological phase. Our study completes the proof of Kitaev's original proposal of the low-field ITO with $c=1/2$ going beyond his mean-field arguments by including the crucial effect of the gauge fluctuations, and provides a resolution of the debate surrounding the intermediate field phase in the AFM case.

cond-mat.str-el↗

Field tuning Kitaev systems for spin fractionalization and topological order

The honeycomb Kitaev model describes a $Z_2$ spin liquid with topological order and fractionalized excitations consisting of gapped $π$-fluxes and free Majorana fermions. Competing interactions, even when not very strong, are known to destabilize the Kitaev spin liquid. Magnetic fields are a convenient parameter for tuning between different phases of the Kitaev systems, and have even been investigated for potentially counteracting the effects of other destabilizing interactions leading to a revival of the topological phase. Here we review the progress in understanding the effects of magnetic fields on some of the perturbed Kitaev systems, particularly on fractionalization and topological order.

cond-mat.str-el↗

Hard Math -- Easy UVM: Pragmatic solutions for verifying hardware algorithms using UVM

This paper presents pragmatic solutions for verifying complex mathematical algorithms implemented in hardware in an efficient and effective manner. Maximizing leverage of a known-answer-test strategy, based on predefined data scenarios combined with design-for-verification modes, we demonstrate how to find and isolate concept and design bugs early in the flow. The solutions presented are based on real project experience with single chip radar sensors for a variety of applications. The verification environments supporting the presented strategies are based on SystemVerilog and the Universal Verification Methodology.

cs.AI↗

Verifying Non-friendly Formal Verification Designs: Can We Start Earlier?

The design of Systems on Chips (SoCs) is becoming more and more complex due to technological advancements. Missed bugs can cause drastic failures in safety-critical environments leading to the endangerment of lives. To overcome these drastic failures, formal property verification (FPV) has been applied in the industry. However, there exist multiple hardware designs where the results of FPV are not conclusive even for long runtimes of model-checking tools. For this reason, the use of High-level Equivalence Checking (HLEC) tools has been proposed in the last few years. However, the procedure for how to use it inside an industrial toolchain has not been defined. For this reason, we proposed an automated methodology based on metamodeling techniques which consist of two main steps. First, an untimed algorithmic description written in C++ is verified in an early stage using generated assertions; the advantage of this step is that the assertions at the software level run in seconds and we can start our analysis with conclusive results about our algorithm before starting to write the RTL (Register Transfer Level) design. Second, this algorithmic description is verified against its sequential design using HLEC and the respective metamodel parameters. The results show that the presented methodology can find bugs early related to the algorithmic description and prepare the setup for the HLEC verification. This helps to reduce the verification efforts to set up the tool and write the properties manually which is always error-prone. The proposed framework can help teams working on datapaths to verify and make decisions in an early stage of the verification flow.

cs.AR↗

FuzzWiz -- Fuzzing Framework for Efficient Hardware Coverage

Ever-increasing design complexity of System-on-Chips (SoCs) led to significant verification challenges. Unlike software, bugs in hardware design are vigorous and eternal i.e., once the hardware is fabricated, it cannot be repaired with any patch. Despite being one of the powerful techniques used in verification, the dynamic random approach cannot give confidence to complex Register Transfer Leve (RTL) designs during the pre-silicon design phase. In particular, achieving coverage targets and exposing bugs is a complicated task with random simulations. In this paper, we leverage an existing testing solution available in the software world known as fuzzing and apply it to hardware verification in order to achieve coverage targets in quick time. We created an automated hardware fuzzing framework FuzzWiz using metamodeling and Python to achieve coverage goals faster. It includes parsing the RTL design module, converting it into C/C++ models, creating generic testbench with assertions, fuzzer-specific compilation, linking, and fuzzing. Furthermore, it is configurable and provides the debug flow if any crash is detected during the fuzzing process. The proposed framework is applied on four IP blocks from Google's OpenTitan chip with various fuzzing engines to show its scalability and compatibility. Our benchmarking results show that we could achieve around 90% of the coverage 10 times faster than traditional simulation regression based approach.

cs.AR↗

GCM-Net: Graph-enhanced Cross-Modal Infusion with a Metaheuristic-Driven Network for Video Sentiment and Emotion Analysis

Sentiment analysis and emotion recognition in videos are challenging tasks, given the diversity and complexity of the information conveyed in different modalities. Developing a highly competent framework that effectively addresses the distinct characteristics across various modalities is a primary concern in this domain. Previous studies on combined multimodal sentiment and emotion analysis often overlooked effective fusion for modality integration, intermodal contextual congruity, optimizing concatenated feature spaces, leading to suboptimal architecture. This paper presents a novel framework that leverages the multi-modal contextual information from utterances and applies metaheuristic algorithms to learn the contributing features for utterance-level sentiment and emotion prediction. Our Graph-enhanced Cross-Modal Infusion with a Metaheuristic-Driven Network (GCM-Net) integrates graph sampling and aggregation to recalibrate the modality features for video sentiment and emotion prediction. GCM-Net includes a cross-modal attention module determining intermodal interactions and utterance relevance. A harmonic optimization module employing a metaheuristic algorithm combines attended features, allowing for handling both single and multi-utterance inputs. To show the effectiveness of our approach, we have conducted extensive evaluations on three prominent multi-modal benchmark datasets, CMU MOSI, CMU MOSEI, and IEMOCAP. The experimental results demonstrate the efficacy of our proposed approach, showcasing accuracies of 91.56% and 86.95% for sentiment analysis on MOSI and MOSEI datasets. We have performed emotion analysis for the IEMOCAP dataset procuring an accuracy of 85.66% which signifies substantial performance enhancements over existing methods.

cs.CV↗

SafeTail: Efficient Tail Latency Optimization in Edge Service Scheduling via Computational Redundancy Management

Optimizing tail latency while efficiently managing computational resources is crucial for delivering high-performance, latency-sensitive services in edge computing. Emerging applications, such as augmented reality, require low-latency computing services with high reliability on user devices, which often have limited computational capabilities. Consequently, these devices depend on nearby edge servers for processing. However, inherent uncertainties in network and computation latencies stemming from variability in wireless networks and fluctuating server loads make service delivery on time challenging. Existing approaches often focus on optimizing median latency but fall short of addressing the specific challenges of tail latency in edge environments, particularly under uncertain network and computational conditions. Although some methods do address tail latency, they typically rely on fixed or excessive redundancy and lack adaptability to dynamic network conditions, often being designed for cloud environments rather than the unique demands of edge computing. In this paper, we introduce SafeTail, a framework that meets both median and tail response time targets, with tail latency defined as latency beyond the 90^th percentile threshold. SafeTail addresses this challenge by selectively replicating services across multiple edge servers to meet target latencies. SafeTail employs a reward-based deep learning framework to learn optimal placement strategies, balancing the need to achieve target latencies with minimizing additional resource usage. Through trace-driven simulations, SafeTail demonstrated near-optimal performance and outperformed most baseline strategies across three diverse services.

cs.LG↗

Generative AI Augmented Induction-based Formal Verification

Generative Artificial Intelligence (GenAI) has demonstrated its capabilities in the present world that reduce human effort significantly. It utilizes deep learning techniques to create original and realistic content in terms of text, images, code, music, and video. Researchers have also shown the capabilities of modern Large Language Models (LLMs) used by GenAI models that can be used to aid hardware development. Formal verification is a mathematical-based proof method used to exhaustively verify the correctness of a design. In this paper, we demonstrate how GenAI can be used in induction-based formal verification to increase the verification throughput.

cs.AI↗

Efficient Stimuli Generation using Reinforcement Learning in Design Verification

The increasing design complexity of System-on-Chips (SoCs) has led to significant verification challenges, particularly in meeting coverage targets within a timely manner. At present, coverage closure is heavily dependent on constrained random and coverage driven verification methodologies where the randomized stimuli are bounded to verify certain scenarios and to reach coverage goals. This process is said to be exhaustive and to consume a lot of project time. In this paper, a novel methodology is proposed to generate efficient stimuli with the help of Reinforcement Learning (RL) to reach the maximum code coverage of the Design Under Verification (DUV). Additionally, an automated framework is created using metamodeling to generate a SystemVerilog testbench and an RL environment for any given design. The proposed approach is applied to various designs and the produced results proves that the RL agent provides effective stimuli to achieve code coverage faster in comparison with baseline random simulations. Furthermore, various RL agents and reward schemes are analyzed in our work.

cs.AI↗

AADNet: Attention aware Demoiréing Network

Moire pattern frequently appears in photographs captured with mobile devices and digital cameras, potentially degrading image quality. Despite recent advancements in computer vision, image demoire'ing remains a challenging task due to the dynamic textures and variations in colour, shape, and frequency of moire patterns. Most existing methods struggle to generalize to unseen datasets, limiting their effectiveness in removing moire patterns from real-world scenarios. In this paper, we propose a novel lightweight architecture, AADNet (Attention Aware Demoireing Network), for high-resolution image demoire'ing that effectively works across different frequency bands and generalizes well to unseen datasets. Extensive experiments conducted on the UHDM dataset validate the effectiveness of our approach, resulting in high-fidelity images.

cs.CV↗

Effective Design Verification -- Constrained Random with Python and Cocotb

Being the most widely used language across the world due to its simplicity and with 35 keywords (v3.7), Python attracts both hardware and software engineers. Python-based verification environment leverages open-source libraries such as cocotb and cocotb-coverage that enables interfacing the tesbenches with any available simulator and facilitating constrained randomization, coverage respectively. These libraries significantly ease the development of testbenches and have the potential to reduce the setup cost. The goal of this paper is to assess the effectiveness of a Python-Cocotb verification setup with design IPs and compare its features and performance metrics with the current de-facto hardware verification language i.e., SystemVerilog.

cs.AR↗

Towards Efficient Design Verification -- Constrained Random Verification using PyUVM

Python, as a multi-paradigm language known for its ease of integration with other languages, has gained significant attention among verification engineers recently. A Python-based verification environment capitalizes on open-source frameworks such as PyUVM providing Python-based UVM 1.2 implementation and PyVSC facilitating constrained randomization and functional coverage. These libraries play a pivotal role in expediting test development and hold promise for reducing setup costs. The goal of this paper is to evaluate the effectiveness of PyUVM verification testbenches across various design IPs, aiming for a comprehensive comparison of their features and performance metrics with the established SystemVerilog-UVM methodology.

cs.AR↗

Pragmatic Formal Verification of Sequential Error Detection and Correction Codes (ECCs) used in Safety-Critical Design

Error Detection and Correction Codes (ECCs) are often used in digital designs to protect data integrity. Especially in safety-critical systems such as automotive electronics, ECCs are widely used and the verification of such complex logic becomes more critical considering the ISO 26262 safety standards. Exhaustive verification of ECC using formal methods has been a challenge given the high number of data bits to protect. As an example, for an ECC of 128 data bits with a possibility to detect up to four-bit errors, the combination of bit errors is given by 128C1 + 128C2 + 128C3 + 128C4 = 1.1 * 10^7. This vast analysis space often leads to bounded proof results. Moreover, the complexity and state-space increase further if the ECC has sequential encoding and decoding stages. To overcome such problems and sign-off the design with confidence within reasonable proof time, we present a pragmatic formal verification approach of complex ECC cores with several complexity reduction techniques and know-how that were learnt during the course of verification. We discuss using the linearity of the syndrome generator as a helper assertion, using the abstract model as glue logic to compare the RTL with the sequential version of the circuit, k-induction-based model checking and using mathematical relations captured as properties to simplify the verification in order to get an unbounded proof result within 24 hours of proof runtime.

cs.AI↗