DeepVerifier: Learning to Update Test Sequences for Coverage-Guided Verification

YUNTAO LU, The Chinese University of Hong Kong, Hong Kong, Hong Kong CHEN BAI, The Hong Kong University of Science and Technology, Hong Kong, Hong Kong YUXUAN ZHAO, The Chinese University of Hong Kong, Hong Kong, Hong Kong ZIYUE ZHENG, The Hong Kong University of Science and Technology - Guangzhou Campus, Guangzhou, China YANGDI LYU, The Hong Kong University of Science and Technology - Guangzhou Campus, Guangzhou, China MINGYU LIU, Huawei Technologies Co Ltd, Wuhan, China BEI YU, The Chinese University of Hong Kong, Hong Kong, Hong Kong

Verification is critical in ensuring the reliable operation of modern, complex computing systems. However, as processor designs become increasingly sophisticated, conventional static verification techniques struggle to generate high-quality test sequences that achieve comprehensive coverage. Dynamic simulation-based ap- proaches, which leverage coverage-driven objectives, can increase confidence in correct processor function- ality but often suffer from low verification efficiency due to the generation of redundant test sequences and significant computational overhead. To address these challenges, this paper presents DeepVerifier, a novel coverage-guided test generation framework that leverages data-driven learning of existing test sequences and their associated coverage feedback. DeepVerifier uses a language model to learn the semantic representa- tions of test sequences, ensure adherence to syntax constraints, and estimate the relationship between test se- quences and coverage scores. By updating test sequences with higher coverage, DeepVerifier can significantly improve the efficiency and effectiveness of the verification process. Experimental results of verifying an out- of-order RISC-V microprocessor demonstrate that the framework accurately estimates the coverage scores of test sequences and updates high-quality sequences that contribute to higher coverage. This coverage-guided test generation technique holds promise for enhancing the reliability of modern processor designs. CCS Concepts: • Hardware → Coverage metrics; Additional Key Words and Phrases: RISC-V, Coverage-guided Verification, Deep Learning

Authors’ Contact Information: Yuntao Lu, The Chinese University of Hong Kong, Hong Kong, Hong Kong; e-mail: ytlu23@cse.cuhk.edu.hk; Chen Bai, The Hong Kong University of Science and Technology, Hong Kong, Hong Kong; e-mail: cbai@cse.cuhk.edu.hk; Yuxuan Zhao, The Chinese University of Hong Kong, Hong Kong, Hong Kong; e-mail: yxzhao21@cse.cuhk.edu.hk; Ziyue Zheng, The Hong Kong University of Science and Technology - Guangzhou Campus, Guangzhou, Guangdong, China; e-mail: zzheng989@connect.hkust-gz.edu.cn; Yangdi Lyu, The Hong Kong University of Science and Technology - Guangzhou Campus, Guangzhou, Guangdong, China; e-mail: yangdilyu@hkust-gz.edu.cn; Mingyu Liu (Corresponding author), Huawei Technologies Co Ltd., Wuhan, China; e-mail: liumingyu@huawei.com; Bei Yu, The Chinese University of Hong Kong, Hong Kong, Hong Kong; e-mail: byu@cse.cuhk.edu.hk.

This work is licensed under a Creative Commons Attribution-NoDerivatives 4.0 International License.
© 2026 Copyright held by the owner/author(s).
ACM 1084-4309/2026/03-ART70
https://doi.org/10.1145/3721133

ACM Trans. Des. Autom. Electron. Syst., Vol. 31, No. 4, Article 70. Publication date: March 2026.

70:2 Y. Lu et al.

ACM Reference Format: Yuntao Lu, Chen Bai, Yuxuan Zhao, Ziyue Zheng, Yangdi Lyu, Mingyu Liu, and Bei Yu. 2026. DeepVerifier: Learning to Update Test Sequences for Coverage-Guided Verification. ACM Trans. Des. Autom. Electron. Syst. 31, 4, Article 70 (March 2026), 23 pages. https://doi.org/10.1145/3721133

