arXiv subjects

Xiaofeng Zhou

Publications and source records attributed to Xiaofeng Zhou.

18 recordsLinked to original sources

arXiv2026

NeuroAbs: A Neuro-Symbolic RTL Abstraction Framework for Property Checking Acceleration

Formal verification is a crucial technique for ensuring the functional correctness of hardware designs. In the context of property checking, a key challenge is how to efficiently prove a user-specified property in the face of increasingly complex RTL designs. To address this challenge, abstraction techniques are often employed to reduce system complexity and accelerate the verification process. However, prior RTL abstraction methods either require significant manual effort or rely on rule-based techniques that lack flexibility. This paper introduces NeuroAbs, a neuro-symbolic framework for RTL abstraction. NeuroAbs first uses LLM-assisted RTL analysis to identify signals suitable for abstraction. It then combines LLM-based abstraction with an AST-based symbolic RTL representation to better align the generated abstraction with the intended transformation. The soundness of each abstraction is checked using satisfiability modulo theories (SMT) solving. If the abstraction is too coarse for a successful proof, NeuroAbs applies counterexample-guided abstraction refinement (CEGAR) to iteratively refine the model. Experimental results show that NeuroAbs significantly improves the efficiency of hardware property checking across a range of verification tasks.

cs.AR↗

arXiv2026

A-IC3: Learning-Guided Adaptive Inductive Generalization for Hardware Model Checking

The IC3 algorithm represents the state-of-the-art (SOTA) hardware model checking technique, owing to its robust performance and scalability. A significant body of research has focused on enhancing the solving efficiency of the IC3 algorithm, with particular attention to the inductive generalization process: a critical phase wherein the algorithm seeks to generalize a counterexample to inductiveness (CTI), which typically is a state leading to a bad state, into a broader set of states. This inductive generalization is a primary source of clauses in IC3 and thus plays a pivotal role in determining the overall effectiveness of the algorithm. Despite its importance, existing approaches often rely on fixed inductive generalization strategies, overlooking the dynamic and context-sensitive nature of the verification environment in which spurious counterexamples arise. This rigidity can limit the quality of generated clauses and, consequently, the performance of IC3. To address this limitation, we propose a lightweight machine-learning-based framework that dynamically selects appropriate inductive generalization strategies in response to the evolving verification context. Specifically, we employ a multi-armed bandit (MAB) algorithm to adaptively choose inductive generalization strategies based on real-time feedback from the verification process. The agent is updated by evaluating the quality of generalization outcomes, thereby refining its strategy selection over time. Empirical evaluation on a benchmark suite comprising 914 instances, primarily drawn from the latest HWMCC collection, demonstrates the efficacy of our approach. When implemented on the state-of-the-art model checker rIC3, our method solves 26 to 50 more cases than the baselines and improves the PAR-2 score by 194.72 to 389.29.

cs.LO↗

arXiv2026

HiFuzz: Hierarchical Reinforcement Learning for Semantic-Aware and Adaptive CPU Fuzzing

Modern processor verification struggles to reach deep architectural states due to the inefficiencies of traditional mutation-based fuzzing. We propose HiFuzz, a novel hierarchical reinforcement learning framework that replaces mutation with a structured, two-layer generation process: a Program Agent for global layout and a Basic Block Agent for precise instruction filling. To overcome reward sparsity, HiFuzz integrates an adaptive coverage reward mechanism and a semantic-aware basic block encoder providing intrinsic feedback. Extensive evaluations on three real-world RISC-V cores demonstrate that HiFuzz significantly outperforms state-of-the-art fuzzers in coverage and bug detection.

cs.AR↗

arXiv2026

AutoINV: Automated Invariant Generation Framework for Formal Verification on High-Level Synthesis Designs

High-level synthesis (HLS) transforms an algorithmic description of hardware from a higher abstraction (e.g., C/C++) into a register-transfer level (RTL) design, offering reduced development time and greater flexibility in design space exploration. However, such machine-generated RTL designs may contain major functional bugs or security vulnerabilities due to limitations or errors in the HLS tools. One of the most reliable methods to identify these vulnerabilities is formal verification, particularly model checking. Nevertheless, the large size of the generated RTL often causes model checking to struggle to conclude within reasonable time or resource limits. In this study, we propose utilizing the high-level design features from the HLS flow to construct a set of helper assertions aimed at guiding the model checker and accelerating the verification process. To identify the most effective set of helpers to assist the model checker, we develop a proving mechanism that iteratively reuses proving information to select the potentially most useful set of helpers. We evaluate the proposed framework on a set of HLS design benchmarks. Experimental results demonstrate that, when compared to vanilla model checking, our approach achieves a speedup of up to 6.05x, and 2.23x on average.

