arXiv subjects

Yonghao Wang

Publications and source records attributed to Yonghao Wang.

At least 19 recordsLinked to original sources

arXiv2026

Rtl2lean: Automated RTL-to-Lean Translation with Hierarchical Theorem Generation and Lemma Reuse

Formal verification with interactive theorem provers can provide strong correctness guarantees for register transfer level designs, but applying it to existing SystemVerilog code requires substantial manual effort in semantic modeling and proof construction. This paper presents Rtl2lean, a framework that automatically translates RTL designs into executable Lean 4 models and builds a hierarchical theorem library for subsequent verification. The generated model represents hardware execution as a pure state transition function, while a four layer theorem framework captures combinational semantics, sequential updates, single cycle behavior, and reachability and invariants. When a high level property cannot be discharged by the existing theorem base, an LLM based proving loop proposes intermediate lemmas from the current proof context and Lean feedback. Only lemmas accepted by the Lean kernel are added to the reusable lemma pool. Experiments on six SystemVerilog designs generate 403 theorems, all of which are successfully checked by Lean. Among 358 foundational lemmas, 287 are available for automatic reuse, yielding a reusable lemma ratio of 80.2 percent. The results demonstrate that Rtl2lean can construct machine checked RTL proof libraries with low checking overhead and substantial cross property lemma reuse.

cs.AR↗

arXiv2026

Arcane: An Assertion Reduction Framework through Semantic Clustering and MCTS-Guided Rule Exploring

Assertion-based Verification (ABV) is essential for ensuring that hardware designs conform to their intended specifications. However, existing automated assertion-generation approaches, such as LLM-based frameworks, often generate large numbers of redundant assertions, which significantly degrade simulation efficiency. To mitigate the simulation overhead caused by redundant assertions, this paper proposes Arcane, an efficient assertion reduction framework. It integrates a two-tier assertion clustering approach for accurate semantic classification of large assertion sets, and employs Monte Carlo Tree Search (MCTS) to explore optimal rule-application sequences for efficient assertion reduction. The experimental results on Assertionbench [20] show that Arcane achieves a reduction of up to 76.2% in the assertion count while fully preserving formal coverage and mutation-detection ability. Further simulation studies demonstrate a speedup of 2.6x to 6.1x speedup in simulation time. The proposed framework is released at https://anonymous.4open.science/r/Arcane1-0A6F/.

cs.AI↗

arXiv2026

From Indiscriminate to Targeted: Functionally Critical Signal-Driven Assertion Generation using LLMs for Efficient RTL Verification

Functional verification has become the most time-consuming phase in IC development, and Assertion-Based Verification (ABV) is key to reducing debugging time. However, existing LLM-based assertion generation methods typically pursue indiscriminate verification, aiming for maximal coverage without considering signal criticality, whereas industrial practice demands maximizing coverage with minimal verification cost. Consequently, identifying signals that have the greatest impact on design functionality and error propagation-enabling a shift from indiscriminate to targeted verification-remains a key challenge. To address this, we propose AgileAssert, a key signal-driven assertion generation framework that constructs RTL semantic graphs and identifies the top-K critical signals via a hybrid scoring and selection mechanism, followed by structure-aware RTL slicing to provide the LLM with precise targets and contextual information, thereby guiding LLMs to generate tightly constrained targeted assertions for efficient verification. Evaluated on block- and CPU-level designs, with an average 66.68% reduction in assertions, our approach outperforms three existing SOTA methods, and significantly improving coverage metrics while reducing input token consumption by 64%. In mutation testing, when our approach surpasses existing methods in error detection rate, the average number of assertions used decreases by 72.74%.

cs.AR↗

arXiv2026

CoverAssert: Iterative LLM Assertion Generation Driven by Functional Coverage via Syntax-Semantic Representations

LLMs can generate SystemVerilog assertions (SVAs) from natural language specs, but single-pass outputs often lack functional coverage due to limited IC design understanding. We propose CoverAssert, an iterative framework that clusters semantic and AST-based structural features of assertions, maps them to specifications, and uses functional coverage feedback to guide LLMs in prioritizing uncovered points. Experiments on four open-source designs show that integrating CoverAssert with AssertLLM and Spec2Assertion improves average improvements of 9.57 % in branch coverage, 9.64 % in statement coverage, and 15.69 % in toggle coverage.

cs.AR↗

