® DIGITAL mopeny PDF Download2026 Sore Total Downloads: 06 Latest updates: hitps://dl.acm.org/doi/10.1145/3721133 Accepted: 17 February 2025 RESEARCH-ARTICLE Revised: 21 January 2025 Received: 07 November 2024 DeepVerifier: Learning to Update Test Sequences for Coverage-Guided Con fon Verification

YUNTAO LU, Chinese University of Hong Kong, Hong Kong, Hong Kong

CHEN BAL, Hong Kong University of Science and Technology, Hong Kong, Hong Kong

YUXUAN ZHAO, Chinese University of Hong Kong, Hong Kong, Hong Kong

ZIYUE ZHENG, The Hong Kong University of Science and Technology (Guangzhou), Guangzhou, Guangdong, China

YANGDI LYU, The Hong Kong University of Science and Technology (Guangzhou), Guangzhou, Guangdong, China

MINGYU LIU, Huawei Technologies Co., Ltd., Shenzhen, Guangdong, China

View all

Open Access Support provided by: Chinese University of Hong Kong

The Hong Kong University of Science and Technology (Guangzhou)

Huawei Technologies Co., Ltd.

Hong Kong University of Science and Technology

                                                 ACM Transactions on Design Automation of Electronic Systems
                                                                             hitps://doi.org/10.1145/3721133
                                                                                 EISSN:            1557-7309

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

Veriication is critical in ensuring the reliable operation of modern, complex computing systems. However, as processor designs become increasingly sophisticated, conventional static veriication techniques struggle to generate high-quality test sequences that achieve comprehensive coverage. Dynamic simulation-based approaches, which leverage coverage-driven objectives, can increase conidence in correct processor functionality but often sufer from low veriication eiciency due to the generation of redundant test sequences and signiicant computational overhead. To address these challenges, this paper presents DeepVeriier, a novel coverage-guided test generation framework that leverages data-driven learning of existing test sequences and their associated coverage feedback. DeepVeriier uses a language model to learn the semantic representations of test sequences, ensure adherence to syntax constraints, and estimate the relationship between test sequences and coverage scores. By updating test sequences with higher coverage, DeepVeriier can signiicantly improve the eiciency and efectiveness of the veriication 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.

1 Introduction RISC-V represents an open-source instruction set architecture (ISA) [1], [2] that has lourished across various sectors of academia and industry due to its modular and extensible characteristics. In the development of processors utilizing RISC-V ISAs, functional veriication 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].

Corresponding author: Mingyu Liu. 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, 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 International 4.0 License.
© 2025 Copyright held by the owner/author(s).
ACM 1557-7309/2025/3-ART
https://doi.org/10.1145/3721133

    ACM Trans. Des. Autom. Electron. Syst.

2 • Y. Lu et al.