1 Introduction RISC-V represents an open-source instruction set architecture (ISA) [1, 2] that has flourished across various sectors of academia and industry due to its modular and extensible characteristics. In the development of processors utilizing RISC-V ISAs, functional verification plays a pivotal role in ensuring the correctness of functionality; this phase can account for as much as 70% of the design and development lifecycle [3]. Coverage metrics are quantitative indicators that show the extent to which a design has been verified. The idea behind coverage-guided verification is to implement more advanced methods for identifying untested behaviors in a design. This approach ultimately improves the effectiveness of the verification process, as seen in various constrained functional verification techniques [4–6]. As processor designs have become increasingly complex, the focus on functional verification has intensified. There is a growing interest in automated verification techniques, aiming to im- prove coverage metrics and reduce the time required for verification. To address these challenges, advanced approaches have been proposed, including static formal analysis, dynamic simulation, and semi-formal methods. Static formal techniques use mathematical formulations and equivalence checking [7] to theoret- ically prove the correctness or generate counterexamples. However, a state explosion issue arises when verifying complex designs with deep hard-to-reach states [8–10]. This challenge limits the practicality and scalability of formal methods for large-scale designs. On the other hand, dynamic simulation techniques function by modeling the system under ex- amination within a hardware-level environment. This methodology facilitates the verification of design functionality through the systematic observation of the system’s behavior across a range of conditions and scenarios. This approach is widely regarded as the leading solution for the eval- uation of large-scale circuits. A simulation verification work [11] achieves coverage objectives through two pioneering techniques: constrained random generation and coverage-guided test se- quence generation. The application of constraints effectively narrows the search space of test sequences, while coverage scores strategically direct the exploration of these generated test se- quences to maximize the coverage of hardware states. Instruction stream generators (ISGs), such as FORCE-RISCV [12], RISC-V design verification framework [13], and RISC-V Non-ISA-specific coverage tool [14], have been developed to system- atically produce test sequences randomly and repetitively. This approach significantly enhances the coverage of various design frameworks. Semi-formal methods, i.e., a concolic testing approach [15], generate effective test sequences by analyzing the control flow graph (CFG) of register- transfer level (RTL) designs. These sequences are simulated and executed to check coverage scores, which then guide the next round of sequence generation. Successfully applying this method requires a thorough understanding of both the design and the grammatical structure of RTL code to accurately analyze the control and data flows that inform the generation of test sequences. Ad- ditionally, inspired by successful software testing practices, fuzzing methods have been applied to hardware verification tasks. Coverage-guided fuzzing techniques have been proposed in [16–20] to generate test sequences that achieve higher coverage scores, revealing bugs and vulnerabilities in hardware designs. Nevertheless, these methods generate test sequences within a few hours or days. The effectiveness of coverage-guided fuzzing is significantly influenced by the combination

ACM Trans. Des. Autom. Electron. Syst., Vol. 31, No. 4, Article 70. Publication date: March 2026.

DeepVerifier: Learning to Update Test Sequences for Coverage-Guided Verification 70:3

of RTL structure analysis and coverage scores. This quality relies on heuristic mutation methods and search algorithms developed by experts, who utilize feedback from coverage scores of test sequences to enhance their strategies. Recently, the increasing trend of machine learning (ML) techniques has opened up new pos- sibilities for addressing the challenges of generating high-quality test sequences with minimal professional knowledge. ML approaches represent a promising direction to reduce reliance on do- main expertise while facilitating greater automation and scalability in test sequence generation. In previous work, a fully connected Bayesian network [21] described the relationships between input test stimuli and coverage metrics. To enhance the representational capabilities of ML models, researchers developed a three-layer artificial neural network [22] that accelerated the test genera- tion process and improved coverage. Additionally, a language model [23] was employed to under- stand the semantics of RTL (Register Transfer Level) code, allowing it to predict the hit rate of functional coverage, which in turn improved verification efficiency. However, the adoption of ML methods also introduces new challenges. These include the need for substantial amounts of data to learn the relevant representations and implicit relationships, as well as the inherent complexity associated with interpretation. In this paper, we introduce a novel framework for generating test sequences called DeepVerifier. This framework is guided by coverage metrics and learns to leverage the relationship between gen- erated test sequences and their associated coverage scores using a language model. Additionally, it employs an objective coverage model to optimize these test sequences for achieving higher cov- erage. To address the challenges posed by limited data and interpretation issues, we generate data from a large number of test sequences along with their corresponding coverage scores obtained from a simulator. We highlight the proposed DeepVerifier, focusing on three key aspects. First, we customized a language model to represent RISC-V ISA instruction sequences. This model tokenizes and trans- forms assembly RISC-V instructions into continuous, low-dimensional embedded vectors, which can then be used as input for a subsequent neural network that estimates coverage scores. Second, we designed a coverage score estimator capable of predicting diverse coverage values for these continuous instruction sequence embeddings. This lightweight predictor allows for fast and ac- curate predictions across various embeddings of RISC-V instruction snippets. Third, we propose an end-to-end differentiable learning strategy to optimize the generated test sequences. Our se- quence update strategy is informed by the predicted coverage values and the deviation between the estimated coverage and the closure coverage scores. By computing the gradients of the test se- quence embeddings for the predicted coverage values, we can update the embeddings using these gradients and adaptive learning rates. This process aims to produce test sequences with higher coverage. A comparison between conventional coverage-guided test generation methods and DeepVerifier is illustrated in Figure 1. In traditional methods, test sequences are generated based on feedback scores from the coverage analyzer, following co-simulation with both the instruction set simulator and the RTL simulator, as depicted in Figure 1(a). In contrast, DeepVerifier efficiently generates high-quality test sequences using a sequence rep- resentation language model, a score predictor, and a sequence optimizer, as shown in Figure 1(b). The effectiveness of DeepVerifier lies in its ability to accurately represent RISC-V instruction sequences through the language model and utilize a fast and reliable coverage score predictor, which minimizes the waiting time during co-simulation. While we demonstrate our approach on 64-bit RISC-V processors, the methodology is inherently extensible to other ISA families. The transformer-based framework requires only adaptation of the tokenization layer and ISA architectural constraints from specifications for different targets, making it applicable to various

    ACM Trans. Des. Autom. Electron. Syst., Vol. 31, No. 4, Article 70. Publication date: March 2026.

70:4                                                                              Y. Lu et al.

                 Random Instruction Stream Generator

