arXiv subjects

Jiaxi Zhang

Publications and source records attributed to Jiaxi Zhang.

18 recordsLinked to original sources

arXiv2026

E-ALS: Approximation-Potential-Aware E-Graph Rewriting for Approximate Logic Synthesis

Approximate logic synthesis (ALS) improves circuit power, performance, and area by trading exact correctness for bounded functional error. However, existing structural ALS methods largely overlook structural bias: even functionally equivalent netlists can expose markedly different approximation opportunities and lead to substantially different outcomes under the same downstream ALS flow. Our experiments show that this effect can induce final area gaps of up to 42.77%. To unlock this opportunity, we propose E-ALS, an e-graph-based framework for approximation-aware structural search. E-ALS combines Function-Reduced Saturation, an ALS-coupled surrogate, search-based extraction, and budget-guided refinement to identify approximation-friendly equivalent structures. Experiments on well-established arithmetic and logic benchmarks show that E-ALS achieves additional area reductions of 3.2 and 7.0 percentage points under maximum Hamming-Distance and Error-Distance constraints, respectively. Code is available in https://github.com/ZenuSunB/Ecompile.git.

cs.ET↗

arXiv2026

UniGround: Universal 3D Visual Grounding via Training-Free Scene Parsing

3D Visual Grounding (3DVG) localizes objects from natural-language descriptions in 3D scenes and is fundamental to embodied AI applications. Although foundation models enable open-vocabulary reasoning, they typically rely on pre-generated candidates, creating two sequential bottlenecks. The \emph{candidate bottleneck} occurs when dataset-specific 3D proposal models miss, fragment, or incorrectly group targets under distribution shifts, excluding them from VLM reasoning. The \emph{evidence bottleneck} stems from incomplete visual evidence: global renderings preserve spatial context but obscure object details, whereas candidate-centric views capture local appearance but lack global context. To address these bottlenecks, we propose UniGround, a zero-shot 3DVG framework that addresses both bottlenecks through Global Candidate Filtering and Contextual Precision Grounding. Global Candidate Filtering constructs topology-consistent, class-agnostic candidates from 3D topology and multi-view semantic cues, without dataset-trained 3D detectors, task-specific proposal supervision, or predefined box and category priors. Contextual Precision Grounding jointly reasons over global spatial context and candidate-centric visual evidence, followed by closed-loop consistency verification for reliable target identification. UniGround achieves 46.1\%/34.1\% Acc@0.25/0.5 on ScanRefer and 28.7\% Acc@0.25 on the evaluated ARKitScenes subset of EmbodiedScan. Further experiments demonstrate competitive grounding without dataset-specific 3D priors, cross-dataset generalization to unseen indoor scenes, and robustness to real-world reconstruction noise and practical domain shifts.

cs.RO↗

arXiv2026

What Limits Vision-and-Language Navigation ?

Vision-and-Language Navigation (VLN) is a cornerstone of embodied intelligence. However, current agents often suffer from significant performance degradation when transitioning from simulation to real-world deployment, primarily due to perceptual instability (e.g., lighting variations and motion blur) and under-specified instructions. While existing methods attempt to bridge this gap by scaling up model size and training data, we argue that the bottleneck lies in the lack of robust spatial grounding and cross-domain priors. In this paper, we propose StereoNav, a robust Vision-Language-Action framework designed to enhance real-world navigation consistency. To address the inherent gap between synthetic training and physical execution, we introduce Target-Location Priors as a persistent bridge. These priors provide stable visual guidance that remains invariant across domains, effectively grounding the agent even when instructions are vague. Furthermore, to mitigate visual disturbances like motion blur and illumination shifts, StereoNav leverages stereo vision to construct a unified representation of semantics and geometry, enabling precise action prediction through enhanced depth awareness. Extensive experiments on R2R-CE and RxR-CE demonstrate that StereoNav achieves state-of-the-art egocentric RGB performance, with SR and SPL scores of 81.1% and 68.3%, and 67.5% and 52.0%, respectively, while using significantly fewer parameters and less training data than prior scaling-based approaches. More importantly, real-world robotic deployments confirm that StereoNav substantially improves navigation reliability in complex, unstructured environments. Project page: https://yunheng-wang.github.io/stereonav-public.github.io.

cs.RO↗

arXiv2026