Coverage metrics are quantitative indicators that show the extent to which a design has been veriied. The idea behind coverage-guided veriication is to implement more advanced methods for identifying untested behaviors in a design. This approach ultimately improves the efectiveness of the veriication process, as seen in various constrained functional veriication techniques [4], [5], [6]. As processor designs have become increasingly complex, the focus on functional veriication has intensiied. There is a growing interest in automated veriication techniques, aiming to improve coverage metrics and reduce the time required for veriication. 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 theoretically prove the correctness or generate counterexamples. However, a state explosion issue arises when verifying complex designs with deep hard-to-reach states [8], [9], [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 examination within a hardware-level environment. This methodology facilitates the veriication 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 evaluation of large-scale circuits. A simulation veriication work [11] achieves coverage objectives through two pioneering techniques: constrained random generation and coverage-guided test sequence generation. The application of constraints efectively narrows the search space of test sequences, while coverage scores strategically direct the exploration of these generated test sequences to maximize the coverage of hardware states. Instruction stream generators (ISGs), such as FORCE-RISCV [12], RISC-V design veriication framework [13], and RISC-V Non-ISA-speciic coverage tool [14], have been developed to systematically produce test sequences randomly and repetitively. This approach signiicantly enhances the coverage of various design frameworks. Semi-formal methods, i.e., a concolic testing approach [15], generate efective test sequences by analyzing the control low 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 lows that inform the generation of test sequences. Additionally, inspired by successful software testing practices, fuzzing methods have been applied to hardware veriication tasks. Coverage-guided fuzzing techniques have been proposed in [16], [17], [18], [19], [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 efectiveness of coverage-guided fuzzing is signiicantly inluenced by the combination 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 possibilities for addressing the challenges of generating high-quality test sequences with minimal professional knowledge. ML approaches represent a promising direction to reduce reliance on domain 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 artiicial neural network [22] that accelerated the test generation process and improved coverage. Additionally, a language model [23] was employed to understand the semantics of RTL (Register Transfer Level) code, allowing it to predict the hit rate of functional coverage, which in turn improved veriication eiciency. 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.

ACM Trans. Des. Autom. Electron. Syst.

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

Random Instruction Stream Generator

Defined Architecture Instruction Instruction Set Template | | User Data Generati Sequences Simulator APIs on RISC-V RTL Simulator Architecture | Instruction Engine RISC-V ELFs Configuration | ISA j Compiler Coverage ] Analyzer Coverage Feedback (a)

Random Generation | Transformer Language Model Coverage Score Predictor Continues Predicted Coverage Instruction | Representation Transformer || | | Sequence 1 d<latexitsha1_base64="J7Z4l6l4xpH4EkC/9P/e4FTqF5g=">AAAB8HicbVC7SgNBFJ31GeMrKtjYLAbBKuxaRMsQG8sEzEOSJczO3k2GzGOZmRXCkq+wsVDEVvAv/AI7G7/FyaPQxAMXDufcy733hAmj2njel7Oyura+sZnbym/v7O7tFw4Om1qmikCDSCZVO8QaGBXQMNQwaCcKMA8ZtMLh9cRv3YPSVIpbM0og4LgvaEwJNla6i3oZlxGwca9Q9EreFO4y8eekWDmuf9P36ketV/jsRpKkHIQhDGvd8b3EBBlWhhIG43w31ZBgMsR96FgqMAcdZNODx+6ZVSI3lsqWMO5U/T2RYa71iIe2k2Mz0IveRPzP66QmvgoyKpLUgCCzRXHKXCPdyfduRBUQw0aWYKKovdUlA6wwMTajvA3BX3x5mTQvSn65VK7bNKpohhw6QafoHPnoElXQDaqhBiKIowf0hJ4d5Tw6L87rrHXFmc8coT9w3n4ACl6USA== Blocks Li Loss Update model il Linear i1 {| Projection |i |! Target Coverage Optimized Validation Optimization Sequence

Diversity and + Semantic + Higher Optimized 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 ofers feedback on the coverage of a coverage predictor during the early verification stages in the flow.

In this paper, we introduce a novel framework for generating test sequences called DeepVeriier. This framework is guided by coverage metrics and learns to leverage the relationship between generated 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 coverage. 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 DeepVeriier, focusing on three key aspects. First, we customized a language model to represent RISC-V ISA instruction sequences. This model tokenizes and transforms 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 accurate predictions across various embeddings of RISC-V instruction snippets. Third, we propose an end-to-end diferentiable learning strategy to optimize the generated test sequences. Our sequence update strategy is informed by the predicted coverage values and the deviation between the estimated coverage and the

ACM Trans. Des. Autom. Electron. Syst.

(

                       …

4 • Y. Lu et al.

closure coverage scores. By computing the gradients of the test sequence 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 DeepVeriier is illustrated in Fig. 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 Fig. 1(a). In contrast, DeepVeriier eiciently generates high-quality test sequences using a sequence representation language model, a score predictor, and a sequence optimizer, as shown in Fig. 1(b). The efectiveness of DeepVeriier 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 speciications for diferent targets, making it applicable to various 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 syntactic 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 efectively integrates representations of instruction sequences, estimates coverage eiciently, and optimizes test sequences, achieving 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 veriication tasks. Section 3 presents the problem formulation for the test sequence update issue. Section 4 ofers an overview of the DeepVeriier framework, including the algorithms employed. Section 5 outlines the experimental setup and evaluates the results obtained from DeepVeriier. Finally, Section 6 summarizes the indings 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 instruction set, referred to as RV32I, RV64I, or RV128I, which is characterized by speciic register widths. Additionally, it includes various optional extensions identiied by single letters; for example, the letters M, A, C, F, and D correspond to integer multiplication and division, atomic instructions, compressed instructions, and single and double precision loating point operations, respectively. For example, RV32IMC speciies a 32-bit core equipped with both M and C extensions. The designation G signiies the IMAFD instruction set; therefore, RV32GC denotes RV32IMAFDC. Each core contains 32 general-purpose registers, labeled from x0 to x31, while the loating point extensions contribute an additional 32 loat-point registers. Moreover, there exist speciic 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 speciication.

ACM Trans. Des. Autom. Electron. Syst.

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

Furthermore, the privileged speciication outlined in the RISC-V documentation [2] encompasses several critical functionalities essential for environmental interaction and operating system execution. This speciication delineates various execution modes, particularly the mandatory machine 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 registers 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 identiies 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 identiication of the processor, among other functionalities. The complexity and modularity of the RISC-V ISA present challenges and opportunities for veriication. The diverse instruction categories activate diferent components of the design, which exercise speciic 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 instruction patterns and coverage metrics, which helps identify which instruction combinations efectively exercise diferent parts of the design. For sequence updates, understanding the semantic structure of RISC-V instructions allows our method to generate valid and efective test sequences.

2.2 Simulation-based Verification In simulation-based veriication, 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 veriication tests. Once the simulation infrastructure 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 inal result is compared 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 conirm the fundamental functionality of the design or to investigate speciic, deliberate corner cases. For over three decades, to rigorously assess the design, both industry professionals and academic researchers have relied on veriication 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 instruction streams based on predeined conigurations. 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 [26], [27], [12]. By applying complete random instruction streams to stress the design under test, one can assess the system comprehensively. 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 ofer 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 veriication relies heavily on random test generation and manual coverage analysis, our approach enhances this paradigm by introducing learning-based guidance. DeepVeriier leverages the coverage

    ACM Trans. Des. Autom. Electron. Syst.

6 • Y. Lu et al.

feedback from simulation runs to train our transformer model, enabling it to learn the relationship between instruction sequences and coverage outcomes. It creates a more intelligent test generation process that combines the thoroughness of simulation-based veriication with the predictive power of deep learning. Instead of purely random exploration or manual guidance, our method automatically learns instruction patterns and makes the veriication process more eicient and systematic.

2.3 Language Model in Natural Language Processing Natural language processing (NLP) constitutes a domain within linguistics and machine learning 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 thousands of pre- trained models capable of performing various tasks across diferent modalities in text. These tasks include text classiication, 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 analysis 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]. Reference [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 dependencies and semantic relationships, inspire our approach to hardware veriication. We adapt these techniques to treat RISC-V assembly sequences as a domain-speciic language, where instructions are tokens and their relationships represent dependencies. Similar to the transformers learning semantic relationships between words in natural language, our model learns relationships between instructions and their impact on veriication coverage. Furthermore, we extend beyond direct NLP applications by incorporating instruction types and coverage objectives into the model. This allows DeepVeriier to not only understand instruction sequences but also predict their veriication efectiveness and guide test generation.

3 Problem Formulation The problem is articulated as follows: Problem 1. Given a RISC-V microprocessor, the task is to devise a method for generating high-quality test cases that efectively assess its functionality. The primary goal is to maximize the scores of established coverage metrics. In Problem 1, a test case is deined 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 veriication approaches typically rely on random testing to achieve coverage requirements, DeepVer- iier, illustrated in Fig. 1(b), serves as a complementary method, speciically targeting hard-to-reach coverage cases through intelligent test sequence generation. While achieving near-100% coverage is crucial in processor veriication, DeepVeriier is designed not as a replacement for existing methods, but as a complementary approach

ACM Trans. Des. Autom. Electron. Syst.

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

to enhance coverage eiciency. Traditional random testing remains essential for broad coverage but can be time-consuming when targeting speciic coverage cases. DeepVeriier 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 particularly excels at identifying patterns that lead to improved coverage in challenging scenarios, working alongside conventional methods to accelerate the veriication 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 eiciency, we preprocess these sequences and utilize them to train a transformer language model that learns the semantic patterns leading to efective coverage. Our approach comprises three key components designed to reduce the number of instructions needed for achieving target coverage: (1) an encoder that eiciently embeds test sequences into continuous vector rep- resentations; (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 identiication of promising test sequences through iterative parameter adjustment, signiicantly reducing the exploration time compared to random testing alone. The instruction stream generator creates test sequences based on predeined templates specifying instruction types, opcode weights, and sequence length. The transformer model’s encoder-decoder architecture eiciently converts between text sequences and token vectors, maintaining sequence validity while exploring the coverage space. A ine-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 align input and output distributions, capturing crucial patterns that inluence coverage. The coverage predictor uses the transformer’s inal hidden state to build a neural network that eiciently maps sequence characteristics to coverage outcomes. To accelerate coverage improvement, we compute mean square loss between target and predicted coverage scores, using this deviation to update sequence representations. The gradient-based optimization process, guided by scheduled learning rates, eiciently modiies input sequences while maintaining their validity through a correctness veriication tool. This approach complements random testing by speciically targeting coverage gaps, potentially reducing the total 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 varying 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 speciications of the RISC-V ISA [1] and [2], we categorize opcodes into ive distinct types and operands into three categories. To efectively 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 tokenizer, which signify the start and end identiiers of each input sequence, we delineate each instruction sequence by inserting and at the beginning and concluding points of each sequence. To interpret the instructions within the RISC-V ISA speciications and convert instruction opcodes and operands into continuous vector representations suitable for subsequent utilization by a transformer language model, we reine the tokenizer. An instruction

    ACM Trans. Des. Autom. Electron. Syst.

8 • Y. Lu et al.

                ADDI x1, x1, 651              <s> ADDI <dsts> x1; <srcs> x1; <const>
                SLLI x1, x1, 0xd              <s> SLLI <dsts> x1; <srcs> x1; <const>
                …                             …
                LD x22, x29, 0                <s> LD <dsts> x22; <srcs> <mem> x29; <const> </mem>
                BEQ x22, x21, 4               <s> BEQ <srcs> x22; x21; <addr> <const> </addr>
                JALR x0, x1, 0                <s> JALR <dsts> x0; <srcs> x1; <addr> <const> </addr>
                …                             …
                                              </s>

    Tokenizer
                     Integer Register-Register:               Floating-Point:
                     ADD, SUB, …, AND, OR                     FADD.S, FSUB.S, …, FLT.S

                 Integer Immediate:                                   Compressed:
                 ADDI, SLLI, …, ANDI, ORI      Pre-trained            C.ADDI, C.BEQZ, …, C.J
                                                Tokenizer
                 Mutiplications/Divisions:                            Registers:
                 MUL, DIV, …, REM                                     x0, …, x31, f0, …, f31

                                               Special Tokens:
                                               <srcs>, <dsts>, <mem>,
                                               </mem>, <addr>, </addr>


    New Tokenizer

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.

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 diferentiate 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 append 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 modiications 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 efective test sequences. Unlike traditional approaches that treat instructions in isolation, our method preserves contextual dependencies that inluence coverage outcomes.

4.3 Model Architecture To learn semantic representations for hardware veriications, the LSTM network in [23] can sequentially learn the dependencies in an instruction sequence, while this approach faces several limitations. The sequential nature

ACM Trans. Des. Autom. Electron. Syst.

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

of LSTM processing makes it computationally expensive for long instruction sequences, and its ixed-size hidden state becomes a bottleneck when modeling complex instruction dependencies. The Transformer model [34] is a widely recognized technique for sequence modeling, which ofers three key advantages through its architecture. First, its parallel processing and self-attention mechanism excels at capturing long-distance dependencies within input sequences while maintaining computational eiciency. Second, its multi-head attention allows simultaneous modeling of diferent types of instruction relationships. Third, its explicit position encoding better preserves instruction order constraints critical for veriication 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 ine-tuned transformer-based sequence-to- sequence language model. This customization involved speciic 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 instruction embedding across architectures, our model is speciically optimized for veriication integration with custom tokenization. Furthermore, we bridge representation learning with coverage-guided veriication by introducing components for coverage prediction and sequence updates. This customization includes veriication-speciic adaptations of a tailored tokenizer and specialized loss functions, enabling both better coverage results and more interpretable veriication worklows. The customized tokenizer has been developed to efectively capture the distinct characteristics of RISC-V assembly sequences, including opcodes, register operands, address operands, and constant immediate values. To address the intricate internal structures of instructions, we represent the instruction sequence by appending special tokens as deined in Section 4.2. Additionally, we generate a speciic tokenizer tailored for this purpose, which builds upon the standard tokenizer of BART to incorporate instruction-related tokens into the vocabulary. The processes of preprocessing and tokenizing the instruction sequences, along with the composition of the RISC-V ISA-speciic tokenizer utilizing a customized vocabulary, are illustrated in Fig. 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 composed of a position-wise input embedding layer, followed by 𠐀 transformer blocks. Each transformer 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 inal 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 expan- sion to diverse veriication scenarios through adaptable token vocabularies and sequence lengths. The transformer model’s self-attention mechanism inherently supports sequences well beyond our current implementation, fa- cilitating the veriication 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 processor designs introduce more sophisticated features, the transformer’s capacity to capture intricate semantic relationships between instructions becomes increasingly valuable for comprehensive veriication coverage. The input embedding and positional encoding layer transforms input tokens x into a continuous embedded representation denoted as TE, while simultaneously incorporating positional information into these represen- tations, referred to as PE. The input tokens x = (𩐀1, 𩐀2, ..., 𩐀𦰀) encompass a sequence of length 𦰀, where each 𩐀𥠀, 𥠀 ∈ {1, 2, ..., 𦰀} signiies a token identity index within the vocabulary. An embedding matrix TE ∈ R𤐀𨰀𧀀𤀀𣠀𣰀 ×𤐀𦠀𧀀𤐀𤠀𦐀 is employed to map each input xi into the embedded space with 𤐀𨰀𧀀𤀀𣠀𣰀 representing the vocabulary size and 𤐀𦠀𧀀𤐀𤠀𦐀 indicating the dimensionality of the embedding space. The embedding te𥠀 corresponding to each token 𩐀𥠀

ACM Trans. Des. Autom. Electron. Syst.

10 • Y. Lu et al.

is articulated by the following Equation (1),

te𥠀                                  = TokenEmbedding(𩐀𥠀 ),                                                                (1)

where TE𩐀𥠀 denote the 𩐀𥠀 -th row of the embedding matrix TE which possesses a dimensionality of 𤐀𦠀𧀀𤐀𤠀𦐀 . For our model, the embedded dimension is deined 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 𧐀𧀀𨀀, 𧐀𧀀𨀀 ∈ {1, 2, ..., 𦰀} and dimension 𥠀, 𥠀 ∈ {1, 2, ..., 𤐀𦠀𧀀𤐀𤠀𦐀 }, the positional encoding is bifurcated into even indices pe𧐀𧀀𨀀,2𥠀 and odd indices pe𧐀𧀀𨀀,2𥠀+1. These indices correspond to the sine and cosine functions respectively, as indicated in Equation (2),

pe     pe𧐀𧀀𨀀,2𥠀                   = sine( 100002𥠀𥠀𥠀/𤐀𦠀𧀀𤐀𤠀𦐀 ),                                                    (2)
𧐀𧀀𨀀,2𥠀+1                          = cosine( 100002𥠀/𤐀𦠀𧀀𤐀𤠀𦐀 ).

The inal representation e𥠀 of each input token is derived by concatenating the token embedding te𥠀 with the positional encoding pe𧐀𧀀𨀀 . This relationship is expressed as e𥠀 = te𥠀 + pe𧐀𧀀𨀀 . Through the processes of token embedding and positional encoding, the input sequence X ∈ R𦰀×𤐀𨰀𧀀𤀀𣠀𣰀 of the length 𦰀 and a vocabulary size 𤐀𨰀𧀀𤀀𣠀𣰀 is converted into a sequence of continuous embedded representations E ∈ R𦰀×𤐀𦠀𧀀𤐀𤠀𦐀 , which maintains the same length 𦰀 and a dimension of 𤐀𦠀𧀀𤐀𤠀𦐀 . The attention mechanism employed within each transformer block is designed to capture long-range dependencies present in the embedded sequence and to evaluate the signiicance of various components through the computation of attention scores. Each transformer block incorporates a multi-head self-attention layer to derive these attention scores. Speciically, each input embedded matrix is linearly projected into three distinct matrices: query Q, key K, and value V by the projection matrices W𡀀 , W🠀, W𢐀 ∈ R𤐀𦠀𧀀𤐀𤠀𦐀 ×𤐀𦀀 , where 𤐀𦀀 = (𤐀𦠀𧀀𤐀𤠀𦐀 /𞰀 ), 𞰀 denotes the number of self-attention heads, which is established as 4 in the model. The multi-head attention score is expressed by Equation (3) as follows:

                            Atni(Q𥠀, K𥠀, V𥠀 ) = sotmax( Q√𥠀𤐀K𦀀𥠀⊤ )V𥠀,        (3)

MultiHeadAttention(Q, K, V) = Concat(Atn1, ..., AtnH)W𠠀 , where the computation of each self-attention head, the self-attention score is derived by taking the dot product of the query matrix Q𥠀 and key matrix K𥠀 . This result is subsequently scaled by the square root of the key dimension 𤐀𦀀 . The sotmax function is then applied to normalize the scores, ensuring that their sum equals one. Following this step, a weighted sum of the value matrix V𥠀 is calculated to produce the output Atni for each self-attention head. The inal multi-head attention score is formed by concatenating the outputs of 𞰀 self-attention heads, after which these concatenated results are projected using the weight matrix W𠠀 ∈ R𤐀𦠀𧀀𤐀𤠀𦐀 ×𤐀𦠀𧀀𤐀𤠀𦐀 . 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 sub- sequently directed into the feed-forward network present within each transformer block. This feed-forward network comprises two fully connected layers, fc1 and fc , which operate on each hidden state h. A Gaussian 2

ACM Trans. Des. Autom. Electron. Syst.

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

Instruction Instruction Sequence Sequence Tokenizer Transformer J) Transformer 2 Tokenizer

T D || [| Token IDs || <latexitsha1_base64="y9tfvJsYxlYFrN0R1Gx1G1XgXEk=">AAAB8nicbVBNT8JAEJ3iF+IX6tHLRjDxRFoO6JHEi0dMBExKQ7bbLWzY7ja7WxLS8DO8eNAYr/4ab/4bF+hBwZdM8vLeTGbmhSln2rjut1Pa2t7Z3SvvVw4Oj45PqqdnPS0zRWiXSC7VU4g15UzQrmGG06dUUZyEnPbDyd3C70+p0kyKRzNLaZDgkWAxI9hYya9Hw3wqCQ7n9WG15jbcJdAm8QpSgwKdYfVrEEmSJVQYwrHWvuemJsixMoxwOq8MMk1TTCZ4RH1LBU6oDvLlyXN0ZZUIxVLZEgYt1d8TOU60niWh7UywGet1byH+5/mZiW+DnIk0M1SQ1aI448hItPgfRUxRYvjMEkwUs7ciMsYKE2NTqtgQvPWXN0mv2fBajdZDs9ZGRRxluIBLuAYPbqAN99CBLhCQ8Ayv8OYY58V5dz5WrSWnmDmHP3A+fwDUFJDdd (sha1_base64="gC9yTm68IZYr3cDfMlwdTr5l2aY=">AAAB8HicbVA9TwJBEJ3DL8Qv1NJmI5hYkTsKtCTaWGIiH4a7kL1lDzbs7l1290zIhV9hY6Extv4cO/+NC1yh4EsmeXlvJjPzwoQzbVz32ylsbG5t7xR3S3v7B4dH5eOTjo5TRWibxDxWvRBrypmkbcMMp71EUSxCTrvh5Hbud5+o0iyWD2aa0EDgkWQRI9hY6bHq37DRyM+qg3LFrbkLoHXi5aQCOVqD8pc/jEkqqDSEY637npuYIMPKMMLprOSnmiaYTPCI9i2VWFAdZIuDZ+jCKkMUxcqWNGih/p7IsNB6KkLbKbAZ61VvLv7n9VMTXQcZk0lqqCTLRVHKkYnR/Hs0ZIoSw6eWYKKYvRWRMVaYGJtRyYbgrb68Tjr1mteoNe7rlWY1j6MIZ3AOl+DBFTThDlrQBgICnuEV3hzlvDjvzseyteDkM6fwB87nD9b5j7M=<latexit

*+,-. E vocab | D | | <latexitsha1_base64="y9tfvJsYxlYFrN0R1Gx1G1XgXEk=">AAAB8nicbVBNT8JAEJ3iF+IX6tHLRjDxRFoO6JHEi0dMBExKQ7bbLWzY7ja7WxLS8DO8eNAYr/4ab/4bF+hBwZdM8vLeTGbmhSln2rjut1Pa2t7Z3SvvVw4Oj45PqqdnPS0zRWiXSC7VU4g15UzQrmGG06dUUZyEnPbDyd3C70+p0kyKRzNLaZDgkWAxI9hYya9Hw3wqCQ7n9WG15jbcJdAm8QpSgwKdYfVrEEmSJVQYwrHWvuemJsixMoxwOq8MMk1TTCZ4RH1LBU6oDvLlyXN0ZZUIxVLZEgYt1d8TOU60niWh7UywGet1byH+5/mZiW+DnIk0M1SQ1aI448hItPgfRUxRYvjMEkwUs7ciMsYKE2NTqtgQvPWXN0mv2fBajdZDs9ZGRRxluIBLuAYPbqAN99CBLhCQ8Ayv8OYY58V5dz5WrSWnmDmHP3A+fwDUFJDddvocab(sha1_base64="gC9yTm68IZYr3cDfMlwdTr5l2aY=">AAAB8HicbVA9TwJBEJ3DL8Qv1NJmI5hYkTsKtCTaWGIiH4a7kL1lDzbs7l1290zIhV9hY6Extv4cO/+NC1yh4EsmeXlvJjPzwoQzbVz32ylsbG5t7xR3S3v7B4dH5eOTjo5TRWibxDxWvRBrypmkbcMMp71EUSxCTrvh5Hbud5+o0iyWD2aa0EDgkWQRI9hY6bHq37DRyM+qg3LFrbkLoHXi5aQCOVqD8pc/jEkqqDSEY637npuYIMPKMMLprOSnmiaYTPCI9i2VWFAdZIuDZ+jCKkMUxcqWNGih/p7IsNB6KkLbKbAZ61VvLv7n9VMTXQcZk0lqqCTLRVHKkYnR/Hs0ZIoSw6eWYKKYvRWRMVaYGJtRyYbgrb68Tjr1mteoNe7rlWY1j6MIZ3AOl+DBFTThDlrQBgICnuEV3hzlvDjvzseyteDkM6fwB87nD9b5j7M=<latexit |] Decoder A ! "# $%& '(")' cross A | —t | Predictor entr O T Generation H o | <latexitsha1_base64="y9tfvJsYxlYFrN0R1Gx1G1XgXEk=">AAAB8nicbVBNT8JAEJ3iF+IX6tHLRjDxRFoO6JHEi0dMBExKQ7bbLWzY7ja7WxLS8DO8eNAYr/4ab/4bF+hBwZdM8vLeTGbmhSln2rjut1Pa2t7Z3SvvVw4Oj45PqqdnPS0zRWiXSC7VU4g15UzQrmGG06dUUZyEnPbDyd3C70+p0kyKRzNLaZDgkWAxI9hYya9Hw3wqCQ7n9WG15jbcJdAm8QpSgwKdYfVrEEmSJVQYwrHWvuemJsixMoxwOq8MMk1TTCZ4RH1LBU6oDvLlyXN0ZZUIxVLZEgYt1d8TOU60niWh7UywGet1byH+5/mZiW+DnIk0M1SQ1aI448hItPgfRUxRYvjMEkwUs7ciMsYKE2NTqtgQvPWXN0mv2fBajdZDs9ZGRRxluIBLuAYPbqAN99CBLhCQ8Ayv8OYY58V5dz5WrSWnmDmHP3A+fwDUFJDddvocab(sha1_base64="gC9yTm68IZYr3cDfMlwdTr5l2aY=">AAAB8HicbVA9TwJBEJ3DL8Qv1NJmI5hYkTsKtCTaWGIiH4a7kL1lDzbs7l1290zIhV9hY6Extv4cO/+NC1yh4EsmeXlvJjPzwoQzbVz32ylsbG5t7xR3S3v7B4dH5eOTjo5TRWibxDxWvRBrypmkbcMMp71EUSxCTrvh5Hbud5+o0iyWD2aa0EDgkWQRI9hY6bHq37DRyM+qg3LFrbkLoHXi5aQCOVqD8pc/jEkqqDSEY637npuYIMPKMMLprOSnmiaYTPCI9i2VWFAdZIuDZ+jCKkMUxcqWNGih/p7IsNB6KkLbKbAZ61VvLv7n9VMTXQcZk0lqqCTLRVHKkYnR/Hs0ZIoSw6eWYKKYvRWRMVaYGJtRyYbgrb68Tjr1mteoNe7rlWY1j6MIZ3AOl+DBFTThDlrQBgICnuEV3hzlvDjvzseyteDkM6fwB87nD9b5j7M=<latexit H M | Predicted Coverage Update Parameters Update Parameters (a) (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.

Error Linear Unit (GELU) activation function, as speciied in Equation (5),

GELU(h) = h · 21 (1 + Φ( √h√2 )) (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(X𣠀𨐀𨐀𦰀W1 + b1), (6) fc2 = GELU(fc W + b2), 1 2

where W1 ∈ R𤐀𦠀𧀀𤐀𤠀𦐀 ×𤐀𤰀 𤰀 𦰀, W2 ∈ R𤐀𤰀 𤰀 𦰀×𤐀𦠀𧀀𤐀𤠀𦐀 represent the projection matrices, while b1 ∈ R𤐀𤰀 𤰀 𦰀, b2 ∈ R𤐀𦠀𧀀𤐀𤠀𦐀 denote the bias vectors corresponding to the irst and second fully-connected layers, respectively. The dimension of the feed-forward network, denoted as 𤐀𤰀 𤰀 𦰀 , is established as 1024 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 ∈ R𦠀,𤐀𨰀𧀀𤀀𣠀𣰀 , where 𦠀 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 ininity values −∞ to the attention scores of future positions before the application of the sotmax function. The input matrices for the decoder’s self-attention are initialized with the outputs from the encoder’s self-attention. Speciically, 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.

12 • Y. Lu et al.

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 instruction 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 veriication worklows, requiring minimal additional setup while providing substantial beneits in test generation eiciency and coverage improvement. The ine-tuning task illustrated in Fig. 3(a) exposes a transformer model to efectively capture the sequence. Subsequently, we apply the ine-tuned model to conduct the downstream task of predicting coverage scores, as depicted in Fig. 3(b). Unlike traditional BART implementations that use text inilling as a noising method during training, our sequential modeling task is a ine-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 language tasks where partial text corruption is acceptable, hardware veriication 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 execution rules about tokens in a test sequence, and about existing training samples, the proposed model efectively learns the generation of instruction sequencing and the correlation between sequence patterns and objective coverage scores. Ö𦰀 Ö𦰀 L(x) = 𠰀 (𩐀𥠀 |x<𥠀 ) = 𠰀 (𩐀𥠀 |𩐀1, 𩐀2, ..., 𩐀𥠀 −1). (7) 𥠀=1 𥠀=1 Through model training, we can delineate the relationships between each token 𩐀𥠀 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. Furthermore, the ine-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 low. Additionally, a valid test program should achieve correct termination and maintain the integrity of both computational semantics and architectural constraints. On one hand, the ine-tuned transformer model facilitates the appropriate next tokens and execution low; 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 inal hidden state, denoted as h𦰀, of the transformer block through transformations applied in the decoder. The objective of this task is to minimize the diference between the input sequence generated by the encoder and the output sequence produced by the decoder. A cross-entropy (CE) loss function

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

                                                          1  𦐀
                                                LossMSE = 𦐀 𥠀=1 (𨀀ˆ𥠀  − 𨀀¯𥠀 )2 .                        (10)
4.5 Test Sequence Updates and Correction
The sequence update and correction process comprises three principal components: (1) A coverage score predictor,
which utilizes a transformer-based neural network consisting of two layers to map instruction sequences to
their corresponding predicted coverage scores. (2) A gradient-based optimizer employs an iterative reinement

                                                                            ACM Trans. Des. Autom. Electron. Syst.

ACM Trans. Des. Autom. Electron. Syst.

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

         Random Instruction Stream Generator

         Architecture Model
         G0;03<9:2; 5; =:;0
Python Test        Registers
 Templates  Template  Instruction    /01 23 4
             Paser
                          CS@   56708 9:2;     É
                                Handler
 @FF001 J ?40
     1 J ?4
 @FF    J ?4
@FF
     ?0F
   II:?0F:
 I:?0F      Sequence      Data
           Generator   Generator
                                S:1 > ?<923 @BC F
5H I I:?0F     É


     Instruction Set Simulator


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

                                ACM Trans. Des. Autom. Electron. Syst.

16 • Y. Lu et al.

                 Table 1. Descriptions of coverage metrics.

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

Table 2. Average coverage and runtime of diferent test sequence generation methods.

    20.0 DeepVerifier
    15.0 Mutation
    LSTM
    10.0

    5.0

    0.0

    −5.0

    Test Sequences IDs

    ACM Trans. Des. Autom. Electron. Syst.

100  200  300  400  500  600  700  800  900 1,000

18 • Y. Lu et al.

suggests that the simpler sequential modeling of LSTM fails to capture the complex dependencies present in
assembly code efectively.

                     20.0     Line
                     15.0    Branch
                             Toggle
                     10.0

                      5.0

                      0.0

                     −5.0


    Test Sequences IDs

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

                         20.0     Line
                         15.0    Branch
                                 Toggle
                         10.0

                          5.0

                          0.0

                         −5.0


    Test Sequences IDs

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

                             20.0     Line
                             15.0    Branch
                                     Toggle
                             10.0

                              5.0

                              0.0

                             −5.0


    Test Sequences IDs

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


ACM Trans. Des. Autom. Electron. Syst.

100  200  300  400  500  600  700  800  900  1,000








100  200  300  400  500  600  700  800  900  1,000








100  200  300  400  500  600  700  800  900  1,000

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

    # of Test Cases # of Test Cases
    (a) (b)

    ACM Trans. Des. Autom. Electron. Syst.

0 200  400  600  800  1, 000    0 200  400  600  800  1, 000

Fig. 11. (a) Training loss of the transformer language model; (b) Training loss of coverage prediction model.

ACM Trans. Des. Autom. Electron. Syst.

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

  Test Sequences IDs    Test Sequences IDs
  (c)                          (d)

Fig. 12. (a) ∼ (c) Deviation of predicted line, branch, and toggle coverage with the ground truth in the test dataset. (d)
Comparison of predicted error between transformer and LSTM model body.

6 Conclusion
Veriication eforts are heavily based on the quality and diversity of test sequences, which are essential for efective
veriication practices. The coverage-directed random generation method produces various test sequences; however,
it requires human input to create test templates and conigure architectures. In addition, achieving coverage with
simulators can be a time-consuming process.
          To harness the capabilities of language models for semantic representation and eicient sequence generation,
we propose a coverage-directed test generation strategy that employs a transformer model and a coverage
predictor based on randomly generated test sequences. This strategy can integrate semantic representations of
instructions, quickly align coverage predictions to illustrate the relationship between sequences and coverage,
and ultimately enhance sequences for improved coverage.
              While our current work demonstrates efectiveness on the RISC-V processor implementation, we acknowledge
several important directions for future research, to enhance the scalability to evaluate DeepVeriier on larger

                                                                               ACM Trans. Des. Autom. Electron. Syst.










Toggle Coverage (%)    Line Coverage (%)

100  200  300  400  500  600  700  800  900  1,000  100  200  300  400  500  600  700  800  900  1,000







100  200  300  400  500  600  700  800  900  1,000  100  200  300  400  500  600  700  800  900  1,000

                                 conigurations with more complex out-of-order execution features, we need to investigate performance on
                            designs with advanced features and handle increased state space in larger processor designs. In addition to
                    exploring the generalizability of DeepVeriier, we need to extend to support other designs and adapt the instruction
                            embedding and tokenization schemes for diferent ISAs. Create a more generic coverage modeling approach that
                        can accommodate diverse architectural features, and the current implementation can serve as a proof-of-concept,
                                and extensions would help establish DeepVeriier as a more comprehensive veriication solution for modern

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

 207ś212.

ACM Trans. Des. Autom. Electron. Syst.