Defined | Template | |{| user Bein || Sequences | Simulator Architecture | | Instruction | ELFs Configuration 7 ISA & Coverage Analyzer Coverage Feedback

                                             (@)

    Random Generation  |    Transformer Language Model           |  Coverage Score Predictor
                            Continues                            i                 Coverage)
    Instruction        i                 |₄       Blocks     be      i                    wm
                                                    oe
                                         i|     Projection   1   |
                       i                 H                   Pid     |  Target
                                                                 Target       Coverage




    Semantic Mgher
    Scalability Representations Coverage —— Sequences

    (b)

Fig. 1. (a) End-to-end verification workflow for a random test sequence generator used in RISC-V designs. (b) We propose a new strategy for updating test sequences using a transformer language model, which offers feedback on the coverage of a coverage predictor during the early verification stages in the flow.

processors. The current implementation with a limited set of RISC-V instruction tokens represents a starting point, and the transformer architecture can scale to much larger vocabularies with large-scale tokens to accommodate more complex ISA extensions, additional architectural states, or even mixed-ISA systems. Additionally, it employs a gradient-based sequence update strategy to enhance test sequences in the optimal direction for achieving higher coverage scores. Our contributions are summarized below:

— A customized novel language model has been developed for learning the semantic and syn-
  tactic representations of RISC-V instruction sequences.
— A fast and accurate coverage predictor calculates coverage scores for test instruction
  sequences.
— A gradient-based sequence update strategy uses the target coverage scores to enhance test
  sequences, aiming for higher coverage.
— Experimental results demonstrate that our framework effectively integrates representations
  of instruction sequences, estimates coverage efficiently, and optimizes test sequences, achiev-
  ing a coverage improvement of approximately 3% to 6%, thereby facilitating coverage closure.

The rest of this paper is organized as follows: Section 2 introduces the fundamentals of verification tasks. Section 3 presents the problem formulation for the test sequence update issue. Section 4 offers an overview of the DeepVerifier framework, including the algorithms employed.

ACM Trans. Des. Autom. Electron. Syst., Vol. 31, No. 4, Article 70. Publication date: March 2026.

DeepVerifier: Learning to Update Test Sequences for Coverage-Guided Verification 70:5

Section 5 outlines the experimental setup and evaluates the results obtained from DeepVerifier. Finally, Section 6 summarizes the findings and discusses future research directions.

2 Preliminaries 2.1 RISC-V ISA The RISC-V Instruction Set Architecture (ISA) [1] comprises a mandatory base integer instruc- tion set, referred to as RV32I, RV64I, or RV128I, which is characterized by specific register widths. Additionally, it includes various optional extensions identified by single letters; for example, the letters M, A, C, F, and D correspond to integer multiplication and division, atomic instructions, com- pressed instructions, and single and double precision floating point operations, respectively. For example, RV32IMC specifies a 32-bit core equipped with both M and C extensions. The designation G signifies the IMAFD instruction set; therefore, RV32GC denotes RV32IMAFDC. Each core contains 32 general-purpose registers, labeled from x0 to x31, while the floating point extensions contribute an additional 32 float-point registers. Moreover, there exist specific instructions to access these registers by their designated names, where source registers are referred to as rs1 and rs2, and the destination register is designated as RD. The format and semantics of both the base ISA and its extensions are delineated in the unprivileged ISA specification. Furthermore, the privileged specification outlined in the RISC-V documentation [2] encom- passes several critical functionalities essential for environmental interaction and operating system execution. This specification delineates various execution modes, particularly the mandatory ma- chine mode, along with the extensions for Supervisor and User modes, accompanied by detailed descriptions of the corresponding control and status registers (CSRs). CSRs are specialized reg- isters that are fundamental to the privileged architecture framework. For instance, the machine status register monitors and regulates the current operating state of the hardware thread (hart), the machine ISA register identifies the ISA extensions supported by the processor, and the machine trap-vector base-address register designates the address of the trap/interrupt handler. Additionally, a read-only machine architecture ID register encodes the unique architecture identification of the processor, among other functionalities. The complexity and modularity of the RISC-V ISA present challenges and opportunities for ver- ification. The diverse instruction categories activate different components of the design, which exercise specific functional units and control paths, making comprehensive coverage crucial yet challenging to achieve through manual or random testing alone. The characteristics of RISC-V motivate our transformer-based approach in several ways. For the instruction representation, our model learns semantic relationships to capture both the syntax of individual instructions. For the coverage correlation, the self-attention mechanism enables modeling relationships between in- struction patterns and coverage metrics, which helps identify which instruction combinations ef- fectively exercise different parts of the design. For sequence updates, understanding the semantic structure of RISC-V instructions allows our method to generate valid and effective test sequences.

2.2 Simulation-based Verification In simulation-based verification, the RTL model of the microprocessor is converted into a high- level object-oriented software class within both open-source and commercial environments [24, 25]. This translated high-level model is subsequently instantiated in the testbench alongside a memory model that is populated with the relevant verification tests. Once the simulation in- frastructure is established, it is essential to develop criteria to ascertain whether the simulated tests yield a pass or fail outcome. The most straightforward approach is to conduct correctness checking through directed tests. Upon completion of a test execution, the final result is compared

    ACM Trans. Des. Autom. Electron. Syst., Vol. 31, No. 4, Article 70. Publication date: March 2026.

