Hao Zheng

Hanbo Huang, Yiran Zhang, Hao Zheng et al.

Large language model (LLM) watermarking has shown promise in detecting AI-generated content and mitigating misuse, with prior work claiming robustness against paraphrasing and text editing. In this paper, we argue that existing evaluations are not sufficiently adversarial, obscuring critical vulnerabilities and overstating the security. To address this, we introduce the adaptive robustness radius, a formal metric that quantifies the worst-case resilience of watermarks against adaptive adversaries. By lifting the paraphrase space into a KL-divergence ball, we approximate this radius and theoretically demonstrate that optimizing the attack context and model parameters can significantly reduce the approximate radius, making watermarks highly vulnerable to paraphrase attacks. Leveraging this insight, we propose RLCracker, a reinforcement learning (RL)-based adaptive attack that erases watermark signals with limited watermarked examples and limited access to the detector. Despite weak supervision, it empowers a 3B model to achieve 98.5% removal success with minimal semantic shift on 1,500-token Unigram-marked texts after training on only 100 short samples. This performance dramatically exceeds 6.75% by GPT-4o and generalizes across five model sizes over ten watermarking schemes. Our code is available at https://github.com/OTT0-OTO/RLCracker.

Bardia Nadimi, Ghali Omar Boutaib, Hao Zheng

Recently, there has been a growing interest in leveraging Large Language Models for Verilog code generation. However, the current quality of the generated Verilog code remains suboptimal. This is largely due to the absence of well-defined, well-organized datasets with high-quality samples, as well as a lack of innovative fine-tuning methods and models specifically trained on Verilog. In this paper, we introduce a novel open-source dataset and a corresponding fine-tuning technique, which utilizes a multi-layered structure that we refer to as PyraNet. Our experiments demonstrate that employing the proposed dataset and fine-tuning approach leads to a more accurate fine-tuned model, producing syntactically and functionally correct Verilog code. The evaluation results show improvements by up-to $32.6\%$ in comparison to the CodeLlama-7B baseline model and up-to $16.7\%$ in comparison to the state-of-the-art models using VerilogEval evaluation platform.

Bardia Nadimi, Khashayar Filom, Deming Chen et al.

With the rapid advancement of Large Language Models (LLMs), there is growing interest in applying them to hardware design and verification. Among these stages, design verification remains the most time-consuming and resource-intensive phase, where generating effective stimuli for the design under test (DUT) is both critical and labor-intensive. We present {\it TB or not TB}, a framework for automated stimulus generation using LLMs fine-tuned through Coverage-Driven Direct Preference Optimization (CD-DPO). To enable preference-based training, we introduce PairaNet, a dataset derived from PyraNet that pairs high- and low-quality testbenches labeled using simulation-derived coverage metrics. The proposed CD-DPO method integrates quantitative coverage feedback directly into the optimization objective, guiding the model toward generating stimuli that maximize verification coverage. Experiments on the CVDP CID12 benchmark show that {\it TB or not TB} outperforms both open-source and commercial baselines, achieving up to 77.27\% improvement in code coverage, demonstrating the effectiveness of Coverage-driven preference optimization for LLM-based hardware verification.

Bardia Nadimi, Hao Zheng

Recently, there has been a surging interest in using large language models (LLMs) for Verilog code generation. However, the existing approaches are limited in terms of the quality of the generated Verilog code. To address such limitations, this paper introduces an innovative multi-expert LLM architecture for Verilog code generation (MEV-LLM). Our architecture uniquely integrates multiple LLMs, each specifically fine-tuned with a dataset that is categorized with respect to a distinct level of design complexity. It allows more targeted learning, directly addressing the nuances of generating Verilog code for each category. Empirical evidence from experiments highlights notable improvements in terms of the percentage of generated Verilog outputs that are syntactically and functionally correct. These findings underscore the efficacy of our approach, promising a forward leap in the field of automated hardware design through machine learning.

Hao Zheng, Md Rubel Ahmed, Parijat Mukherjee et al.