arXiv2026

RTLSeek: Boosting the LLM-Based RTL Generation with Multi-Stage Diversity-Oriented Reinforcement Learning

Register Transfer Level (RTL) design translates high-level specifications into hardware using HDLs such as Verilog. Although LLM-based RTL generation is promising, the scarcity of functionally verifiable high-quality data limits both accuracy and diversity. Existing post-training typically produces a single HDL implementation per specification, lacking awareness of RTL variations needed for different design goals. We propose RTLSeek, a post-training paradigm that applies rule-based Diversity-Oriented Reinforcement Learning to improve RTL correctness and diversity. Our Diversity-Centric Multi-Objective Reward Scheduling integrates expert knowledge with EDA feedback, and a three-stage framework maximizes the utility of limited data. Experiments on the RTLLM benchmark show that RTLSeek surpasses prior methods, with ablation results confirming that encouraging broader design-space exploration improves RTL quality and achieves the principle of "the more generated, the better results." Implementation framework, including the dataset, source code, and model weights, is shown at https://anonymous.4open.science/r/DAC2026ID71-ACB4/.

cs.AR↗

arXiv2026

Constraining the presence of exotrojans in hot Jupiter systems using TTV observations from TESS

Co-orbital bodies (Trojans) share a 1:1 mean-motion resonance with a planet. Although Trojans are common in the Solar System, none has yet been confirmed in an exoplanetary system. Hot Jupiters are not expected to retain primordial co-orbitals efficiently, but their deep and frequent transits make them favorable targets for observational constraints using transit timing variations (TTVs). As part of the ExoEcho project, we analyze TESS photometry for 260 confirmed hot Jupiters with published RV-based masses to search for TTV signals compatible with Trojan companions. We derive transit times and compare the observed residuals with co-orbital models computed with REBOUND N-body simulations. Accounting for the degeneracy between Trojan mass and libration amplitude, we place upper mass limits on possible companions over a range of typical libration amplitudes. For a representative libration amplitude of 15 deg, we rule out exotrojans more massive than 1 Earth mass in 130 systems, corresponding to about 50% of the sample. A more conservative chi-square analysis that incorporates observational uncertainties raises this threshold to 3 Earth masses. We further combine these limits with dynamical-stability constraints for the 1:1 resonance to exclude unstable configurations. Our results provide population-level constraints on massive exotrojans in short-period systems and establish a framework for future high-precision searches with missions such as PLATO and ET (Earth 2.0).

astro-ph.EP↗

arXiv2026

Iterative LLM-Based Assertion Generation Using Syntax-Semantic Representations for Functional Coverage-Guided Verification

While leveraging LLMs to automatically generate SystemVerilog assertions (SVAs) from natural language specifications holds great potential, existing techniques face a key challenge: LLMs often lack sufficient understanding of IC design, leading to poor assertion quality in a single pass. Therefore, verifying whether the generated assertions effectively cover the functional specifications and designing feedback mechanisms based on this coverage remain significant hurdles. To address these limitations, this paper introduces CoverAssert, a novel iterative framework for optimizing SVA generation with LLMs. The core contribution is a lightweight mechanism for matching generated assertions with specific functional descriptions in the specifications. CoverAssert achieves this by clustering the joint representations of semantic features of LLM-generated assertions and structural features extracted from abstract syntax trees (ASTs) about signals related to assertions, and then mapping them back to the specifications to analyze functional coverage quality. Leveraging this capability, CoverAssert constructs a feedback loop based on functional coverage to guide LLMs in prioritizing uncovered functional points, thereby iteratively improving assertion quality. Experimental evaluations on four open-source designs demonstrate that integrating CoverAssert with state-of-the-art generators, AssertLLM and Spec2Assertion, achieves average improvements of 9.57 % in branch coverage, 9.64 % in statement coverage, and 15.69 % in toggle coverage.

cs.AR↗

arXiv2025

Think with Self-Decoupling and Self-Verification: Automated RTL Design with Backtrack-ToT