70:6 Y. Lu et al.

against a pre-calculated reference answer. The determination of success or failure is based on this comparison. While directed tests are extensively utilized within the industry, their primary aim is often to confirm the fundamental functionality of the design or to investigate specific, deliberate corner cases. For over three decades, to rigorously assess the design, both industry professionals and academic researchers have relied on verification binaries that are generated randomly. A Random Instruction Generator (RIG), also referred to as a test program generator or instruction stream generator, is a software utility designed to produce randomized assembly in- struction streams based on predefined configurations. The tests generated by the RIG encompass a wide range of implemented functionalities. This tool is capable of creating intricate test cases that may be challenging for engineers to devise independently [12, 26, 27]. By applying complete random instruction streams to stress the design under test, one can assess the system comprehen- sively. However, complete randomness lacks control over the generated tests, resulting in a low probability of uncovering deeply concealed bugs arising from complex interactions among various components. To address this limitation, some RIGs offer the capability to exert control over the generated tests via test program templates. These templates provide an abstract representation of the test, delineating a set of constraints that the generator must adhere to. Consequently, this enables the management of both the direction and depth of the generated tests [5]. While simulation-based verification relies heavily on random test generation and manual cover- age analysis, our approach enhances this paradigm by introducing learning-based guidance. Deep- Verifier leverages the coverage feedback from simulation runs to train our transformer model, enabling it to learn the relationship between instruction sequences and coverage outcomes. It cre- ates a more intelligent test generation process that combines the thoroughness of simulation-based verification with the predictive power of deep learning. Instead of purely random exploration or manual guidance, our method automatically learns instruction patterns and makes the verification process more efficient and systematic.

2.3 Language Model in Natural Language Processing Natural language processing (NLP) constitutes a domain within linguistics and machine learn- ing that concentrates on comprehending all aspects of human language. The primary objective of NLP tasks is not merely to interpret individual words in isolation, but rather to grasp the broader context in which these words are situated. Moreover, recent advancements in Transformers [28] have resulted in the availability of thou- sands of pre-trained models capable of performing various tasks across different modalities in text. These tasks include text classification, information extraction, question answering, summarization, machine translation, and text generation, supporting over 100 languages. The automatic generation of vector representations for assembly instructions at the binary anal- ysis level draws upon methodologies from the natural language processing (NLP) domain [29], treating binary assembly code as analogous to natural language documents. Prominent deep pre- trained language models in NLP include BERT [30], GPT [31], RoBERTa [32], and BART [33]. Refer- ence [29] introduced a pre-trained assembly language model aimed at general-purpose instruction representation learning, which acknowledges the inherent naturalness of assembly instruction sequences. This work underscores the potential for acquiring semantic representations through pre-trained language models, facilitating their application across a variety of downstream tasks. Advances in NLP, particularly the transformer architecture’s success in capturing sequential de- pendencies and semantic relationships, inspire our approach to hardware verification. We adapt these techniques to treat RISC-V assembly sequences as a domain-specific language, where in- structions are tokens and their relationships represent dependencies. Similar to the transformers learning semantic relationships between words in natural language, our model learns relationships

ACM Trans. Des. Autom. Electron. Syst., Vol. 31, No. 4, Article 70. Publication date: March 2026.

DeepVerifier: Learning to Update Test Sequences for Coverage-Guided Verification 70:7

between instructions and their impact on verification coverage. Furthermore, we extend beyond direct NLP applications by incorporating instruction types and coverage objectives into the model. This allows DeepVerifier to not only understand instruction sequences but also predict their veri- fication effectiveness and guide test generation.

3 Problem Formulation The problem is articulated as follows:

P%&'()* 1. Given a RISC-V microprocessor, the task is to devise a method for generating high- quality test cases that effectively assess its functionality. The primary goal is to maximize the scores of established coverage metrics.

In Problem 1, a test case is defined as a sequence of instructions. In this context, the terms “test sequences” and “test cases” are used interchangeably to convey the same concept.

4 DeepVerifier Framework 4.1 Overview Traditional verification approaches typically rely on random testing to achieve coverage require- ments. DeepVerifier, illustrated in Figure 1(b), serves as a complementary method, specifically tar- geting hard-to-reach coverage cases through intelligent test sequence generation. While achieving near-100% coverage is crucial in processor verification, DeepVerifier is designed not as a replace- ment for existing methods, but as a complementary approach to enhance coverage efficiency. Tra- ditional random testing remains essential for broad coverage but can be time-consuming when targeting specific coverage cases. DeepVerifier addresses this limitation by learning from existing test sequences to intelligently guide the generation of new tests, potentially reducing the number of instructions and simulation time needed to achieve target coverage levels. Our framework par- ticularly excels at identifying patterns that lead to improved coverage in challenging scenarios, working alongside conventional methods to accelerate the verification process. Initially, we generate assembly instruction sequences through a random instruction sequence generator [12] in conjunction with a customized fuzzing tool. These sequences are compiled and simulated using RTL simulators like Synopsys VCS [25] or Verilator [24] to capture coverage scores. To optimize simulation time and instruction count efficiency, we preprocess these sequences and utilize them to train a transformer language model that learns the semantic patterns leading to effective coverage. Our approach comprises three key components designed to reduce the number of instructions needed for achieving target coverage: (1) an encoder that efficiently embeds test sequences into continuous vector representations; (2) a coverage predictor that rapidly forecasts coverage values from these representations; and (3) a decoder that translates optimized continuous representations back into valid instruction sequences. This framework enables quick identification of promising test sequences through iterative parameter adjustment, significantly reducing the exploration time compared to random testing alone. The instruction stream generator creates test sequences based on predefined templates speci- fying instruction types, opcode weights, and sequence length. The transformer model’s encoder- decoder architecture efficiently converts between text sequences and token vectors, maintaining sequence validity while exploring the coverage space. A fine-tuned tokenizer works with the transformer model to convert instructions into token vectors matching the vocabulary size. The encoder creates compact word embeddings, while the decoder reconstructs valid sequences. The model training process minimizes cross-entropy loss to

    ACM Trans. Des. Autom. Electron. Syst., Vol. 31, No. 4, Article 70. Publication date: March 2026.