cs.AR↗

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

FPPS: An FPGA-Based Point Cloud Processing System

Point cloud processing is a computational bottleneck in autonomous driving systems, especially for real-time applications, while energy efficiency remains a critical system constraint. This work presents FPPS, an FPGA-accelerated point cloud processing system designed to optimize the iterative closest point (ICP) algorithm, a classic cornerstone of 3D localization and perception pipelines. Evaluated on the widely used KITTI benchmark dataset, the proposed system achieves up to 35$\times$ (and a runtime-weighted average of 15.95x) speedup over a state-of-the-art CPU baseline while maintaining equivalent registration accuracy. Notably, the design improves average power efficiency by 8.58x, offering a compelling balance between performance and energy consumption. These results position FPPS as a viable solution for resource-constrained embedded autonomous platforms where both latency and power are key design priorities.

cs.AR↗

arXiv2026

EvolveGen: Algorithmic Level Hardware Model Checking Benchmark Generation through Reinforcement Learning

Progress in hardware model checking depends critically on high-quality benchmarks. However, the community faces a significant benchmark gap: existing suites are limited in number, often distributed only in representations such as BTOR2 without access to the originating register-transfer-level (RTL) designs, and biased toward extreme difficulty where instances are either trivial or intractable. These limitations hinder rigorous evaluation of new verification techniques and encourage overfitting of solver heuristics to a narrow set of problems. To address this, we introduce EvolveGen, a framework for generating hardware model checking benchmarks by combining reinforcement learning (RL) with high-level synthesis (HLS). Our approach operates at an algorithmic level of abstraction in which an RL agent learns to construct computation graphs. By compiling these graphs under different synthesis directives, we produce pairs of functionally equivalent but structurally distinct hardware designs, inducing challenging model checking instances. Solver runtime is used as the reward signal, enabling the agent to autonomously discover and generate small-but-hard instances that expose solver-specific weaknesses. Experiments show that EvolveGen efficiently creates a diverse benchmark set in standard formats (e.g., AIGER and BTOR2) and effectively reveals performance bottlenecks in state-of-the-art model checkers.

cs.AR↗

arXiv2025

FORWORD: Accelerating Formal Datapath Verification via Word-Level Sweeping

Modern circuit design process increasingly adopts high-level hardware construction languages and parameterized design methodologies to shorten development cycles and maintain high reusability, in contrast to traditional hardware description languages. Such designs often involve complex datapath with arithmetic operations, wide bit-vectors, and on-chip memories, whose scale and level of modeling often pose significant challenges to formal datapath verification. Traditional bit-level SAT sweeping techniques lack the necessary abstraction and adaptability that are required to establish equivalence at a higher level. In this paper, we propose FORWORD, a novel word-level sweeping verification engine tailored explicitly to formal datapath verification. FORWORD integrates randomized and constraint-driven word-level simulations, leveraging adaptive optimization to dynamically refine equivalent candidates identified during simulation. Experimental results demonstrate that FORWORD significantly outperforms state-of-the-art bit-level SAT sweeping engines and the monolithic SMT solving method, thanks to its enhanced capability in effectively identifying equivalent pairs. To the best of our knowledge, FORWORD is the first word-level sweeping engine explicitly designed for datapath verification, offering improved efficiency and adaptability to modern circuit designs.

cs.LO↗

arXiv2025

Free-form conformal metasurfaces robustly generating topological skyrmions

Skyrmions are topologically stable vector textures as potential information carriers for high-density data storage and communications, especially boosted by the recently emerging meta-generators of skyrmions in electromagnetic fields. However, these implementations always rely on planar, rigid designs with stringent fabrication requirements. Here, we propose the free-form conformal metasurface generating skyrmions towards future wearable and flexible devises for topological resilience light fields. Furthermore, we experimentally tested the outstanding topological robustness of the skyrmion number under different disorder degrees on the metasurface. This work promotes the development of flexible compact skyrmion-based communication devices and demonstrates their potential to improve the quality of space information transmission.

physics.optics↗

arXiv2025

Debate, Reflect, and Distill: Multi-Agent Feedback with Tree-Structured Preference Optimization for Efficient Language Model Enhancement

Large Language Models (LLMs) continue to set new standards in knowledge-intensive and complex reasoning tasks, yet their high computational demands limit widespread adoption. While distilling large models into smaller ones offers a sustainable solution, current techniques--such as static knowledge distillation, resource-intensive reinforcement learning from human feedback, or limited self-reflection--struggle to yield substantial and lasting performance gains. In this paper, we present a novel Debate and Reflect (D&R) framework that orchestrates multi-turn debates between smaller models and stronger teacher models, eliciting actionable feedback (e.g., error analysis, corrective strategies) to guide student models. Further, we introduce Tree-structured Direct Preference Optimization (T-DPO) to efficiently leverage these debate logs, organizing interactions into a hierarchical format for effective training. Empirical evaluations across diverse NLP benchmarks demonstrate that our approach significantly improves smaller-model accuracy, robustness, and generalization, outperforming conventional baselines by a large margin.