AutoPDR: Circuit-Aware Solver Configuration Prediction for Hardware Model Checking

Property Directed Reachability (PDR) is a powerful algorithm for formal verification of hardware and software systems, but its performance is highly sensitive to parameter configurations. Manual parameter tuning is time-consuming and requires domain expertise, while traditional automated parameter tuning frameworks are not well-suited for time-sensitive verification tasks like PDR. This paper presents a circuit-aware solver configuration framework that employs graph learning for intelligent heuristic selection in PDR-based verification. Our approach combines graph representations with static circuit features to predict optimal PDR solving configurations for specific circuits. We incorporate expert prior knowledge through constraint-based parameter filtering to eliminate invalid and inefficient configurations and reduce 78% search space. Our feature extraction pipeline captures structural, functional, and connectivity characteristics of circuit topology and component patterns. Experimental evaluation on a comprehensive benchmark suite demonstrates significant performance improvements compared to default configurations and commonly-used settings. The system successfully identifies circuit-specific parameter patterns and automatically selects the most suitable solving strategies based on circuit characteristics, making it a practical tool for automated formal verification workflows.

cs.AR↗

arXiv2026

Morphology-Consistent Humanoid Interaction through Robot-Centric Video Synthesis

Equipping humanoid robots with versatile interaction skills typically requires either extensive policy training or explicit human-to-robot motion retargeting. However, learning-based policies face prohibitive data collection costs. Meanwhile, retargeting relies on human-centric pose estimation (e.g., SMPL), introducing a morphology gap. Skeletal scale mismatches result in severe spatial misalignments when mapped to robots, compromising interaction success. In this work, we propose Dream2Act, a robot-centric framework enabling zero-shot interaction through generative video synthesis. Given a third-person image of the robot and target object, our framework leverages video generation models to envision the robot completing the task with morphology-consistent motion. We employ a high-fidelity pose extraction system to recover physically feasible, robot-native joint trajectories from these synthesized dreams, subsequently executed via a general-purpose whole-body controller. Operating strictly within the robot-native coordinate space, Dream2Act avoids retargeting errors and eliminates task-specific policy training. We evaluate Dream2Act on the Unitree G1 across four whole-body mobile interaction tasks: ball kicking, sofa sitting, bag punching, and box hugging. Dream2Act achieves a 37.5% overall success rate, compared to 0% for conventional retargeting. While retargeting fails to establish correct physical contacts due to the morphology gap (with errors compounded during locomotion), Dream2Act maintains robot-consistent spatial alignment, enabling reliable contact formation and substantially higher task completion.

cs.RO↗

arXiv2026

Iterative Closed-Loop Motion Synthesis for Scaling the Capabilities of Humanoid Control

Physics-based humanoid control relies on training with motion datasets that have diverse data distributions. However, the fixed difficulty distribution of datasets limits the performance ceiling of the trained control policies. Additionally, the method of acquiring high-quality data through professional motion capture systems is constrained by costs, making it difficult to achieve large-scale scalability. To address these issues, we propose a closed-loop automated motion data generation and iterative framework. It can generate high-quality motion data with rich action semantics, including martial arts, dance, combat, sports, gymnastics, and more. Furthermore, our framework enables difficulty iteration of policies and data through physical metrics and objective evaluations, allowing the trained tracker to break through its original difficulty limits. On the PHC single-primitive tracker, using only approximately 1/10 of the AMASS dataset size, the average failure rate on the test set (2201 clips) is reduced by 45% compared to the baseline. Finally, we conduct comprehensive ablation and comparative experiments to highlight the rationality and advantages of our framework.

cs.RO↗

arXiv2026

Spherical Latent Motion Prior for Physics-Based Simulated Humanoid Control

Learning motion priors for physics-based humanoid control is an active research topic. Existing approaches mainly include variational autoencoders (VAE) and adversarial motion priors (AMP). VAE introduces information loss, and random latent sampling may sometimes produce invalid behaviors. AMP suffers from mode collapse and struggles to capture diverse motion skills. We present the Spherical Latent Motion Prior (SLMP), a two-stage method for learning motion priors. In the first stage, we train a high-quality motion tracking controller. In the second stage, we distill the tracking controller into a spherical latent space. A combination of distillation, a discriminator, and a discriminator-guided local semantic consistency constraint shapes a structured latent action space, allowing stable random sampling without information loss. To evaluate SLMP, we collect a two-hour human combat motion capture dataset and show that SLMP preserves fine motion detail without information loss, and random sampling yields semantically valid and stable behaviors. When applied to a two-agent physics-based combat task, SLMP produces human-like and physically plausible combat behaviors only using simple rule-based rewards. Furthermore, SLMP generalizes across different humanoid robot morphologies, demonstrating its transferability beyond a single simulated avatar.