70:8 Y. Lu et al.

align input and output distributions, capturing crucial patterns that influence coverage. The cov- erage predictor uses the transformer’s final hidden state to build a neural network that efficiently maps sequence characteristics to coverage outcomes. To accelerate coverage improvement, we compute mean square loss between target and pre- dicted coverage scores, using this deviation to update sequence representations. The gradient- based optimization process, guided by scheduled learning rates, efficiently modifies input se- quences while maintaining their validity through a correctness verification tool. This approach complements random testing by specifically targeting coverage gaps, potentially reducing the to- tal number of instructions needed to achieve coverage targets.

4.2 Test Sequence Representation The test sequences comprise a diverse array of assembly programming language snippets of vary- ing lengths, generated by a RISC-V instruction stream generator [12]. Each sequence encompasses a series of instructions, with lengths ranging from 128 to 256. Each instruction comprises opcodes and operands. In alignment with the specifications of the RISC-V ISA [1] and [2], we categorize opcodes into five distinct types and operands into three categories. To effectively represent each instruction, we construct a vocabulary that includes both opcodes and operands, along with a tokenizer designed to convert each token into its corresponding embedded form. To maintain the representation strategy of the and tokens utilized in the trained tok- enizer, which signify the start and end identifiers of each input sequence, we delineate each instruc- tion sequence by inserting and at the beginning and concluding points of each sequence. To interpret the instructions within the RISC-V ISA specifications and convert instruction opcodes and operands into continuous vector representations suitable for subsequent utilization by a trans- former language model, we refine the tokenizer. An instruction comprises tokens that include an opcode (e.g., ADD, SUB), register operands, address operands, and immediate values. We incorporate opcodes and register symbols as new tokens within the vocabulary. To differ- entiate between source and destination operands, we employ the tokens and to represent source registers and destination registers in an instruction, respectively. For immediate operands, we utilize the token to mitigate the presentation of diverse concrete values. Furthermore, for load and store instructions (e.g., LD, SD) that access memory addresses, we ap- pend and labels as tokens at the beginning and end of the instruction to represent the memory access pattern. For conditional and unconditional jump instructions (e.g., BEQ, JAL) that reference the next instruction address, we propose the use of and tokens to identify the range of address registers. Notably, to facilitate the processing of sequences, we replace commas within the instruction with semicolons and subsequently restore them following optimized modifications to maintain the validity of the instruction format. This tokenization approach enables our model to capture both instruction-level and sequence- level semantic relationships, which is crucial for generating effective test sequences. Unlike tradi- tional approaches that treat instructions in isolation, our method preserves contextual dependen- cies that influence coverage outcomes.

4.3 Model Architecture To learn semantic representations for hardware verifications, the LSTM network in [23] can se- quentially learn the dependencies in an instruction sequence, while this approach faces several limitations. The sequential nature of LSTM processing makes it computationally expensive for long instruction sequences, and its fixed-size hidden state becomes a bottleneck when modeling complex instruction dependencies. The Transformer model [34] is a widely recognized technique for sequence modeling, which offers three key advantages through its architecture. First, its parallel

ACM Trans. Des. Autom. Electron. Syst., Vol. 31, No. 4, Article 70. Publication date: March 2026.

DeepVerifier: Learning to Update Test Sequences for Coverage-Guided Verification  70:9

oni







|                  |
H    Tokenizer     H