cs.CL↗

arXiv2021

Cluster magnetic octupole induced out-of-plane spin polarization in antiperovskite antiferromagnet

Out-of-plane spin polarization σ_z has attracted increasing interests of researchers recently, due to its potential in high-density and low-power spintronic devices. Noncollinear antiferromagnet (AFM), which has unique 120° triangular spin configuration, has been discovered to possess σ_z. However, the physical origin of σ_z in noncollinear AFM is still not clear, and the external magnetic field-free switching of perpendicular magnetic layer using the corresponding σ_z has not been reported yet. Here, we use the cluster magnetic octupole in antiperovskite AFM Mn3SnN to demonstrate the generation of σ_z. σ_z is induced by the precession of carrier spins when currents flow through the cluster magnetic octupole, which also relies on the direction of the cluster magnetic octupole in conjunction with the applied current. With the aid of σ_z, current induced spin-orbit torque (SOT) switching of adjacent perpendicular ferromagnet is realized without external magnetic field. Our findings present a new perspective to the generation of out-of-plane spin polarizations via noncollinear AFM spin structure, and provide a potential path to realize ultrafast high-density applications.

cond-mat.mtrl-sci↗

arXiv2021

Magnon-mediated interlayer coupling in an all-antiferromagnetic junction

The interlayer coupling mediated by fermions in ferromagnets brings about parallel and anti-parallel magnetization orientations of two magnetic layers, resulting in the giant magnetoresistance, which forms the foundation in spintronics and accelerates the development of information technology. However, the interlayer coupling mediated by another kind of quasi-particle, boson, is still lacking. Here we demonstrate such a static interlayer coupling at room temperature in an antiferromagnetic junction Fe2O3/Cr2O3/Fe2O3, where the two antiferromagnetic Fe2O3 layers are functional materials and the antiferromagnetic Cr2O3 layer serves as a spacer. The Néel vectors in the top and bottom Fe2O3 are strongly orthogonally coupled, which is bridged by a typical bosonic excitation (magnon) in the Cr2O3 spacer. Such an orthogonally coupling exceeds the category of traditional collinear interlayer coupling via fermions in ground state, reflecting the fluctuating nature of the magnons, as supported by our magnon quantum well model. Besides the fundamental significance on the quasi-particle-mediated interaction, the strong coupling in an antiferromagnetic magnon junction makes it a realistic candidate for practical antiferromagnetic spintronics and magnonics with ultrahigh-density integration.

cond-mat.mtrl-sci↗

arXiv2020

Current-induced in-plane magnetization switching in biaxial ferrimagnetic insulator

Ferrimagnetic insulators (FiMI) have been intensively used in microwave and magneto-optical devices as well as spin caloritronics, where their magnetization direction plays a fundamental role on the device performance. The magnetization is generally switched by applying external magnetic fields. Here we investigate current-induced spin-orbit torque (SOT) switching of the magnetization in Y3Fe5O12 (YIG)/Pt bilayers with in-plane magnetic anisotropy, where the switching is detected by spin Hall magnetoresistance. Reversible switching is found at room temperature for a threshold current density of 10^7 A cm^-2. The YIG sublattices with antiparallel and unequal magnetic moments are aligned parallel or antiparallel to the direction of current pulses, which is consistent to the Neel order switching in antiferromagnetic system. It is proposed that such a switching behavior may be triggered by the antidamping-torque acting on the two antiparallel sublattices of FiMI. Our finding not only broadens the magnetization switching by electrical means and promotes the understanding of magnetization switching, but also paves the way for all-electrically modulated microwave devices and spin caloritronics with low power consumption.

cond-mat.mtrl-sci↗

arXiv2019

Polar Codes with Memory

Polar codes with memory (PCM) are proposed in this paper: a pair of consecutive code blocks containing a controlled number of mutual information bits. The shared mutual information bits of the succeeded block can help the failed block to recover. The underlying polar codes can employ any decoding scheme such as the successive cancellation (SC) decoding (PCM-SC), the belief propagation (BP) decoding (PCM-BP), and the successive cancellation list (SCL) decoding (PCM-SCL). The analysis shows that the packet error rate (PER) of PCM decreases to the order of PER squared while maintaining the same complexity as the underlying polar codes. Simulation results indicate that for PCM-SC, the PER is comparable to (less than 0.3 dB) the stand-alone SCL decoding with two lists for the block length $N=256$. The PER of PCM-SCL with $L$ lists can match that of the stand-alone SCL decoding with $2L$ lists. Two hardware decoders for PCM are also implemented: the in-serial (IS) decoder and the low-latency interleaved (LLI) decoder. For $N=256$, synthesis results show that in the worst case, the latency of the PCM LLI decoder is only $16.1\%$ of the adaptive SCL decoder with $L=2$, while the throughput is improved by 13 times compared to it.