Large language models (LLMs) hold promise for automating integrated circuit (IC) engineering using register transfer level (RTL) hardware description languages (HDLs) like Verilog. However, challenges remain in ensuring the quality of Verilog generation. Complex designs often fail in a single generation due to the lack of targeted decoupling strategies, and evaluating the correctness of decoupled sub-tasks remains difficult. While the chain-of-thought (CoT) method is commonly used to improve LLM reasoning, it has been largely ineffective in automating IC design workflows, requiring manual intervention. The key issue is controlling CoT reasoning direction and step granularity, which do not align with expert RTL design knowledge. This paper introduces VeriBToT, a specialized LLM reasoning paradigm for automated Verilog generation. By integrating Top-down and design-for-verification (DFV) approaches, VeriBToT achieves self-decoupling and self-verification of intermediate steps, constructing a Backtrack Tree of Thought with formal operators. Compared to traditional CoT paradigms, our approach enhances Verilog generation while optimizing token costs through flexible modularity, hierarchy, and reusability.

cs.AR↗

arXiv2025

AssertMiner: Module-Level Spec Generation and Assertion Mining using Static Analysis Guided LLMs

Assertion-based verification (ABV) is a key approach to checking whether a logic design complies with its architectural specifications. Existing assertion generation methods based on design specifications typically produce only top-level assertions, overlooking verification needs on the implementation details in the modules at the micro-architectural level, where design errors occur more frequently. To address this limitation, we present AssertMiner, a module-level assertion generation framework that leverages static information generated from abstract syntax tree (AST) to assist LLMs in mining assertions. Specifically, it performs AST-based structural extraction to derive the module call graph, I/O table, and dataflow graph, guiding the LLM to generate module-level specifications and mine module-level assertions. Our evaluation demonstrates that AssertMiner outperforms existing methods such as AssertLLM and Spec2Assertion in generating high-quality assertions for modules. When integrated with these methods, AssertMiner can enhance the structural coverage and significantly improve the error detection capability, enabling a more comprehensive and efficient verification process.

cs.AR↗

arXiv2025

AssertGen: Enhancement of LLM-aided Assertion Generation through Cross-Layer Signal Bridging

Assertion-based verification (ABV) serves as a crucial technique for ensuring that register-transfer level (RTL) designs adhere to their specifications. While Large Language Model (LLM) aided assertion generation approaches have recently achieved remarkable progress, existing methods are still unable to effectively identify the relationship between design specifications and RTL designs, which leads to the insufficiency of the generated assertions. To address this issue, we propose AssertGen, an assertion generation framework that automatically generates SystemVerilog assertions (SVA). AssertGen first extracts verification objectives from specifications using a chain-of-thought (CoT) reasoning strategy, then bridges corresponding signals between these objectives and the RTL code to construct a cross-layer signal chain, and finally generates SVAs based on the LLM. Experimental results demonstrate that AssertGen outperforms the existing state-of-the-art methods across several key metrics, such as pass rate of formal property verification (FPV), cone of influence (COI), proof core and mutation testing coverage.

cs.AR↗

arXiv2025

AssertFix: Empowering Automated Assertion Fix via Large Language Models

Assertion-based verification (ABV) is critical in ensuring that register-transfer level (RTL) designs conform to their functional specifications. SystemVerilog Assertions (SVA) effectively specify design properties, but writing and maintaining them manually is challenging and error-prone. Although recent progress of assertion generation methods leveraging large language models (LLMs) have shown great potential in improving assertion quality, they typically treat assertion generation as a final step, leaving the burden of fixing of the incorrect assertions to human effects, which may significantly limits the application of these methods. To address the above limitation, we propose an automatic assertion fix framework based on LLMs, named AssertFix. AsserFix accurately locates the RTL code related to the incorrect assertion, systematically identifies the root causes of the assertion errors, classifies the error type and finally applies dedicated fix strategies to automatically correct these errors, improving the overall quality of the generated assertions. Experimental results show that AssertFix achieves noticeable improvements in both fix rate and verification coverage across the Opencore benchmarks.

cs.AR↗

arXiv2025

DeepAssert: An LLM-Aided Verification Framework with Fine-Grained Assertion Generation for Modules with Extracted Module Specifications