cs.RO↗

arXiv2025

BoolSkeleton: Boolean Network Skeletonization via Homogeneous Pattern Reduction

Boolean equivalence allows Boolean networks with identical functionality to exhibit diverse graph structures. This gives more room for exploration in logic optimization, while also posing a challenge for tasks involving consistency between Boolean networks. To tackle this challenge, we introduce BoolSkeleton, a novel Boolean network skeletonization method that improves the consistency and reliability of design-specific evaluations. BoolSkeleton comprises two key steps: preprocessing and reduction. In preprocessing, the Boolean network is transformed into a defined Boolean dependency graph, where nodes are assigned the functionality-related status. Next, the homogeneous and heterogeneous patterns are defined for the node-level pattern reduction step. Heterogeneous patterns are preserved to maintain critical functionality-related dependencies, while homogeneous patterns can be reduced. Parameter K of the pattern further constrains the fanin size of these patterns, enabling fine-tuned control over the granularity of graph reduction. To validate BoolSkeleton's effectiveness, we conducted four analysis/downstream tasks around the Boolean network: compression analysis, classification, critical path analysis, and timing prediction, demonstrating its robustness across diverse scenarios. Furthermore, it improves above 55% in the average accuracy compared to the original Boolean network for the timing prediction task. These experiments underscore the potential of BoolSkeleton to enhance design consistency in logic synthesis.

cs.AR↗

arXiv2025

CNOT Oriented Synthesis for Small-Scale Boolean Functions Using Spatial Structures of Parallelotopes

Quantum computing has garnered significant interest for its potential to achieve exponential speedups over classical approaches. However, in the Noisy Intermediate-Scale Quantum (NISQ) era, quantum circuit scalability remains limited by gate fidelity and qubit counts, restricting physical implementations to small-scale circuits. While prior work has explored logic network structures for quantum circuit synthesis, these methods often neglect the spatial structure intrinsic to Boolean functions. In this paper, we leverage this spatial structure, encoded by parallelotopes embedded in the hypercube defined by the Boolean function, to access a broader optimization space, enhancing synthesis efficiency and reducing circuit complexity. We propose the Spatial Structure-based Hypercube Reduction~(SSHR), a novel synthesis method tailored for small-scale Boolean functions ($\leq 8$). SSHR extracts global spatial features to minimize the use of Multi-Control Toffoli (MCT) gates. To further exploit spatial correlations, we introduce two variants: SSHR-H employs heuristic functions to accelerate synthesis runtime, while SSHR-I integrates an Integer Linear Programming (ILP) solver to maximize spatial structure utilization. Our approach outperforms existing techniques in small-scale circuit synthesis, achieving 56\% and 81\% reductions in CNOT gate counts compared to the Exclusive Sum-of-Products (ESOP) and Xor-And-Inverter Graph (XAG) methods, respectively.

quant-ph↗

arXiv2025

Wit-HW: Bug Localization in Hardware Design Code via Witness Test Case Generation

Debugging hardware designs requires significant manual effort during hardware development. After engineers identify a bug-triggering test case in simulation-based hardware verification, they usually spend considerable time analyzing the execution trace to localize the bug. Although numerous automated hardware debugging techniques exist, they are not applicable to large designs and deep bugs. A primary reason for their limitations is that these techniques only utilize the information of a single bug-triggering test case for bug localization, which prevents them from effectively analyzing intricate hardware systems and figure out the root cause of bugs. To solve this problem, in this paper, we transform the hardware bug localization problem into a test generation problem, aiming to find a set of effective witness test cases beyond the initial bug-triggering test case to enhance hardware bug localization. Witness test cases refer to the cases that do not trigger the bug in the faulty design. By analyzing the execution differences between passing and failing test cases with spectrum-based method, we can eliminate innocent design statements and localize the buggy ones. To further refine the suspicious area, we define the criteria for effective witness test cases and use a mutation-based strategy to generate such test cases. Based on this approach, we propose an automated hardware bug localization framework named Wit-HW. We evaluate Wit-HW on 41 bugs from various hardware designs. The experimental results show that Wit-HW effectively localize 49%, 73%, 88% bugs within Top-1, Top-5, Top-10 ranks, significantly outperforming state-of-the-art bug localization techniques. Additionally, we evaluate Wit-HW on 13 real-world bugs collected from open-source hardware projects, showcasing the robust performance of our method.