cs.IT↗

arXiv2019

Mining Rules Incrementally over Large Knowledge Bases

Multiple web-scale Knowledge Bases, e.g., Freebase, YAGO, NELL, have been constructed using semi-supervised or unsupervised information extraction techniques and many of them, despite their large sizes, are continuously growing. Much research effort has been put into mining inference rules from knowledge bases. To address the task of rule mining over evolving web-scale knowledge bases, we propose a parallel incremental rule mining framework. Our approach is able to efficiently mine rules based on the relational model and apply updates to large knowledge bases; we propose an alternative metric that reduces computation complexity without compromising quality; we apply multiple optimization techniques that reduce runtime by more than 2 orders of magnitude. Experiments show that our approach efficiently scales to web-scale knowledge bases and saves over 90% time compared to the state-of-the-art batch rule mining system. We also apply our optimization techniques to the batch rule mining algorithm, reducing runtime by more than half compared to the state-of-the-art. To the best of our knowledge, our incremental rule mining system is the first that handles updates to web-scale knowledge bases.

cs.DB↗

arXiv2018

Electric field switching of the uniaxial magnetic anisotropy of an antiferromagnet

Electric field control of magnetic anisotropy in ferromagnets has been intensively pursued in spintronics to achieve efficient memory and computing devices with low energy consumption. Compared with ferromagnets, antiferromagnets hold huge potential in high-density information storage for their ultrafast spin dynamics and vanishingly small stray field. However, the switching of magnetic anisotropy of antiferromagnets via electric field remains elusive. Here we use ferroelastic strain from piezoelectric materials to switch the uniaxial magnetic anisotropy and the Néel order reversibly in antiferromagnetic Mn2Au films with an electric field of only a few kV/cm at room temperature. Owing to the uniaxial magnetic anisotropy, a ratchet-like switching behavior driven by the Néel spin-orbit torque is observed in the Mn2Au, which can be reversed by electric fields.

cond-mat.mtrl-sci↗

arXiv2018

Observation of Anomalous Hall Effect in Noncollinear Antiferromagnetic Mn3Sn Films

Magnetotransport is at the center of the spintronics. Mn3Sn, an antiferromagnet that has a noncollinear 120° spin order, exhibits large anomalous Hall effect (AHE) at room temperature. But such a behavior has been remained elusive in Mn3Sn films. Here we report the observation of robust AHE up to room temperature in quasi-epitaxial Mn3Sn thin films, prepared by magnetron sputtering. The growth of both (11-20)- and (0001)-oriented Mn3Sn films provides a unique opportunity for comparing AHE in three different measurement configurations. When the magnetic field is swept along (0001) plane, such as the direction of [01-10] and [2-1-10] the films show comparatively higher anomalous Hall conductivity than its perpendicular counterpart ([0001]), irrespective of their respectively orthogonal current along [0001] or [01-10]. A quite weak ferromagnetic moment of 3 emu/cm^3 is obtained in (11-20)-oriented Mn3Sn films, guaranteeing the switching of the Hall signals with magnetization reversal. Our finding would advance the integration of Mn3Sn in antiferromagnetic spintronics.

cond-mat.mtrl-sci↗

arXiv2018

How to manipulate magnetic states of antiferromagnets

Antiferromagnetic materials, which have drawn considerable attention recently, have fascinating features: they are robust against perturbation, produce no stray fields, and exhibit ultrafast dynamics. Discerning how to efficiently manipulate the magnetic state of an antiferromagnet is key to the development of antiferromagnetic spintronics. In this review, we introduce four main methods (magnetic, strain, electrical, and optical) to mediate the magnetic states and elaborate on intrinsic origins of different antiferromagnetic materials. Magnetic control includes a strong magnetic field, exchange bias, and field cooling, which are traditional and basic. Strain control involves the magnetic anisotropy effect or metamagnetic transition. Electrical control can be divided into two parts, electric field and electric current, both of which are convenient for practical applications. Optical control includes thermal and electronic excitation, an inertia-driven mechanism, and terahertz laser control, with the potential for ultrafast antiferromagnetic manipulation. This review sheds light on effective usage of antiferromagnets and provides a new perspective on antiferromagnetic spintronics.

cond-mat.mtrl-sci↗