Concise and abstract models of system-level behaviors are invaluable in design analysis, testing, and validation. In this paper, we consider the problem of inferring models from communication traces of system-on-chip~(SoC) designs. The traces capture communications among different blocks of a SoC design in terms of messages exchanged. The extracted models characterize the system-level communication protocols governing how blocks exchange messages, and coordinate with each other to realize various system functions. In this paper, the above problem is formulated as a constraint satisfaction problem, which is then fed to a SMT solver. The solutions returned by the SMT solver are used to extract the models that accept the input traces. In the experiments, we demonstrate the proposed approach with traces collected from a transaction-level simulation model of a multicore SoC design and traces of a more detailed multicore SoC design developed in GEM5 environment.

MD Rubel Ahmed, Hao Zheng, Parijat Mukherjee et al.

Comprehensive and well-defined specifications are necessary to perform rigorous and thorough validation of system-on-chip (SoC) designs. Message flows specify how components of an SoC design communicate and coordinate with each other to realize various system functions. Message flow specifications are essential for efficient system-level validation and debug for SoC designs. However, in practice such specifications are usually not available, often ambiguous, incomplete, or even contain errors. This paper addresses that problem by proposing a specification mining framework, FlowMiner, that automatically extracts message flows from SoC execution traces, which, unlike software traces, show a high degree of concurrency. A set of inference rules and optimization techniques are presented to improve mining performance and reduce mining complexity. Evaluation of this framework in several experiments shows promising results.

Hao Zheng, Andrew Price, Chris Myers

The enormous number of states reachable during explicit model checking is the main bottleneck for scalability. This paper presents approaches of using decision diagrams to represent very large state space compactly and efficiently. This is possible for asynchronous systems as two system states connected by a transition often share many same local portions. Using decision diagrams can significantly reduce memory demand by not using memory to store the redundant information among different states. This paper considers multi-value decision diagrams for this purpose. Additionally, a technique to reduce the runtime overhead of using these diagrams is also described. Experimental results and comparison with the state compression method as implemented in the model checker SPIN show that the approaches presented in this paper are memory efficient for storing large state space with acceptable runtime overhead.

Hao Zheng, Yingying Zhang, Chris Myers

This paper presents an approach to more efficient partial order reduction for model checking concurrent systems. This approach utilizes a compositional reachability analysis to generate over-approximate local state transition models for all processes in a concurrent system where an independence relation and other useful information can be extracted. The extracted independence relation, compared to what can be obtained by statically analyzing the system descriptions, is more precise and refined, therefore leads to more efficient partial order reduction. This approach is demonstrated on a set of concurrent system examples. Significantly higher reduction in state space has been observed in several cases compared to what can be obtained using SPIN.

Yuting Cao, Parijat Mukherjee, Mahesh Ketkar et al.

Comprehensive specifications are essential for various activities across the entire validation continuum for system-on-chip (SoC) designs. However, specifications are often ambiguous, incomplete, or even contain inconsistencies or errors. This paper addresses this problem by developing a specification mining approach that automatically extracts sequential patterns from SoC transaction-level traces such that the mined patterns collectively characterize system-level specifications for SoC designs. This approach exploits long short-term memory (LSTM) networks trained with the collected SoC execution traces to capture sequential dependencies among various communication events. Then, a novel algorithm is developed to efficiently extract sequential patterns on system-level communications from the trained LSTM models. Several trace processing techniques are also proposed to enhance the mining performance. We evaluate the proposed approach on simulation traces of a non-trivial multi-core SoC prototype. Initial results show that the proposed approach is capable of extracting various patterns on system-level specifications from the highly concurrent SoC execution traces.

Yuting Cao, Hao Zheng, Sandip Ray

Reconstruction of how components communicate with each other during system execution is crucial for debugging system-on-chip designs. However, limited observability is the major obstacle to the efficient and accurate reconstruction in the post-silicon validation stage. This paper addresses that problem by proposing several communication event selection methods guided by system-level communication protocols. Such methods are optimized for on-chip communication event tracing infrastructure to enhance observability. The effectiveness of these methods are demonstrated with experiments on a non-trivial multicore SoC prototype. The results show that with the proposed method, more comprehensive information on system internal execution can be inferred from traces under limited observability.