cs.AR↗

arXiv2025

Bridging the Gap between Hardware Fuzzing and Industrial Verification

As hardware design complexity increases, hardware fuzzing emerges as a promising tool for automating the verification process. However, a significant gap still exists before it can be applied in industry. This paper aims to summarize the current progress of hardware fuzzing from an industry-use perspective and propose solutions to bridge the gap between hardware fuzzing and industrial verification. First, we review recent hardware fuzzing methods and analyze their compatibilities with industrial verification. We establish criteria to assess whether a hardware fuzzing approach is compatible. Second, we examine whether current verification tools can efficiently support hardware fuzzing. We identify the bottlenecks in hardware fuzzing performance caused by insufficient support from the industrial environment. To overcome the bottlenecks, we propose a prototype, HwFuzzEnv, providing the necessary support for hardware fuzzing. With this prototype, the previous hardware fuzzing method can achieve a several hundred times speedup in industrial settings. Our work could serve as a reference for EDA companies, encouraging them to enhance their tools to support hardware fuzzing efficiently in industrial verification.

cs.CR↗

arXiv2024

VerilogReader: LLM-Aided Hardware Test Generation

Test generation has been a critical and labor-intensive process in hardware design verification. Recently, the emergence of Large Language Model (LLM) with their advanced understanding and inference capabilities, has introduced a novel approach. In this work, we investigate the integration of LLM into the Coverage Directed Test Generation (CDG) process, where the LLM functions as a Verilog Reader. It accurately grasps the code logic, thereby generating stimuli that can reach unexplored code branches. We compare our framework with random testing, using our self-designed Verilog benchmark suite. Experiments demonstrate that our framework outperforms random testing on designs within the LLM's comprehension scope. Our work also proposes prompt engineering optimizations to augment LLM's understanding scope and accuracy.

cs.SE↗

arXiv2023

Adaptive Reconvergence-driven AIG Rewriting via Strategy Learning

Rewriting is a common procedure in logic synthesis aimed at improving the performance, power, and area (PPA) of circuits. The traditional reconvergence-driven And-Inverter Graph (AIG) rewriting method focuses solely on optimizing the reconvergence cone through Boolean algebra minimization. However, there exist opportunities to incorporate other node-rewriting algorithms that are better suited for specific cones. In this paper, we propose an adaptive reconvergence-driven AIG rewriting algorithm that combines two key techniques: multi-strategy-based AIG rewriting and strategy learning-based algorithm selection. The multi-strategy-based rewriting method expands upon the traditional approach by incorporating support for multi-node-rewriting algorithms, thus expanding the optimization space. Additionally, the strategy learning-based algorithm selection method determines the most suitable node-rewriting algorithm for a given cone. Experimental results demonstrate that our proposed method yields a significant average improvement of 5.567\% in size and 5.327\% in depth.

cs.AI↗

arXiv2023

MEC: An Open-source Fine-grained Mapping Equivalence Checking Tool for FPGA

Technology mapping is an essential step in EDA flow. However, the function of the circuit may be changed after technology mapping, and equivalence checking (EC) based verification is highly necessary. The traditional EC method has significant time and resource constraints, making it only feasible to carry out at a coarse-grained level. To make it efficient for technology mapping, we propose a fine-grained method called MEC, which leverages a combination of two approaches to significantly reduce the time cost of verification. The local block verification approach performs fast verification and the global graph cover approach guarantees correctness. The proposed method is rigorously tested and compared to three EC tools, and the results show that MEC technique offers a substantial improvement in speed. MEC not only offers a faster and more efficient way of performing EC on technology mapping but also opens up new opportunities for more fine-grained verification in the future.

cs.AR↗

arXiv2023

Fast Exact NPN Classification with Influence-aided Canonical Form