Fig. 2. Creating customized tokens to represent instruction sequences and integrating RISC-V ISA-specific tokens into the vocabulary, along with developing a new tokenizer. processing and self-attention mechanism excels at capturing long-distance dependencies within in- put sequences while maintaining computational efficiency. Second, its multi-head attention allows simultaneous modeling of different types of instruction relationships. Third, its explicit position encoding better preserves instruction order constraints critical for verification tasks. To leverage these advantages of the model to understand both the semantics and syntax of RISC- V assembly sequences, we developed a customized version of BART [33], a fine-tuned transformer- based sequence-to-sequence language model. This customization involved specific adaptations, including a tailored tokenizer and loss functions, aimed at enhancing RISC-V assembly sequence representation and improving coverage score prediction, drawing inspiration from PalmTree [29], a prior assembly language representation model. Unlike [29] that aims for general-purpose in- struction embedding across architectures, our model is specifically optimized for verification inte- gration with custom tokenization. Furthermore, we bridge representation learning with coverage- guided verification by introducing components for coverage prediction and sequence updates. This customization includes verification-specific adaptations of a tailored tokenizer and specialized loss functions, enabling both better coverage results and more interpretable verification workflows. The customized tokenizer has been developed to effectively capture the distinct characteristics of RISC-V assembly sequences, including opcodes, register operands, address operands, and con- stant immediate values. To address the intricate internal structures of instructions, we represent the instruction sequence by appending special tokens as defined in Section 4.2. Additionally, we generate a specific tokenizer tailored for this purpose, which builds upon the standard tokenizer of BART to incorporate instruction-related tokens into the vocabulary. The processes of prepro- cessing and tokenizing the instruction sequences, along with the composition of the RISC-V ISA- specific tokenizer utilizing a customized vocabulary, are illustrated in Figure 2. The fundamental components of a transformer model encompass an encoder, a decoder, and several linear projection layers designated for downstream tasks. The encoder and decoder are

    ACM Trans. Des. Autom. Electron. Syst., Vol. 31, No. 4, Article 70. Publication date: March 2026.

70:10                                                                                        Y. Lu et al.

composed of a position-wise input embedding layer, followed by N transformer blocks. Each trans-
former block includes a multi-head self-attention layer, a fully connected feed-forward network,
and multiple additive and normalization layers. The output generated from the final transformer
block is subsequently processed through linear projection layers to derive the conclusive output
representation of the input sequence.
               While our current implementation focuses on RISC-V instruction tokenization, the framework
enables expansion to diverse verification scenarios through adaptable token vocabularies and se-
quence lengths. The transformer model’s self-attention mechanism inherently supports sequences
well beyond our current implementation, facilitating the verification of sophisticated designs. The
extensible nature of our architecture accommodates the integration of advanced instruction sets,
architectural states, and control mechanisms. This inherent scalability positions our framework
to adapt to emerging processor architectures and their increasing complexity. As modern proces-
sor designs introduce more sophisticated features, the transformer’s capacity to capture intricate
semantic relationships between instructions becomes increasingly valuable for comprehensive ver-
ification coverage.
            The input embedding and positional encoding layer transforms input tokens x into a continuous
embedded representation denoted as TE, while simultaneously incorporating positional informa-
tion into these representations, referred to as PE. The input tokens x = (x1, x2, . . . , xn ) encompass
a sequence of length n, where each xi , i ∈ {1, 2, . . . , n} signifies a token identity index within the
vocabulary. An embedding matrix TE ∈ Rd!oc ab ×dmod el          is employed to map each input xi into the
embedded space with d!ocab representing the vocabulary size and dmodel              indicating the dimen-
sionality of the embedding space. The embedding tei corresponding to each token xi is articulated
by the following Equation (1),
                              tei = TokenEmbedding(xi ),                                              (1)

where TExi denote the xi -th row of the embedding matrix TE which possesses a dimensionality of d model . For our model, the embedded dimension is defined as 768. To encode positional information for each token within the sequence, sinusoidal positional encoding employs both cosine and sine functions. For a given position pos, pos ∈ {1, 2, . . . , n} and dimension i, i ∈ {1, 2, . . . , dmodel }, the positional encoding is bifurcated into even indices pepos,2i and odd indices pepos,2i+1. These indices correspond to the sine and cosine functions respectively, as indicated in Equation (2),

    pe                        pepos,2i = sine (( 100002iii/dmod el )) ,                               (2)
    pos,2i+1 = cosine 100002i/dmod el .

The final representation ei of each input token is derived by concatenating the token embedding tei with the positional encoding pepos . This relationship is expressed as ei = tei + pepos . Through the processes of token embedding and positional encoding, the input sequence X ∈ Rn×d!oc ab of the length n and a vocabulary size d!ocab is converted into a sequence of continuous embedded representations E ∈ Rn×dmod el , which maintains the same length n and a dimension of dmodel . The attention mechanism employed within each transformer block is designed to capture long-range dependencies present in the embedded sequence and to evaluate the significance of various components through the computation of attention scores. Each transformer block incor- porates a multi-head self-attention layer to derive these attention scores. Specifically, each input embedded matrix is linearly projected into three distinct matrices: query Q, key K, and value V by the projection matrices WQ , WK , WV ∈ Rdmod el ×dₖ , where dk = (dmodel /H ), H denotes the num- ber of self-attention heads, which is established as four in the model. The multi-head attention

ACM Trans. Des. Autom. Electron. Syst., Vol. 31, No. 4, Article 70. Publication date: March 2026.

DeepVerifier: Learning to Update Test Sequences for Coverage-Guided Verification              70:11

score is expressed by Equation (3) as follows:

                    A+ni(Qi , Ki , Vi ) = so,max ( Q√idKki$ ) Vi ,                              (3)
    MultiHeadAttention(Q, K, V) = Concat(A+n1, . . . , A+nH)WO ,

where the computation of each self-attention head, the self-attention score is derived by taking
the dot product of the query matrix Qi    and key matrix Ki . This result is subsequently scaled by
the square root of the key dimension dk . The so,max function is then applied to normalize the
scores, ensuring that their sum equals one. Following this step, a weighted sum of the value matrix
Vi      is calculated to produce the output A+ni for each self-attention head. The final multi-head
attention score is formed by concatenating the outputs of H self-attention heads, after which these
concatenated results are projected using the weight matrix WO ∈ Rdmod el ×dmod el .
        The output generated by the multi-head self-attention layer undergoes normalization through