Assertion-Based Verification (ABV) is a crucial method for ensuring that logic designs conform to their architectural specifications. However, existing assertion generation methods primarily rely on information either from the design specification, or register-transfer level (RTL) code. The former methods are typically limited to generating assertions for the top-level design. As the top-level design is composed of different modules without module-level specifications, they are unable to generate deep assertions that target the internal functionality of modules. The latter methods often rely on a golden RTL model, which is difficult to obtain. To address the above limitations, this paper presents a novel large language model (LLM)-aided verification framework named DeepAssert. DeepAssert is capable of analyzing the invocation relationships between modules and extracting independent specifications for each module with its I/O port information. These extracted specifications are subsequently used to guide LLMs to automatically generate fine-grained deep assertions for these modules. Our evaluation demonstrates that DeepAssert significantly outperforms existing methods such as AssertLLM and Spec2Assertion in generating high-quality deep assertions for modules. Furthermore, when integrated with these methods, DeepAssert can enhance the overall quality of the assertions generated. This allows for a more comprehensive and effective verification process.

cs.AR↗

arXiv2025

HST/WFC3 Constraints on the Abundances of OH and FeH in the Atmosphere of the Ultra-Hot Neptune LTT-9779 b

Planets residing within the hot-Neptune Desert are rare, and studying their atmospheres can provide valuable insights into their formation and evolutionary processes. We present the atmospheric characterization of the first known ultra-hot Neptune, LTT-9779 b, using transmission spectroscopic observations obtained with the HST/WFC3 G141 and G102 grisms. Using the Iraclis pipeline and TauREx3 retrieval code, we find that LTT-9779 b likely possesses a H/He-dominated primary atmosphere with an opaque aerosol layer and the pure cloudy, flat-line model is rejected with approximately 2.7-$\sigma$ confidence. Although we do not find conclusive evidence supporting the presence of any molecular species, we place 95% confidence level upper limits on the volume mixing ratios (VMRs) of hydroxyl radical (OH) and iron hydride (FeH) at $7.18\times10^{-2}$ and $1.52\times10^{-8}$, respectively. Notably, the retrieval results are inconsistent with predictions from equilibrium chemistry models, which favor higher $\rm H_2O$ abundances over OH. This discrepancy suggests that disequilibrium processes, such as photochemistry or vertical mixing, may have altered the atmospheric composition. Comparisons between HST, Spitzer and JWST data reveal no evidence of temporal variations in the atmospheric composition of the terminator region. Our results highlight the need for higher-resolution spectroscopy and secondary eclipse observations to resolve LTT-9779 b's temperature-pressure (T-P) profile and chemical inventory definitively.

astro-ph.EP↗

arXiv2025

Supporting Urban Low-Altitude Economy: Channel Gain Map Inference Based on 3D Conditional GAN

The advancement of advanced air mobility (AAM) in recent years has given rise to the concept of low-altitude economy (LAE). However, the diverse flight activities associated with the emerging LAE applications in urban scenarios confront complex physical environments, which urgently necessitates ubiquitous and reliable communication to guarantee the operation safety of the low-altitude aircraft. As one of promising technologies for the sixth generation (6G) mobile networks, channel knowledge map (CKM) enables the environment-aware communication by constructing a site-specific dataset, thereby providing a priori on-site information for the aircraft to obtain the channel state information (CSI) at arbitrary locations with much reduced online overhead. Diverse base station (BS) deployments in the three-dimensional (3D) urban low-altitude environment require efficient 3D CKM construction to capture spatial channel characteristics with less overhead. Towards this end, this paper proposes a 3D channel gain map (CGM) inference method based on a 3D conditional generative adversarial network (3D-CGAN). Specifically, we first analyze the potential deployment types of BSs in urban low-altitude scenario, and investigate the CGM representation with the corresponding 3D channel gain model. The framework of the proposed 3D-CGAN is then discussed, which is trained by a dataset consisting of existing CGMs. Consequently, the trained 3D-CGAN is capable of inferring the corresponding CGM only based on the BS coordinate without additional measurement. The simulation results demonstrate that the CGMs inferred by the proposed 3D-CGAN outperform those of the benchmark schemes, which can accurately reflect the radio propagation condition in 3D environment.

eess.SP↗

arXiv2024

Constraining the Presence of Companion Planets in Hot Jupiter Planetary System Using TTV Observation from TESS