NPN classification has many applications in the synthesis and verification of digital circuits. The canonical-form-based method is the most common approach, designing a canonical form as representative for the NPN equivalence class first and then computing the transformation function according to the canonical form. Most works use variable symmetries and several signatures, mainly based on the cofactor, to simplify the canonical form construction and computation. This paper describes a novel canonical form and its computation algorithm by introducing Boolean influence to NPN classification, which is a basic concept in analysis of Boolean functions. We show that influence is input-negation-independent, input-permutation-dependent, and has other structural information than previous signatures for NPN classification. Therefore, it is a significant ingredient in speeding up NPN classification. Experimental results prove that influence plays an important role in reducing the transformation enumeration in computing the canonical form. Compared with the state-of-the-art algorithm implemented in ABC, our influence-aided canonical form for exact NPN classification gains up to 5.5x speedup.

cs.LG↗

arXiv2023

$Radar^2$: Passive Spy Radar Detection and Localization using COTS mmWave Radar

Millimeter-wave (mmWave) radars have found applications in a wide range of domains, including human tracking, health monitoring, and autonomous driving, for their unobtrusive nature and high range accuracy. These capabilities, however, if used for malicious purposes, could also result in serious security and privacy issues. For example, a user's daily life could be secretly monitored by a spy radar. Hence, there is a strong urge to develop systems that can detect and locate such spy radars. In this paper, we propose $Radar^2$, a practical system for passive spy radar detection and localization using a single commercial off-the-shelf (COTS) mmWave radar. Specifically, we propose a novel \textit{Frequency Component Detection} method to detect the existence of mmWave signals, distinguish between mmWave radar and WiGig signals using a waveform classifier based on a convolutional neural network (CNN), and localize spy radars using triangulation based on the detector's observations at multiple anchor points. Not only does $Radar^2$ work for different types of mmWave radar, but it can also detect and localize multiple radars simultaneously. Finally, we performed extensive experiments to evaluate the effectiveness and robustness of $Radar^2$ in various settings. Our evaluation results show that the radar detection rate is above 96$\%$ and the localization error is within 0.3m. The results also reveal that $Radar^2$ is robust against various environmental factors (e.g., room layout and human activities).

eess.SP↗

arXiv2023

Rethinking NPN Classification from Face and Point Characteristics of Boolean Functions

NPN classification is an essential problem in the design and verification of digital circuits. Most existing works explored variable symmetries and cofactor signatures to develop their classification methods. However, cofactor signatures only consider the face characteristics of Boolean functions. In this paper, we propose a new NPN classifier using both face and point characteristics of Boolean functions, including cofactor, influence, and sensitivity. The new method brings a new perspective to the classification of Boolean functions. The classifier only needs to compute some signatures, and the equality of corresponding signatures is a prerequisite for NPN equivalence. Therefore, these signatures can be directly used for NPN classification, thus avoiding the exhaustive transformation enumeration. The experiments show that the proposed NPN classifier gains better NPN classification accuracy with comparable speed.

cs.CC↗

arXiv2021

Enhanced Fast Boolean Matching based on Sensitivity Signatures Pruning

Boolean matching is significant to digital integrated circuits design. An exhaustive method for Boolean matching is computationally expensive even for functions with only a few variables, because the time complexity of such an algorithm for an n-variable Boolean function is $O(2^{n+1}n!)$. Sensitivity is an important characteristic and a measure of the complexity of Boolean functions. It has been used in analysis of the complexity of algorithms in different fields. This measure could be regarded as a signature of Boolean functions and has great potential to help reduce the search space of Boolean matching. In this paper, we introduce Boolean sensitivity into Boolean matching and design several sensitivity-related signatures to enhance fast Boolean matching. First, we propose some new signatures that relate sensitivity to Boolean equivalence. Then, we prove that these signatures are prerequisites for Boolean matching, which we can use to reduce the search space of the matching problem. Besides, we develop a fast sensitivity calculation method to compute and compare these signatures of two Boolean functions. Compared with the traditional cofactor and symmetric detection methods, sensitivity is a series of signatures of another dimension. We also show that sensitivity can be easily integrated into traditional methods and distinguish the mismatched Boolean functions faster. To the best of our knowledge, this is the first work that introduces sensitivity to Boolean matching. The experimental results show that sensitivity-related signatures we proposed in this paper can reduce the search space to a very large extent, and perform up to 3x speedup over the state-of-the-art Boolean matching methods.

cs.CC↗