the function LayerNorm. This layer is designed to normalize inputs across features by utilizing
the mean μ and variance σ      of each hidden state h within a transformer block, as illustrated in
Equation (4),

                            LayerNorm(h) = √hσ −2 +μ ε γ + β .                                  (4)

   Upon processing through the multi-head attention layer, the resultant outputs, denoted as Xattn,
are subsequently directed into the feed-forward network present within each transformer block.
This feed-forward network comprises two fully connected layers, fc1 and fc2, which operate on
each hidden state h. A Gaussian Error Linear Unit (GELU) activation function, as specified in
Equation (5),    GELU(h) = h · 21 ((1 + Φ ( √√h2 ))              )                              (5)
                           ≈ 0.5h     1 + tanh   2(h+0.044715h3)     ,
                                                 π

where - is the cumulative distribution function for Gaussian distribution.
  The following feed-forward network is given by Equation (6),

                          fc1 = GELU(Xat t nW1 + b1),                                           (6)
                          fc2 = GELU(fc       W + b2),
                               1              2

where W1 ∈ Rdmod el ×df f n , W2 ∈ Rdf f n×dmod el represent the projection matrices, while b1 ∈ Rdf f n , b2 ∈ Rdmod el denote the bias vectors corresponding to the first and second fully-connected layers, respectively. The dimension of the feed-forward network, denoted as df f n, is established as 1, 024 within the model. The customized transformer model comprises both encoder and decoder components, consisting of two transformer blocks. The decoder utilizes a preceding output matrix Y ∈ Rm,d!oc ab , where m represents the length of the output sequence. To prevent the decoder from attending to future tokens, the self-attention mechanism is masked. This is achieved by assigning negative infinity val- ues −( to the attention scores of future positions before the application of the so,max function. The input matrices for the decoder’s self-attention are initialized with the outputs from the en- coder’s self-attention. Specifically, the query matrix Q) is derived from the masked self-attention of the decoder, while the key matrix K) and value matrix V) are obtained from the encoder’s outputs.

  ACM Trans. Des. Autom. Electron. Syst., Vol. 31, No. 4, Article 70. Publication date: March 2026.

70:12 Y. Lu et al.

Sequence         |[er]                                      Sequence
           Transformer                                                                        Transformer