The presence of another planetary companion in a transiting exoplanet system can impact its transit light curve, leading to sinusoidal transit timing variations (TTV). By utilizing both $\chi^2$ and RMS analysis, we have combined the TESS observation data with an N-body simulation to investigate the existence of an additional planet in the system and put a limit on its mass. We have developed CMAT, an efficient and user-friendly tool for fitting transit light curves and calculating TTV with a theoretical period, based on which we can give a limit on its hidden companion's mass. We use 260 hot Jupiter systems from the complete TESS data set to demonstrate the use of CMAT. Our findings indicate that, for most systems, the upper mass limit of a companion planet can be restricted to several Jupiter masses. This constraint becomes stronger near resonance orbits, such as the 1:2, 2:1, 3:1, and 4:1 mean motion resonance, where the limit is reduced to several Earth masses. These findings align with previous studies suggesting that a lack of companion planets with resonance in hot Jupiter systems could potentially support the high eccentricity migration theory. Additionally, we observed that the choice between $\chi^2$ or {root mean square (RMS)} method does not significantly affect the upper limit on companion mass; however, $\chi^2$ analysis may result in weaker restrictions but is statistically more robust compared to RMS analysis in most cases.

astro-ph.EP↗

arXiv2023

Long-term Orbital Period Variation of Hot Jupiters from Transiting Time Analysis using TESS Survey Data

Many hot Jupiters may experience orbital decays, which are manifested as long-term transit timing variations. We have analyzed 7068 transits from the Transiting Exoplanet Survey Satellite (TESS) for a sample of 326 hot Jupiters. These new mid-transit time data allow us to update ephemerides for these systems. By combining the new TESS transit timing data with archival data, we search for possible long-term orbital period variations in these hot Jupiters using a linear and a quadratic ephemeris model. We identified 26 candidates that exhibit possible long-term orbital period variations, including 18 candidates with decreasing orbital periods and 8 candidates with increasing orbital periods. Among them, 12 candidates have failed in our leave-one-out cross-validation (LOOCV) test and thus should be considered as marginal candidates. In addition to tidal interaction, alternative mechanisms such as apsidal precession, R{\o}mer effect, and Applegate effect could also contribute to the observed period variations. The ephemerides derived in this work are useful for scheduling follow-up observations for these hot Jupiters in the future. The Python code used to generate the ephemerides is made available online.

astro-ph.EP↗

arXiv2022

Hubble WFC3 Spectroscopy of the Terrestrial Planets L~98-59~c \& d: No Evidence for a Clear Hydrogen Dominated Primary Atmosphere

The nearby bright M-dwarf star L~98-59 has three terrestrial-sized planets. One challenge remaining in characterizing atmospheres around such planets is that it is not known a priori whether they possess any atmospheres. Here we report the study of the atmospheres of L~98-59~c and L~98-59~d using the near-infrared spectral data from the G141 grism of HST/WFC3. We can reject the hypothesis of a clear atmosphere dominated by hydrogen and helium at a confidence level of $\sim$ 3~sigma for both planets. Thus they may have a primary hydrogen-dominated atmosphere with an opaque cloud layer, or have lost their primary hydrogen-dominated atmosphere and re-established a secondary thin atmosphere, or have no atmosphere at all. We cannot distinguish between these scenarios for the two planets using the current HST data. Future observations with JWST would be capable of confirming the existence of atmospheres around L~98-59~c and d and determining their compositions.

astro-ph.EP↗

arXiv2022

Hubble WFC3 Spectroscopy of the Rocky Planet L 98-59 b: No Evidence for a Cloud-Free Primordial Atmosphere

We are using archived data from HST of transiting exoplanet L~98-59~b to place constraints on its potentially hot atmosphere. We analyze the data from five transit visits and extract the final combined transmission spectrum using Iraclis. Then we use the inverse atmospheric retrieval code TauREx to analyze the combined transmission spectrum. There is a weak absorption feature near 1.40~$μm$ and 1.55~$μm$ in the transmission spectrum, which can be modeled by a cloudy atmosphere with abundant HCN. However, the unrealistically high abundance of HCN derived cannot be explained by any equilibrium chemical model with reasonable assumptions. Thus, the likeliest scenario is that L~98-59~b has a flat, featureless transmission spectrum in the WFC3/G141 bandpass due to a thin atmosphere with high mean molecular weight, an atmosphere with an opaque aerosol layer, or no atmosphere, and it is very unlikely for L~98-59~b to have a clear hydrogen-dominated primary atmosphere. Due to the narrow wavelength coverage and low spectral resolution of HST/WFC3 G141 grism observation, we cannot tell these different scenarios apart. Our simulation shows future higher precision measurements over wider wavelengths from the James Webb Space Telescope (JWST) can be used to better characterize the planetary atmosphere of L~98-59~b.

astro-ph.EP↗