IT        |]      pe as                             [|ᵀᵒᵏᵉⁿˢ                                  =
                    ==                                                                      |
                 =        |                         Rea                                       ==
                                                    ‘Actual Coverage
                                                    I
                                                                                       immedi
                Te        |                                CoverageI

entropy A 5s Th I TTT Update parameters Update Parameters (b) Fig. 3. (a) Training a transformer model for a sequential modeling task focused on sequence generation will help the model learn the semantics and syntax of instruction sequences. (b) Performing a supervised prediction task to assess coverage scores using the fine-tuned transformer model from the generation task will enable us to estimate the relationship between the input sequence and its corresponding output.

4.4 Training Tasks By incorporating coverage feedback into the test generation process, our approach captures the sequence pattern and optimizes coverage objectives. These optimization tasks help discover in- struction dependencies in a sequence and obtain the coverage feedback in a short time to guide the successive test generation process. To implement our framework practically, we integrate the existing transformer framework and verification workflows, requiring minimal additional setup while providing substantial benefits in test generation efficiency and coverage improvement. The fine-tuning task illustrated in Figure 3(a) exposes a transformer model to effectively capture the sequence. Subsequently, we apply the fine-tuned model to conduct the downstream task of pre- dicting coverage scores, as depicted in Figure 3(b). Unlike traditional BART implementations that use text infilling as a noising method during train- ing, our sequential modeling task is a fine-tuning task that prioritizes maintaining strict RISC-V ISA compliance throughout the training process. The RISC-V instruction sequences must maintain strict syntax and semantics of ISA compliance, as random masking could disrupt critical instruction dependencies and patterns. The primary objective is to optimize coverage scores through valid and executable test sequences. The transformer model needs to learn the precise relationship between instruction patterns and their corresponding coverage metrics. Adding noise during training could potentially interfere with this coverage-guided learning process. Additionally, unlike natural lan- guage tasks where partial text corruption is acceptable, hardware verification demands precise instruction sequences that can be directly compiled and simulated for the coverage analysis. Training Task 1: Sequential Modeling of Test Generation. The representation of instruction sequences serves to maintain the architectural information of each instruction within a test sequence, as well as the execution rules governing the overall test sequence. This information encompasses the syntactic rules of RISC-V ISAs and highlights execution dependencies between instructions within the current test sequence tied to a particular design under evaluation. Moreover, this information relates to the association between test inputs and code coverage scores for a given design. By acquiring an understanding of the syntax and

ACM Trans. Des. Autom. Electron. Syst., Vol. 31, No. 4, Article 70. Publication date: March 2026.

DeepVerifier: Learning to Update Test Sequences for Coverage-Guided Verification 70:13

execution rules about tokens in a test sequence, and about existing training samples, the proposed model effectively learns the generation of instruction sequencing and the correlation between sequence patterns and objective coverage scores. %n %n L(x) = P(xi |x<i ) = P(xi |x1, x2, . . . , xi−1). (7) i=1 i=1 Through model training, we can delineate the relationships between each token xi and acquire the execution rules pertinent to the current test sequence by optimizing the objective function. For example, regarding the existing tokens in a test sequence { ADD x1 x2 }, the transformer model predicts the subsequent token from among the valid register tokens in the vocabulary. Fur- thermore, the fine-tuned transformer model accurately preserves the syntax of the instruction while also ensuring the proper instruction dependencies. By predicting the subsequent tokens for instruction opcodes and operands, we can ascertain valid register symbols and dependencies, the order of memory access, and the integrity of the control flow. Additionally, a valid test program should achieve correct termination and maintain the integrity of both computational semantics and architectural constraints. On one hand, the fine-tuned transformer model facilitates the appro- priate next tokens and execution flow; on the other hand, we have developed a RISC-V instruction syntax interpreter to guarantee the validity of each instruction following successive updates to the sequence. Training of the transformer model is carried out with a sequence generation task that focuses on recovering the input sequence from the final hidden state, denoted as hn , of the transformer block through transformations applied in the decoder. The objective of this task is to minimize the difference between the input sequence generated by the encoder and the output sequence pro- duced by the decoder. A cross-entropy (CE) loss function is employed to quantify the discrepancy between the predicted token and the corresponding ground-truth token. The objective function is derived from the likelihood of the token sequence, which facilitates the evaluation of the similarity between the source token sequence x, i ∈ {1, 2, . . . , n} of length n and the target token sequence y, j ∈ {1, 2, . . . , m} of length m. Furthermore, the transformer model is updated by minimizing the loss function. The transformer model operates by applying a multi-head self-attention mechanism to the input tokens x. This process is followed by an embedding and positional encoding phase, which converts distinct token vectors into continuous embedded representations. These representations are then subjected to position-wise feed-forward layers, ultimately generating an output distribution for target tokens through a so,max operation. The probability P(%j = c |x, y<j ) of the target token %j , which corresponds to a token identifier & within the vocabulary, is computed based on the preceding tokens y<j and the source token sequence x. This calculation involves a linear projection of the last hidden state hn , resulting in the vector zj containing scores for the potential next tokens in a vocabulary of size d!ocab . Sub- sequently, a so,max function is applied to convert these scores into a probability distribution. The cross-entropy loss, which quantifies the divergence between a target sequence y and input sequence x, is defined in Equation (8),

                                  m d!&
                                1 &  oc ab
                    LossCE = −m j=1 c=1     log P(%j  = c |x, %<j )                           (8)
                                  m d!&
                                1 &
                           = −m j=1  coc ab log 'd    exp(zj,c )     ,
                                     =1     !!=oc ab1  exp(zj,! )

ACM Trans. Des. Autom. Electron. Syst., Vol. 31, No. 4, Article 70. Publication date: March 2026.

Embeddings             |    vail |  Embeddings
                [TTL      |      |
        Tokens

           [en        Sedat      uw
                  Bo             |  x17,
|                     ||         i      on,
         |                       {

Fig. 4. The gradient-based sequence update flow via transformer language model.

70:16    Y. Lu et al.










    Fig. 5. Dataset generation via random instruction stream generator.

                   Table 1. Descriptions of Coverage Metrics
Coverage       Descriptions
Line           Lines or statements were executed.
Toggle         Signals toggle from 0 to 1 and 1 to 0.
Condition      Both true and false states of conditions were covered.
Branch         If, case statements, the ternary operator (?:) branches of execution.

Table 2. Average Coverage and Runtime of Different Test Sequence Generation Methods
Coverage/Runtime Random [12] Mutation [20] LSTM [23] DeepVerifier
Line           76.753122  79.286422  78.791064  83.333333
Branch         71.879106  79.080824  77.777780  79.286422
Toggle         62.054130  66.666670  66.032580  68.977651
Runtime (s)       955        1066       150        176

ACM Trans. Des. Autom. Electron. Syst., Vol. 31, No. 4, Article 70. Publication date: March 2026.

70:18    Y. Lu et al.










Fig. 6. Average coverage improvement of DeepVerifer, LSTM body method, and mutation method over ran-
dom generation.










Fig. 7. Coverage improvement of our transformer method over random generation.










    Fig. 8. Coverage improvement of the mutation over random generation.

DeepVerifier: Learning to Update Test Sequences for Coverage-Guided Verification  70:19










Fig. 9. Coverage improvement of the LSTM body method over random generation.

    ACM Trans. Des. Autom. Electron. Syst., Vol. 31, No. 4, Article 70. Publication date: March 2026.

70:20    Y. Lu et al.

DeepVerifier: Learning to Update Test Sequences for Coverage-Guided Verification  70:21

    ACM Trans. Des. Autom. Electron. Syst., Vol. 31, No. 4, Article 70. Publication date: March 2026.

ACM Trans. Des. Autom. Electron. Syst., Vol. 31, No. 4, Article 70. Publication date: March 2026.

ACM Trans. Des. Autom. Electron. Syst., Vol. 31, No. 4, Article 70. Publication date: March 2026.