CHARGE: Leveraging CWE Hierarchies for Hardware Security SystemVerilog Assertion Generation Xiao Tan
UNC Chapel Hill Chapel Hill, North Carolina, USA [email protected]
arXiv:2607.27776v1 [cs.CR] 30 Jul 2026
Abstract This paper presents CHARGE, an automated framework for generating security properties for unverified RTL modules using CWEs and large language models (LLMs). The hallmark is a reasoning process that leverages the hierarchical nature of CWE entries to improve accuracy when identifying security-critical assets in unverified RTL modules. As a result, the approach can infer expected security behaviors and generate properties from identified assets and CWE semantics, avoiding the need for trusted design specifications and reducing manual engineering effort. We evaluate the framework on the Hack@DAC18, 19, and 21 open source SoC designs using OpenAI’s GPT-4.1. CHARGE detects 27 of 42 known bugs in these designs. For Hack@DAC21 OpenPiton SoC, 89% of the generated SVAs run in Cadence JasperGold FPV, and 92.2% are non-vacuous. We compare to an open-source, manually written set of properties for these designs and find that CHARGE correctly writes properties for three bugs in which the manually written properties were incorrect. In addition, CHARGE-generated properties identify a new bug in the Hack@DAC21 OpenPiton SoC that was not previously identified.
CCS Concepts • Security and privacy → Hardware security implementation; • Hardware → Electronic design automation.
Keywords Hardware Security, CWE, SVA, LLM
This paper is an extended version of the paper accepted to the IEEE/ACM International Conference on Computer-Aided Design (ICCAD 2026).
1
Introduction
Insecure hardware can lead to compromise of the entire system [4]. To protect against this outcome, security verification early in the design life-cycle aims to find weaknesses in the design that could be exploitable post-deployment. Verification techniques differ, but many rely on finding assertion failures in the design. For example, model checking can prove a design will never violate an assertion [29]. While less formal techniques, such as symbolic execution [26, 27] or fuzzing [15, 19, 21] can find instances of assertion violations in large designs. Unfortunately, the verification outcomes are only as strong as the set of assertions used, and writing a comprehensive set of assertions is a challenging and time-consuming task [14]. In the past,
Cynthia Sturton
UNC Chapel Hill Chapel Hill, North Carolina, USA [email protected] techniques involving behavior mining from traces of execution [32], translating properties from one design to another [33], or using a set of templates to generate properties [24] have been used. More recently, a body of work is emerging exploring the use of large language models (LLMs) to generate assertions [13]. Two major challenges to using LLMs to generate assertions persist. The first is that LLMs need quite detailed guidance in order to produce meaningful and accurate assertions [13]. The second is that if the goal is to use the assertions to find bugs in the design, then the design itself cannot be assumed to be bug-free and cannot act as a clean specification to feed to the LLM. In the context of functional verification, these challenges are being successfully addressed by providing the LLM with the design’s specification, which details signal names, timing, and expected behavior. In the context of security verification, however, no such design-specific specifications exist. There are established high-level security goals, for example the Common Weakness Enumeration (CWE) database [20], but these are not design specific, and mapping the high-level goals to the signals, timing, and behavior of a particular design is challenging. To address these challenges, we present CHARGE (CWE Hierarchy AsseRtion Generation Engine), an automated framework that leverages the hierarchical structure of the CWE database to guide LLMs to generate security assertions directly from unverified RTL. We use the CWE entries in lieu of a specification and use a threestep framework to guide the LLM. In the first step, the hierarchy of the CWE is used to guide the LLM toward identifying the relevant assets (signals) in the given RTL. In the second step, the target CWE is used to guide the LLM toward naming the expected behavior of the assets. In the third step, the gathered information is used to prompt the LLM to generate a SystemVerilog Assertion (SVA) that would catch a violation of the target CWE. We compare the assertions generated by our framework with those manually written for recent Hack@DAC SoC designs (2018 [9], 2019 [10], and 2021 [11]) and provided in the open-source Verification Benchmark repository [25]. In our experiments CHARGE generates assertions that detect 27 out of 42 bugs. For assertions generated on Hack@DAC 2021 SoC, 89% of the assertions can be directly used in the JasperGold FPV environment without syntax errors or using invalid signals. For the 15 undetected bugs, we analyze the failure cases and find that some target CWEs tend to be more difficult for the LLM, which aligns with prior findings [2] and that longer RTL modules are more challenging as well. Moreover, CHARGE generates an assertion that finds an undocumented bug in Hack@DAC 2021’s OpenPiton SoC, and we reported this issue to Hack@DAC 2021’s organizers. We also find three instances where CHARGE produces a correct property, but the manually written property in the Verification Benchmark repository was incorrect,
and we reported this issue to the maintainers of the repository. Lastly, we discuss the position of CHARGE in the context of related work, technical considerations, and the scope and limitations of our evaluation. Our main contributions are the following. • We present a methodology to leverage the hierarchical nature of CWEs to address the challenges in generating security SystemVerilog Assertions directly from unverified RTL. • We implement the methodology in CHARGE, an automated framework that takes as input a target CWE and an unverified RTL module, and generates a set of SVAs. • We evaluate our framework on the Hack@DAC 2018, 2019, and 2021 SoCs, and compare to open-source, manually written properties. CHARGE generates assertions that detects 27 out of 42 bugs, detect one previously unreported bug, and corrects three of the manually written properties.
the potentially buggy RTL is the only source of context, which can be misleading for LLMs and embed the bug inside the generated SVA. Therefore, it is important to find a better way to guide LLMs to generate security SVA directly from the buggy RTL, which is the motivation of our work.
3
2 Background 2.1 Assertioned Based Verification Assertion-based verification (ABV) is a widely adopted technique in hardware verification, which uses assertions to specify the expected behavior and check the correctness of the design under verification. SystemVerilog Assertions (SVA) is a commonly used property specification language in hardware verification, which allows designers to specify properties that can be expressed in terms of linear temporal logic. SVA can be used to specify both functional and security properties of a design. Functional properties usually originated from the design specification, while security properties are often highly dependent on the professional expertise of the engineer, as there is no formal specification for security properties of a design. Therefore, generating security SVA is often more challenging than generating functional SVA. SVAs are often manually written by engineers, which is time-consuming. Therefore, there is a growing interest in automatically generating SVA, both functional and security, to improve the efficiency of hardware verification.
2.2
Using the Common Weakness Enumeration
The Common Weakness Enumeration database (CWE) is a standardized taxonomy and database of security weaknesses maintained by MITRE [20]. The database is widely used to describe, categorize, and analyze weaknesses in both software and hardware. Each CWE entry includes a unique ID, a name, a description of the weakness, possible mitigations, and examples of vulnerable implementations. CWE entries do not describe particular vulnerabilities in a particular codebase. Rather, they describe a type of weakness to be avoided. CHARGE uses the CWE database as a specification of desirable security properties. However, the name and description of each CWE entry are in natural language, which cannot be directly used for verification. Therefore, we need to decompose the CWE descriptions into a structured format that can be used for property generation. In this section, we will explain how we decompose the CWE descriptions into a 3-tuple format, how we select the CWEs covered by our framework, and how we build the CWE tree based on the hierarchy.
3.1
Extracting Structured Data from a CWE
Each CWE entry describes a weak or vulnerable pattern in code. By extracting the data from each CWE entry we can specify an associated property. We use a 3-tuple to represent the specified security property: ⟨target, action, condition⟩, where • target is the sensitive hardware asset being protected, such as cryptographic key, data, memory region; • action is the operation performed on the target, such as read, write, zeroize; and • condition is the set of constraints on which the action is prohibited or allowed, typically composed of signals such as privilege level, lock bits, and status flags.
LLMs for SVA generation
LLMs show great potential in understanding natural language, and have been applied in code generation and analysis. Recently, there are research efforts in using LLMs to automatically generate SVA, which can significantly reduce the manual engineering effort. However, there are non-trivial challenges existing in this process. First, the generated SVA needs to be syntactically correct and able to be directly used in verification tools. This is challenging becasue the commercial LLMs are not heavily trained on Hardware description language (HDL) and SVA, and a lot of engineering effort is required to refine the generated SVAs. Some works have addressed this challenge by fine-tuning LLMs on open source hardware designs, while this is also limited by the availability of such datasets, comparing to the software code and natural language dataset. Second, the generated SVA needs to be semantically meaningful and able to correctly express the expected behavior of the design. For functional SVA generation, there are existing works that use LLMs to generate properties from design specification, which serves as a ground truth of how the design should behave. However, for security SVA generation, there is no formal specification and therefore
For example, CWE-226: Sensitive Information in Resource Not Removed Before Reuse has the following description: “The product releases a resource such as memory or a file so that it can be made available for reuse, but it does not clear or zeroize the information contained in the resource before the product performs a critical state transition or makes the resource available for reuse by other entities.” The structured 3-tuple for this CWE is: ⟨sensitive resources, sanitization, reuse/release condition⟩ And, a template SVA for this CWE is:
Listing 1: Template SVA for CWE-226 1 property CWE_226 ; 2 @( posedge clk ) 3 ( reset_trigger_event ) |-> or |= > 4 ( resource_sensitive_data == '0) 5 endproperty
2
The 3-tuple provides a structured representation of the security property encoded in the CWE description, and is used by CHARGE for categorizing assets and specifying the SVA templates for assertion generation.
3.2
3.3
Capturing the Hierarchy of CWE Entries
To leverage the hierarchical nature of the CWE entries, we build a tree of CWE entries. The root of the tree is CWE-1000: Research Concepts. As stated in MITRE’s website [20], “[CWE-1000] is mainly organized according to abstractions of behaviors instead of how they can be detected, where they appear in code, or when they are introduced in the development life cycle.” This view uses a deep hierarchical organization, with more levels of abstraction than other classification schemes. The large tree has 10 subtrees, one for each of the 10 Pillars in CWE-1000. These pillars express high-level security intents. The subtrees are stored in JSON format. For each CWE node inside the subtree, we store its CWE-ID, name, description, mapping status (whether it is mappable or discouraged by MITRE), and its children nodes. Only CWEs that are mappable and covered by our framework can be used as target CWEs for CHARGE. The CWE hierarchy is built once and is part of the CHARGE framework. We start from each mappable CWE, trace upward following the "Child Of" relationship, building the edges and intermediate nodes until we reach a pillar. In this framework, we consider only the Parent–Child relationship. Other relationships in the CWE1000: Research Concepts, such as CanPrecede and CanFollow, are excluded because they do not encode strict hierarchical structure and would unnecessarily complicate the framework. Each CWE node has an additional field, “asset identification,” which includes three subfields (target, action, condition) that are used to build the prompt strings used for asset identification in step 1 of the framework (Sec. 4.1). Figure 1 shows an example of the sequence of prompt strings for CWE-226, starting from the root node (CWE-664). Importantly, our methodology assumes that the CWE database is organized hierarchically and that a child CWE represents a refinement of its parent. Under this assumption, newly introduced CWEs can be incorporated by inheriting and specializing the corresponding 3-tuples of their ancestors. To illustrate this process, Figure 1 includes a hypothetical child CWE, CWE-1999 (Cryptographic Keys Should Be Cleared Upon Reset). CWE-1999 inherits the sanitization-related security intuition of CWE-226 while specializing the target to cryptographic keys and the condition to reset events. Existing CWE definitions and prompts remain unchanged, enabling CHARGE to scale with the continued growth of the CWE database while preserving backward compatibility.
CWEs in Scope
Our goal is to produce SVAs that can be verified as part of a standard verification process. Consequently, our framework focuses on trace properties that can be expressed using temporal logic. CWEs that require reasoning about time or power side channels, physical environmental conditions, information-flow properties, or software or ISA-level behavior fall outside the scope of this framework and are therefore excluded. All CWEs covered by our framework come from the CWE-1194 Hardware Design view. This view contains 13 categories, based on different perspectives of hardware design. We include only CWEs from this view that are designated as “Mappable” in the CWE database. At the time of writing, MITRE lists 110 hardware-related CWE weaknesses. We classify these CWEs into two sets. A CWE is classified as convertible when its security policy can be fully represented by a single 3-tuple and mapped to an assertion template. A CWE is classified as partially convertible when only part of its security intent can be expressed in this form and additional behavioral reasoning is required. For example, CWE-226 is convertible because its security intent naturally maps to a 3-tuple: the target is the sensitive resource, the action is sanitization, and the condition is resource release or reuse. In contrast, CWE-1245 (Improper Finite State Machine) is only partially convertible. While valid state transitions can be represented using a 3-tuple, properties such as unreachable states or privilege-escalation prevention require additional reasoning beyond a single relation. This classification only describes representability within our abstraction and does not change the CHARGE workflow. Both categories are processed using the same pipeline. For partially convertible CWEs, the 3-tuple serves as an initial abstraction, and we leverage the creativity of LLMs to infer additional expected behaviors beyond those explicitly encoded in the tuple. It is important to note that the inclusion of a CWE in our framework does not guarantee that a given CWE can be successfully verified using SVA on a specific RTL module. Whether a CWE can be verified is dependent on the specific RTL module and whether the weakness manifests at the RTL level or arises from higher-level system configurations. In Section 4.2, we discuss how we determine if a CWE is verifiable for a given RTL module, which is based on whether the LLM can identify enough asset details. Other CWE-based hardware verification frameworks adopt different methodologies when selecting the CWEs they cover. For example, Don’t CWEAT It [1], a static analysis framework, classifies 96 hardware CWEs into six categories: Non-RTL, Functional Simulation, Static Analysis (no context), Static Analysis (with context), Static/RTL Elaboration, and Manual Analysis. Table 1 presents the classification of CWEs under CWE-1194.
4
CHARGE Framework
Given a target CWE ID and a RTL module, CHARGE will automatically generate a set of SystemVerilog Assertions (SVAs) that check the security policy indicated by the CWE for the given RTL. CHARGE’s workflow is illustrated in Figure 2. Two aspects of note: we assume the RTL is unverified and potentially buggy, and we do not require design specifications as input. The first step of the framework has two jobs: 1. to determine whether the given CWE is suitable for the framework, and 2. if it is, to output the assets in the RTL along with the desired behaviors and the conditions under which those behaviors hold. The output is formatted as a JSON. If the CWE is found not to be relevant, the framework reports “inapplicable CWE” in step 1. CHARGE collects 3
Classification CWE covered
CWE-ID Convertible to 3-tuple
Partially Convertible to 3-tuple
Physical Env CWE not covered
Side channel / IFP SW/Alg/ISA/System Design Require protocol info/documentation
# of CWEs
1190, 1193, 1274, 1220, 1222, 1262, 1280, 1299, 1209, 1221, 1223, 1224, 1231, 1232, 1233, 1234, 226, 1257, 1282, 1310, 1315, 1317, 1279, 1256, 1271, 1314, 1191, 1243, 1244, 1258, 1272, 1313, 276, 1254, 1239, 1330, 1270 1264, 1283, 1328, 441, 1189, 1240, 1260, 1268, 1294, 1302, 1334, 1245, 1250, 1253, 1252, 1251, 1311, 1312, 1316, 1431, 1320, 1296, 1429, 1281, 1259, 1290, 1292
37
1247, 1248, 1261, 1278, 1319, 1351, 1384, 1263, 1301, 1304, 1338, 1298, 1266, 1297 1255, 1300, 1323, 203, 1331, 1420, 1342, 1303, 319, 1421, 1422, 1423 1332, 1277, 1329, 1357, 1241, 1246, 1318, 1326, 1269 1053, 1059, 440, 1291, 1295, 325, 1192, 1242, 1267, 1276, 1273
14
27
12 9 11
Table 1: Classification of hardware CWEs in our framework.
Figure 1: Explanation of CHARGE’s Usage of CWE Hierarchies the assets from step 1 and put them under 3 categories: primary targets, primary conditions, and relevant assets. The second step takes these three categories of assets from step 1 along with the RTL and CWE and outputs the expected behavior, stated in natural language. The third step takes the natural language description from step 2, the three categories of assets from step 1, the RTL, and
CWE and outputs the generated properties. All three steps use an LLM to generate the desired output. The generated properties are in standard SystemVerilog Assertion (SVA) format and can be used with any testing or formal verification tool that accepts the SVA properties. In our evaluation, we use the Cadence JasperGold FPV model checker to check for 4
property violations, but open source verification frameworks that accept SVA properties could also be used (e.g., [27, 29]). We describe the three steps of the framework in detail next.
4.1
expected security behaviors using the CWE rather than the possibly buggy RTL. To illustrate this step, we will continue to use the same code snippet and target CWE in Step 1. We take the primary targets, primary conditions, and relevant assets identified in Step 1 as the inputs. In this example, the primary targets are prime_i, prime1_i, and msg_in; the primary conditions are r̃st_ni, rst13, en, and we; the relevant assets are msg_out,rdata, wdata . Since action expresses a behavior, we will only extract the assets involved in the action as part of the primary or relevant assets. To bridge the gap between security-critical assets and expected security behaviors, we manually craft a policy question based on the CWE’s security intent, which serves as the "action". For example, for CWE-226, the question is "under what condition should the given asset(s) be zeroized/cleared?" Each question is written once per CWE and is reused across target RTL modules. Using the identified assets, target CWE and prompt, and the unverified RTL code as context, the LLM generates a list of expected security behaviors. For example, "when reset is on, msg_out needs to be cleared," "when reset is on, prime_i needs to be cleared." These expected behaviors can then be used to generate SVAs in the next step. We stored each mappable CWE’s ID, name, description, and the prompting question all in one JSON file. When running this step, only the target CWE’s information is used. The output of this step is a list of expected security behaviors in natural language, stored in a .txt file. CHARGE will later use this list to generate SVAs in Step 3. In the user prompt, we explicitly ask the LLM to answer the prompting question and generate expected behaviors for the target CWE, as well as only use the unverified RTL code as a contextual reference. This is to avoid the issue of the LLM incorrectly assuming the behavior of the unverified RTL code. However, in some cases, the bug inside the unverified RTL code might still get baked into the expected behavior (see Section 6.4.3).
Step 1: LLM-supported Asset Identification
CHARGE starts with asset identification, which is the most critical step in the framework. Given a target CWE, CHARGE traverses the corresponding path in the CWE hierarchy, starting from the children of CWE-1000 and proceeding toward the target node. At each level, the LLM identifies candidate assets. The target CWE ID is first used by CHARGE to retrieve the corresponding hierarchical path from the stored CWE tree. The extracted path, together with the CWE hierarchy represented as a JSON file, is then incorporated into the LLM prompt. The prompt instructs the LLM to follow the extracted path when processing the CWE hierarchy JSON file. The LLM follows the path and processes the queries in the 3-tuple structure to identify assets for each CWE node. The output is a JSON file that includes the identified assets for each CWE node along the path. The user prompt is only processed once by the LLM, and the output is generated in one shot. If the LLM is not able to identify any asset for the target CWE, CHARGE will report the target CWE is not applicable to the given RTL module. Otherwise, the identified assets for the target CWE and its parent are collected as primary assets and the identified assets for other ancestors are collected as relevant assets. By starting at CWE-1000’s children, which expresses the most abstract security intuition, and querying for assets with each CWE along the path to the target CWE, CHARGE is able to identify assets relevant to the target even when the (potentially buggy) RTL does not make their relevance clear. For example, consider the buggy code snippet from Hack@DAC 2021 shown on the top right of Figure 1. Here the target CWE is CWE-226 "Sensitive Information in Resource Not Removed Before Reuse". The line of code that is commented out in the listing is missing from the RTL and is not seen by the LLM. In other words, the LLM does not see the comment; we include it here only to make the bug clear. If we ask the LLM to identify the target assets for CWE-226 without using the hierarchy of CWEs, the LLM may not identify msg_out as a potential target because the expected behavior of zeroizing msg_out during reset is missing. CHARGE’s hierarchicalbased asset identification mitigates this problem by collecting asset information from the ancestor with highest level of abstraction. Although msg_out is not being zeroized when reset, it is a target asset for CWE-664 "Improper Control of a Resource Through its Lifetime," the great-grandparent of CWE-226. Because msg_out is read and written in the module (not shown in the listing), the LLM identifies it as a relevant asset for CWE-664. Figure 1 illustrated this process on the right side. We evaluate the effectiveness of this approach in the evaluation (Section 6.2.2).
4.2
4.3
Step 3: LLM-supported SVA generation
The list of expected behaviors generated in Step 2 are then used to generate SVAs, along with the extracted assets from Step 1’s output, target CWE, unverified RTL code, and a manually crafted SVA template based on the CWE semantics. All SVA templates are stored in a JSON file, where for each mappable CWE, we include the CWE ID, name, description, and the SVA template. When running this step, only the target CWE’s information is used. Similar to the CWE tree and the prompting questions, the SVA templates are created once per CWE and reused across different RTL modules. The templates are designed to be JasperGold inline assertions. See, for example, Listing 1. The LLM is prompted to generate a set of SVAs by filling in the template based on the expected behaviors and other inputs. There’s no limit to the number of SVAs generated for each expected behavior, but each generated SVA should be mapped to at least one expected behavior. LLM is explicitly asked to only use the real RTL signals when generating SVAs, and should neither invent new signals nor use syntax that is not supported by JasperGold (e.g. using for loops to generate multiple SVAs). The output of this step is in a .sv file that includes all generated SVAs. To later
Step 2: LLM-supported Behavioral Mining
The assets extracted from Step 1’s output are then used as the inputs for mining expected security behaviors. Other inputs include unverified RTL code, the target CWE’s description, and a manually crafted policy question based on the CWE’s security intent. The motivation for this step is to prompt the LLM to generate a list of 5
Figure 2: Overview of our framework. evaluate vacuity, we also ask the LLM to generate a cover property for each generated SVA, which is in the format of "cover -name CWE226_cover (reset_trigger_event)", and is provided to LLM as part of the SVA template. This cover property is used to check if the assertion is vacuously true. After this step, we will have a set of SVAs that can be used to check the security property represented by the target CWE.
5
distinct security bugs. These bugs map to 20 unique CWEs, which share 6 common pillars in the CWE hierarchy. Our baseline evaluation (Sec. 6.2) focuses on Hack@DAC 2021, and is designed to demonstrate the effectiveness of our overall framework as well as its components across different LLMs. Using LLM generated assertions, we are able to find 3 errors for the assertions in Verification Benchmark repository, and 1 undocumented bug in Hack@DAC 2021’s OpenPiton SoC.
Implementation
We use OpenAI’s GPT-4.1 API for all LLM interactions. We set the temperature to zero to reduce the nondeterminism of LLM outputs. CHARGE is fully automated, with the necessary information automatically extracted from each step’s output and passed to the next step. The implementation of CHARGE consists of a single Python script, in which each step is implemented as a separate function along with several helper functions. The framework writes the output of each step to a separate file and logs all LLM interactions. CHARGE is available on GitHub: https://github.com/HWSecUNC/CHARGE.
6
6.1
End-to-End Bug Detection Results
We evaluate CHARGE’s performance on end-to-end bug detection by checking if the generated assertions can detect the known bugs inside the Verification Benchmarks. All the assertions generated by CHARGE are JasperGold inline assertions, and we run Cadence JasperGold FPV to check if the generated assertions can detect the known bugs. We made the following edits to the generated assertions in order to use them in JasperGold: deleting the posedge clock keywords (the designs are set up with default clocks in JasperGold environment), deleting the semicolon at the end of the assertion if it exists, and adding a pair of brackets around the assertion body if needed. To account for the nondeterminism of LLM outputs, we run CHARGE three times on each target CWE–RTL module pair. We summarize the bug detection results in Table 2. CHARGE generates useful assets for 34 out of 42 known bugs, generates meaningful expected behaviors for 29 out of 42 known bugs, and generates assertions that detect 27 out of the 42 known bugs. The “Asset” column in Table 2 is checked if all the necessary assets are named in the generated property. In other words, if one of the following three conditions holds: 1) all the assets used in the Verification Benchmark’s property’s body are in the generated assets; 2) the generated expected behaviors (“Behavior” column) will include the missing asset, and the generated behavior is meaningful for assertion generation; or 3) the generated assertions detect the bug without the missing asset. Otherwise, the column is marked with an “x”. To understand the second case, consider Hack@DAC 2021 P39. The bug is "AES plain text is left uncleared after the encryption is over in the peripheral registers". The LLM does not identify ct_valid (ciphertext valid) as the core asset after step 1. However, the LLM does identify ct (ciphertext) and pc (plaintext) as primary targets for CWE-226, and therefore, in step 2 produces the correct behavior that plaintext should be cleared when encryption
Evaluation
To evaluate CHARGE, we compare to the manually written properties for the three Hack@DAC designs in the public Verification Benchmarks repository [25]. The designs are a PULPissimo SoC (Hack@DAC 2018), a CVA6 SoC (Hack@DAC 2019), and an OpenPiton SoC (Hack@DAC 2021). The repository provides properties covering 20, 11, and 17 bugs for the three designs, respectively. Of those, the repository has marked one, one, and two properties, respectively, as “no violation found,” meaning the given property does not catch the relevant bug in the design. We exclude these four cases from our evaluation, as they do not provide a reliable groundtruth reference. We further exclude two additional cases. The first is a clock glitching bug in Hack@DAC 2018, which falls outside our scope as it requires explicit reasoning about clock frequency. The second is a hardcoded HMAC key in Hack@DAC 2021. We found that the corresponding property in the repository is incorrect, and upon manually inspecting the RTL, we were unable to manually write a property to catch this bug that wasn’t trivially tailored to the specific hardcoded value. We noted this issue in a pull request to the repository. After excluding these six bugs, our end-to-end evaluation (Sec. 6.1), which focuses on bug detection, covers 25 RTL modules and 42 6
Design
Bug
Assertion
Behavior
Asset
mux_func CWE-226 mux_func CWE-1240 riscv_cs_registers CWE-1220 riscv_cs_registers CWE-1189 adbg_tap_top CWE-1221 adbg_tap_top CWE-1244 adbg_tap_top CWE-1254 adbg_tap_top CWE-1254 riscv_alu CWE-1245 Hack@DAC18 riscv_controller CWE-1245 riscv_debug_unit CWE-1262 periph_bus_defines CWE-1260 periph_bus_defines CWE-1260 periph_bus_defines CWE-1257 axi_address_decoder_AR CWE-1245 apb_gpio CWE-1189 apb_gpio CWE-1231 soc_interconnect CWE-1189
Module
CWE
29 21 27 3 16 12 9 10 14 13 11 8 1 6 7 5 4 2
✓ ✓ ✗ ✗ ✓ ✗ ✓ ✓ ✗ ✓ ✓ ✓ ✓ ✓ ✓ ✗ ✓ ✓
✓ ✓ ✗ ✗ ✓ ✗ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✗ ✓ ✓
✓ ✓ ✓ ✗ ✓ ✗ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓
axi_node_intf_wrap csr_regfile csr_regfile Hack@DAC19 csr_regfile csr_regfile commit_stage commit_stage ariane ariane controller
CWE-1220 CWE-1262 CWE-1220 CWE-1220 CWE-1220 CWE-1281 CWE-1281 CWE-1281 CWE-1281 CWE-1281
1 9 24 25 29 21 22 23 26 32
✓ ✗ ✗ ✗ ✗ ✗ ✓ ✗ ✗ ✓
✓ ✓ ✗ ✗ ✗ ✗ ✓ ✗ ✗ ✓
✓ ✓ ✗ ✗ ✗ ✓ ✓ ✗ ✓ ✓
sha256_wrapper aes0_wrapper aes0_wrapper aes0_wrapper dmi_jtag Hack@DAC21 dmi_jtag csr_regfile reglk_wrapper reglk_wrapper rsa_wrapper acct_wrapper dma riscv_peripheral aes_192
CWE-1239 CWE-226 CWE-1258 CWE-1258 CWE-1245 CWE-1245 CWE-1262 CWE-1234 CWE-1232 CWE-226 CWE-276 CWE-1245 CWE-1310 CWE-1240
P36 P39 P46 P47 P2 P84 P18 P48 P35 P95 P42 P57 P96 P14
✓ ✓ ✓ ✓ ✓ ✗ ✗ ✓ ✓ ✓ ✓ ✓ ✗ ✓
✓ ✓ ✓ ✓ ✓ ✗ ✗ ✓ ✓ ✓ ✓ ✓ ✗ ✓
✓ ✓ ✓ ✓ ✓ ✓ ✗ ✓ ✓ ✓ ✓ ✓ ✗ ✓
Table 3: Cross-LLM evaluation of Baseline 0 and CHARGE. Metric Bug Detection Compilable Unreachable
GPT-4.1 1/14 11/14 91.1% 89.0% 0% 7.8%
Gemini 2.5 Pro 6/14 11/14 91.5% 97.0% 9.3% 5.9%
Claude Sonnet 4.6 3/14 11/14 97.1% 97.4% 2.7% 9.3%
Table 4: Baseline 1: Asset identification accuracy across different LLMs. Model GPT-4.1 Gemini 2.5 Pro Claude Sonnet 4.6
Hierarchy+3Tuple 30/41 37.5/41 38/41
3Tuple 21.5/41 28/41 35.5/41
None 18.5/41 24.5/41 32/41
6.2.1 Baseline 0. In this experiment, we prompt the LLM to generate assertions to verify the given CWE for the given unverified RTL module. The prompt includes explicit instructions to use real RTL signals. We evaluate the generated assertions on three aspects: syntax correctness, reachability, and bug detection result. Table 3 shows the results. 6.2.2 Baseline 1. In this experiment, we evaluate the effect of using CWE hierarchy and 3-tuple structure on asset identification. We compare three configurations in Step 1 of CHARGE’s framework: 1. Hierarchy + 3-Tuple: the standard CHARGE workflow for asset identification, which leverages both the CWE hierarchy and the 3-tuple structure; 2. No hierarchy + 3 Tuple: explicitly prompting the LLM to only identify assets that are relevant to the target CWE, based on the <target, action, condition> structure; 3. No hierarchy + No 3 Tuple: explicitly prompting LLM to only identify assets relevant to the target CWE, and not leveraging the 3-tuple structure. We run each configuration three times per target CWE–RTL module pair, and we introduce a scoring system to evaluate the quality of the generated assets. For each bug, we first check the number of core assets that are used in the manually written properties in Verification Benchmarks. One asset corresponds to one point. Then we check how many of those core assets can be found in the generated assets across the three configurations. To account for the nondeterminism of LLM outputs, if an asset can be found in all 3 runs, then we mark that asset as "found" and give 1 point; if an asset can be found in 1 or 2 out of 3 runs, then we mark that asset as "partially found" and give 0.5 points; if an asset cannot be found in any of the three runs, then we mark that asset as "not found" and give 0 points. Table 4, summarizes the performance of each configuration on asset identification.
Table 2: Bug detection results across Hack@DAC Designs
is over. We neither identify nor input ct_valid into step 2, but LLM is able to produce it in its output. We determine whether a generated behavior is meaningful for assertion generation through manual inspection of the RTL and “Bug Description” in the Verification Benchmark. Meaningful behavior is in some sense the opposite of the buggy behavior. To check whether the generated assertion can detect the bug, we run JasperGold FPV with the generated assertion, and check whether the assertion is violated by the buggy design, and if so, then either the generated assertion must be semantically equivalent to the manually written property in the Verification Benchmarks that detects the same bug; or we determine through manual inspection of the RTL that the violation is detecting the same bug.
6.2
Method Baseline 0 CHARGE Baseline 0 CHARGE Baseline 0 CHARGE
Comparing to a Baseline
In these experiments we evaluate the effectiveness of each of the features of CHARGE. The experiments are all conducted on the Hack@DAC 2021 OpenPiton SoC design, which has 14 known security bugs, covering 10 unique CWEs and 10 unique RTL modules. As before we run each configuration three times per target CWE–RTL module pair. Moreover, to evaluate the cross-LLM generalization capability, we run CHARGE using three models for each Baseline experiment: GPT-4.1, Gemini 2.5 Pro, and Claude Sonnet 4.6.
Summary. Tables 3 and 4 show that CHARGE consistently improves over the corresponding baselines in both bug detection and asset identification across all three models. These results suggest that the gains primarily arise from CHARGE’s hierarchical reasoning and structured decomposition rather than from a particular LLM. Detailed per-benchmark results are provided in the Appendix. 7
6.3
have an average of 1180 lines of code per module. For example, 5 failure cases are from the csr_regfile module, which has more than 1000 lines of code. • The expected behavior is not within the training data of the LLM: In some cases, the LLM was able to identify the assets, but was not able to build a connection between these assets to generate the expected behavior that can enforce the security property represented by the target CWE. We suspect that this is because the expected behavior between these assets is not within the training data of the LLM.
Finding Errors in the Manually Written Properties
During the course of our evaluation, we found that three of the manually written properties in the public Verification Benchmarks repository were incorrect and CHARGE’s generated properties were correct. In the Hack@DAC 2018 P29 mux_func module and Hack@DAC 2021 P95 rsa_wrapper module, the manually written properties used the overlapped implication operator, while the correct operator should be non-overlapped implication. In the Hack@DAC 2018 P8 periph_bus_defines module, the manually written property specified the wrong address range for checking address overlap, while CHARGE’s generated property specified the correct address range. We reported these issues to the public repository, and our pull requests have been accepted.
6.4
6.4.3 Type2: Behavior/Assertion Generation is Misled by the RTL. In the second category of failure cases, the LLM is able to build a connection between the identified assets, but the connection is wrong (often the opposite). The bugs in this category are Hack@DAC 2018 P5, Hack@DAC 2019 P9, and Hack@DAC 2021 P84. We suspect the LLM is misled by the buggy RTL. For example, in Hack@DAC 2021 P84, the target CWE is CWE-1245 Improper FSM. The expected state transition is missing from the RTL, so the LLM excludes the state from the valid next states.
Failure Mode Analysis
CHARGE is evaluated on 42 known bugs, and 15 of them are not detected by the generated assertions. We analyze the failure modes of these 15 cases, and discuss the limitations of our framework.
6.5
6.4.1 Commonality of failure cases. Our evaluation covered 20 unique CWEs. The 15 undetected bugs are mapped to 7 unique CWEs: 4 bugs are mapped to CWE-1220, 2 bugs are mapped to CWE-1245, 2 bugs are mapped to CWE-1189, 2 bugs are mapped to CWE-1262, 3 bugs are mapped to CWE-1281, 1 bug is mapped to CWE-1244, and 1 bug is mapped to CWE-1310. These 7 CWEs share 4 common ancestors in the CWE hierarchy: CWE-284 (3 children), CWE-710 (2 children), CWE-664 (1 child), and CWE691 (1 child). This result suggests that the failure cases are not randomly distributed across target CWEs. The LASHED paper [2] also found “a significant variation [in] success based on the CWE.” Although the troublesome target CWEs are mostly different for the two frameworks, these results suggest that LLM-based assertion generation is sensitive to choice of CWE. Our findings also suggest that the length of the RTL module is a factor affecting performance. The 27 bugs CHARGE is able to detect originated from 19 different modules with an average of 355 lines per module. The 15 bugs CHARGE is not able to detect originated from 10 different modules with an average of 872 lines per module. Furthermore, 11 of the 15 undetected bugs are from 6 modules with more than 800 lines of code each.
Case Study: Unknown Security Weakness Detection
CHARGE generated an assertion for CWE-226 in aes0_wrapper module that is violated by the design, but not on the HACK@DAC21 bug list. The generated assertion states that key material should be cleared on reset and is given in Listing 2. Listing 2: The assertion detecting an unknown security flaw 1 2 3 4
assert - name reset_p1 { (! aes0_wrapper_i . rst_ni || aes0_wrapper_i . rst_1 ) |= > ( aes0_wrapper_i . key0 == '0) }
Using JasperGold FPV, we constructed a trace as a cover property showing that reset occurs, no key write happens after reset, but AES encryption is initiated, the key used is non-zero and originates from pre-reset state, and the key is actively used in the AES computation. The trace is reachable and indicates that the key material is retained and reused across reset. This behavior violates a standard security property: cryptographic keys should be cleared upon reset. We reported this issue to the Hack@DAC 2021 repository.
6.4.2 Type1: Missing Asset/Behavior. We further classified the 15 undetected cases into two categories. The first is failure due to the LLM missing the asset or behavior. The bugs in this category are Hack@DAC 2018 P3, 27, 12, 14; Hack@DAC 2019 P21, 24, 25, 29, 23, 26; Hack@DAC 2021 P18, 96. We identify four root causes:
6.6
Bug-to-CWE Mapping Algorithm leveraging CWE Hierarchy
In the Verification Benchmarks repository some bugs have no assigned CWE while others have CWEs that is marked as "Discouraged" on Mitre’s CWE website. To address this issue, we leverage the structure of the CWE hierarchy to help with bug-to-CWE mapping. We are inspired by existing research in software security using the CWE hierarchy with an LLM to map CVEs to CWEs or Bugs to CWEs using Github’s open source bug-fix commits [22]. We use a greedy algorithm for bug-to-CWE mapping, leveraging the CWE-hierarchies. We start from the root node of the CWE hierarchy, and ask the LLM to select the most suitable child node based on the bug description and code snippet, iterating until a mappable
• CWE Mismatch: If the given target CWE does not fit the looked-for bug, the LLM will fail to identify the relevant assets for the bug. We found two instances where this was the case in the Verification Benchmarks repository. • Lack of evidence in RTL: If the core asset is completely missing from the RTL, or the evidence is too weak, the LLM will not be able to identify that asset. • Larger RTL modules and more complex behaviors: This category is mostly overlapped with the 11 undetected bugs that 8
CWE is found. Using this algorithm, we successfully mapped 7 bugs previously mapped to a Discouraged CWE in Verification Benchmarks to a mappable CWE. CHARGE successfully identifies the core assets using the newly mapped CWEs. Further research can be done to improve the preciseness by fine-tuning a model instead of using commercial LLMs, or improving the algorithm itself.
7
pipeline, including asset identification, vulnerability classification, policy generation, bug localization, and SVA generation. Consequently, they require different user inputs, produce different verification artifacts, and are evaluated on different benchmark suites. These frameworks address complementary aspects of hardware security verification. As shown in Table 6, recent frameworks have explored a variety of ways to incorporate CWE knowledge, including vulnerability classification, threat modeling, asset identification, and property generation. Together, these approaches demonstrate the value of CWE as a source of security knowledge for hardware verification. CHARGE differs from these approaches in that it treats the CWE taxonomy as a structured knowledge source rather than using individual CWE descriptions in isolation. By combining hierarchical relationships, a 3-tuple abstraction, and assertion templates, CHARGE provides a systematic and reusable methodology for transforming CWE knowledge into security verification artifacts, including assets, security intent, and SVAs. This approach also enables newly introduced CWEs to be incorporated by inheriting and refining the security knowledge of their ancestors, allowing CHARGE to evolve naturally with the CWE taxonomy. Existing approaches such as AST-based representations, retrievalaugmented generation, iterative refinement, and agent-based reasoning are largely orthogonal to CHARGE. These techniques improve the quality of assertion generation once the desired security intent is available, whereas CHARGE focuses on systematically deriving that security intent from RTL and structured CWE knowledge.
Related Work
Using LLMs to Generate Properties. Current work on using LLMs to generate SVA can be categorized across two axes: using commercial LLMs with prompt engineering vs. using customized LLMs, and generating security SVA vs. generating functional SVA. For functional SVA generation, design specification is usually provided as a ground truth, while for security SVA generation, there’s more variation in the input context, as there is no formal specification for security properties of a design. Examples of frameworks for generating functional SVAs not using customized LLMs include FLAG [28] and ChIRAAG [16]. AssertLLM [7] uses customized LLMs, and VERT [18] presents an open-source dataset that can help with fine-tuning LLMs for SVA generation. Kande et al. [13] are one of the first to explore the use of LLMs to generate security SVA. SVAgent [8] uses prompt engineering to break down the security SVA generation process into subquestions. Meng et al. [17] proposed an automated NLP-based security property generator. Using CWEs to Generate or Validate Properties. CWEAT [1] uses CWEs to guide static analysis of early-stage hardware designs by building scanners for RTL, each designed to detect the potential weaknesses associated with a specific CWE. Other work includes DIVAS [23], which uses LLMs to identify relevant CWEs and generate security SVA; LASHED [2], which uses the LLM to identify assets for 5 different CWEs, and then uses static analysis to produce SVAs; and SoCureLLM [31], which uses CWEs to represent the set of vulnerabilities, and divides a large codebase into smaller parts to delegate to different LLMs.
8.2
Technical Considerations
Runtime. CHARGE typically requires less than one minute to generate SVAs for a given RTL module and target CWE, including three LLM calls. Runtime is primarily determined by RTL size and API latency. Property validation in Cadence JasperGold typically requires less than one minute per run to either prove the property or generate a counterexample. Toolchain Dependencies. CHARGE is compatible with Python 3.10+ and currently relies on commercial LLM APIs together with the Cadence JasperGold formal verification tool. Aside from these dependencies, the framework itself is fully automated, with intermediate outputs generated and propagated between stages without manual intervention. Portability. CHARGE generates standard SystemVerilog Assertions (SVAs) and is therefore applicable to verification environments that support SVA. In the current implementation, the final prompting stage includes JasperGold-specific constraints to avoid unsupported language constructs such as for loops and genvar. Adapting CHARGE to another SVA-compatible verification environment therefore primarily requires modifying the final prompting stage, while the identified assets and inferred security behaviors remain unchanged.
Mining Design Behavior to Generate Properties. GoldMine [32] automatically generates assertions by mining data from simulation traces and using static analysis of RTL designs. Isadora [5] focuses on mining information flow properties from RTL designs. Deutschbein et al. [6] evaluates security specification mining for a CISC architecture, and targets properties written at the ISA level. Automatically Translating Properties. Transys [34] translates security properties written for one hardware design to analogous properties suitable for a second design. Transys works on both trace property and informational flow property, and the translation is not using LLMs. Writing Properties Manually. Rogers et al. [25] developed 120 SystemVerilog Assertions for four open-source designs, and they are available in the Verification Benchmark repository. We use these assertions as a benchmark to evaluate the effectiveness of CHARGE.
8 Discussion 8.1 Positioning of CHARGE
8.3
Scope and Limitations of the Evaluation
We evaluate CHARGE using the Hack@DAC designs together with the reference properties provided by the open-source Verification Benchmarks repository [25]. The Hack@DAC designs
Table 5 summarizes recent LLM-based hardware security frameworks. Existing approaches span different stages of the verification 9
Table 5: Recent LLM-based frameworks for hardware security verification and analysis. Framework Assertain [30] LAsset [12] LASSO [3]
Open Source Tool ✗ ✗ ✓
Evaluation Benchmarks 11 RTL designs NEORV32, OpenTitan/OpenCores MIT-CEP, OpenTitan, Hack@DAC24
✗
Hack@DAC21, OpenTitan, e203, Veerwolf
SVAgent [8]
Final Output SVAs Security Asset List SVAs, Bugs, Coverage report Bug explanation and localization SVAs
✗
TrustHub, HOST, PyVerilog
✗
CHARGE
Violation report, Security policies SVAs
Hack@DAC18, TrustHub, HOST22, CVA6, Ibex, CV32E40P 25 RTL modules from Hack@DAC18/19/21
LASHED [2]
Required User Input RTL + Threat Model RTL (+ optional Spec.) RTL + Specification + Documentation RTL + Target CWE
RTL + Threat Model + Security requirement SoCureLLM [31]RTL RTL + CWE ID
✓
Table 6: Comparison of how recent frameworks utilize CWE knowledge. Framework CWEAT [1] DIVAS [23]
Highlighted CWE Usage 5 CWE-specific static-analysis scanners. Generates security properties using CWEs derived from design specifications Uses CWEs as predefined threat models to decompose security requireSVAgent [8] ments into sub-questions. LASHED [2] CWE-specific asset identification and analysis (5 CWEs). SoCureLLM [31]CWE-inspired threat models and security policies. LAsset [12] Maps identified assets to relevant CWEs for validation. Assertain [30] Maps RTL and threat model to CWEs, then generates properties for the intersection of the two CWE sets. CHARGE Uses CWE hierarchies, 3-tuples, and assertion templates to derive assets, security intent, and generate SVAs from RTL.
provide buggy RTL implementations, while the Verification Benchmarks repository provides manually written security properties that serve as ground truth. These reference properties enable comparison of identified assets, inferred expected security behaviors, and bug-detection capability. Our evaluation is limited to benchmark cases for which both buggy RTL implementations and reference properties are available within the selected Hack@DAC designs. Consequently, although CHARGE supports a broader set of hardware CWEs, not all supported CWEs are represented in the current benchmark suite. Extending the evaluation to additional benchmark suites and hardware designs is an important direction for future work and would enable assessment of a broader set of CWEs.
9
Systematic CWE Reasoning Framework ✗ ✗ ✗ ✗ ✗ ✗ ✗ ✓
Acknowledgments We are grateful for the feedback we received from anonymous reviewers; the paper benefited from their insights and questions. This paper reports on work supported by the National Science Foundation under Grant No. CNS2247754 and by Intel under the Scalable Assurance program. This research was also funded in part by a Summer Undergraduate Research Fellowship from the Office for Undergraduate Research at the University of North Carolina at Chapel Hill.
Conclusion
We have presented CHARGE, an LLM-based automated framework for generating security SVAs for unverified RTL designs. CHARGE leverages the hierarchical nature of CWE entries to guide the LLM toward more accurate and reliable asset identification. In our evaluation, CHARGE produces SVAs that catch 27 of 42 bugs in recent Hack@DAC designs. When comparing to an open-source set of manually written properties, CHARGE identifies three errors in the set, producing the correct SVAs. Furthermore, CHARGE generates an SVA that identifies a previously unreported bug in the Hack@DAC 2021 design. 10
References
[21] Sujit Kumar Muduli, Gourav Takhar, and Pramod Subramanyan. 2020. HyperFuzzing for SoC Security Validation. In 2020 IEEE/ACM International Conference On Computer Aided Design (ICCAD). 1–9. [22] Shengyi Pan, Lingfeng Bao, Xin Xia, David Lo, and Shanping Li. 2023. Finegrained Commit-level Vulnerability Type Prediction by CWE Tree Structure. In 2023 IEEE/ACM 45th International Conference on Software Engineering (ICSE). 957–969. doi:10.1109/ICSE48619.2023.00088 [23] Sudipta Paria, Aritra Dasgupta, and Swarup Bhunia. 2023. DIVAS: An LLM-based End-to-End Framework for SoC Security Analysis and Policy-based Protection. arXiv:2308.06932 [cs.CR] https://arxiv.org/abs/2308.06932 [24] F. Restuccia, A. Meza, and R. Kastner. 2021. AKER: A Design and Verification Framework for Safe andSecure SoC Access Control. arXiv:2106.13263 [cs.CR] [25] Jayden Rogers, Niyaz Shakeel, Xiao Tan, Samantha Espinosa, Divya Mankani, Cade Chabra, Kaki Ryan, and Cynthia Sturton. 2025. Hardware Security Benchmarks for Open-Source SystemVerilog Designs. In Proceedings of the Secure Development Conference (SecDev). IEEE. https://github.com/HWSec-UNC/verificationbenchmarks [26] Kaki Ryan and Cynthia Sturton. 2023. Sylvia: Countering the Path Explosion Problem in the Symbolic Execution of Hardware Designs. In Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design (FMCAD). TU Wien Academic Press, New York, NY, USA, 110–121. https://repositum.tuwien.at/ handle/20.500.12708/188806 [27] Kaki Ryan and Cynthia Sturton. 2025. SylQ-SV: Scaling Symbolic Execution of Hardware Designs with Query Caching. In Proceedings of the International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS). ACM. [28] Yu-An Shih, Annie Lin, Aarti Gupta, and Sharad Malik. 2025. FLAG: Formal and LLM-assisted SVA Generation for Formal Specifications of On-Chip Communication Protocols. arXiv:2504.17226 [cs.AR] https://arxiv.org/abs/2504.17226 [29] SymbiYosys (sby). [n. d.]. Front-end for Yosys-based formal verification flows. https://github.com/YosysHQ/sby?tab=readme-ov-file [30] Shams Tarek, Dipayan Saha, Khan Thamid Hasan, Sujan Kumar Saha, Mark Tehranipoor, and Farimah Farahmandi. 2026. Assertain: Automated Security Assertion Generation Using Large Language Models. arXiv:2604.01583 [cs.CR] https://arxiv.org/abs/2604.01583 [31] Shams Tarek, Dipayan Saha, Sujan Kumar Saha, Mark Tehranipoor, and Farimah Farahmandi. 2024. SoCureLLM: An LLM-driven Approach for Large-Scale Systemon-Chip Security Verification and Policy Generation. Cryptology ePrint Archive, Paper 2024/983. https://eprint.iacr.org/2024/983 [32] Shobha Vasudevan, David Sheridan, Sanjay Patel, David Tcheng, Bill Tuohy, and Daniel Johnson. 2010. GoldMine: automatic assertion generation using data mining and static analysis. In Proceedings of the Conference on Design, Automation and Test in Europe (DATE). European Design and Automation Association. [33] R. Zhang and C. Sturton. 2020. Transys: Leveraging Common Security Properties Across Hardware Designs. In IEEE S&P. IEEE. [34] Rui Zhang and Cynthia Sturton. 2020. Transys: Leveraging Common Security Properties Across Hardware Designs. In 2020 IEEE Symposium on Security and Privacy (SP). 1713–1727. doi:10.1109/SP40000.2020.00030
[1] Baleegh Ahmad, Wei-Kai Liu, Luca Collini, Hammond Pearce, Jason M. Fung, Jonathan Valamehr, Mohammad Bidmeshki, Piotr Sapiecha, Steve Brown, Krishnendu Chakrabarty, Ramesh Karri, and Benjamin Tan. 2022. Don’t CWEAT It: Toward CWE Analysis Techniques in Early Stages of Hardware Design. In Proceedings of the 41st IEEE/ACM International Conference on Computer-Aided Design (San Diego, California) (ICCAD ’22). Association for Computing Machinery, New York, NY, USA, Article 157, 9 pages. doi:10.1145/3508352.3549369 [2] Baleegh Ahmad, Hammond Pearce, Ramesh Karri, and Benjamin Tan. 2025. LASHED: LLMs And Static Hardware Analysis for Early Detection of RTL Bugs. arXiv:2504.21770 [cs.CR] https://arxiv.org/abs/2504.21770 [3] Dinesh Reddy Ankireddy, Sudipta Paria, Aritra Dasgupta, Sandip Ray, and Swarup Bhunia. 2025. LASSO: LLM-Aided Security Property Generation for Assertionbased SoC Verification. In 2025 ACM/IEEE 7th Symposium on Machine Learning for CAD (MLCAD). 1–10. doi:10.1109/MLCAD65511.2025.11189178 [4] Ghada Dessouky, David Gens, Patrick Haney, Garrett Persyn, Arun Kanuparthi, Hareesh Khattri, Jason M. Fung, Ahmad-Reza Sadeghi, and Jeyavijayan Rajendran. 2019. Hardfails: insights into software-exploitable hardware bugs. In Proceedings of the 28th USENIX Conference on Security Symposium (Santa Clara, CA, USA) (SEC’19). USENIX Association, USA, 213–230. [5] Calvin Deutschbein, Andres Meza, Francesco Restuccia, Ryan Kastner, and Cynthia Sturton. 2021. Isadora: Automated Information Flow Property Generation for Hardware Designs. In Proceedings of the 5th Workshop on Attacks and Solutions in Hardware Security (Virtual Event, Republic of Korea) (ASHES ’21). Association for Computing Machinery, New York, NY, USA, 5–15. doi:10.1145/3474376.3487286 [6] Calvin Deutschbein and Cynthia Sturton. 2020. Evaluating Security Specification Mining for a CISC Architecture. In 2020 IEEE International Symposium on Hardware Oriented Security and Trust (HOST). 164–175. doi:10.1109/HOST45689. 2020.9300291 [7] Wenji Fang, Mengming Li, Min Li, Zhiyuan Yan, Shang Liu, Hongce Zhang, and Zhiyao Xie. 2026. AssertLLM: Generating and Evaluating Hardware Verification Assertions from Design Specifications via Multi-LLMs. arXiv:2402.00386 [cs.AR] https://arxiv.org/abs/2402.00386 [8] Rui Guo, Avinash Ayalasomayajula, Henian Li, Jingbo Zhou, Sujan Kumar Saha, and Farimah Farahmandi. 2025. SVAgent: AI Agent for Hardware Security Verification Assertion. arXiv:2507.16203 [cs.CR] https://arxiv.org/abs/2507.16203 [9] Hack@DAC 2018 Phase 2 Buggy SoC. [n. d.]. https://github.com/hackdac/ hackdac_2018_beta [10] Hack@DAC 2019 Alpha Stage SoC. [n. d.]. https://github.com/HACK-EVENT/ hackatdac19 [11] Hack@DAC 2021 SoC. [n. d.]. https://github.com/HACK-EVENT/hackatdac21 [12] Md Ajoad Hasan, Dipayan Saha, Khan Thamid Hasan, Nashmin Alam, Azim Uddin, Sujan Kumar Saha, Mark Tehranipoor, and Farimah Farahmandi. 2026. LAsset: An LLM-assisted Security Asset Identification Framework for Systemon-Chip (SoC) Verification. arXiv:2601.02624 [cs.CR] https://arxiv.org/abs/2601. 02624 [13] Rahul Kande, Hammond Pearce, Benjamin Tan, Brendan Dolan-Gavitt, Shailja Thakur, Ramesh Karri, and Jeyavijayan Rajendran. 2024. (Security) Assertions by Large Language Models. IEEE Transactions on Information Forensics and Security 19 (2024), 4374–4389. doi:10.1109/TIFS.2024.3372809 [14] Ryan Kastner, Francesco Restuccia, Andres Meza, Sayak Ray, Jason Fung, and Cynthia Sturton. 2022. Automating hardware security property generation: invited. In Proceedings of the 59th ACM/IEEE Design Automation Conference (San Francisco, California) (DAC ’22). Association for Computing Machinery, New York, NY, USA, 1384–1387. doi:10.1145/3489517.3530637 [15] Kevin Laeufer, Jack Koenig, Donggyu Kim, Jonathan Bachrach, and Koushik Sen. 2018. RFUZZ: Coverage-Directed Fuzz Testing of RTL on FPGAs. In ICAAD. 1–8. doi:10.1145/3240765.3240842 [16] Bhabesh Mali, Karthik Maddala, Vatsal Gupta, Sweeya Reddy, Chandan Karfa, and Ramesh Karri. 2024. ChIRAAG: ChatGPT Informed Rapid and Automated Assertion Generation. In 2024 IEEE Computer Society Annual Symposium on VLSI (ISVLSI). 680–683. doi:10.1109/ISVLSI61997.2024.00130 [17] Xingyu Meng, Amisha Srivastava, Ayush Arunachalam, Avik Ray, Pedro Henrique Silva, Rafail Psiakis, Yiorgos Makris, and Kanad Basu. 2023. Unlocking Hardware Security Assurance: The Potential of LLMs. arXiv:2308.11042 [cs.CR] https: //arxiv.org/abs/2308.11042 [18] Anand Menon, Samit Miftah, Shamik Kundu, Souvik Kundu, Amisha Srivastava, Arnab Raha, Gaberiel Sonnenschien, Suvadeep Banerjee, Deepak Mathaikutty, and Kanad Basu. 2025. Enhancing Large Language Models for Hardware Verification: A Novel SystemVerilog Assertion Dataset. ACM Trans. Des. Autom. Electron. Syst. (Aug. 2025). doi:10.1145/3764934 Just Accepted. [19] Samit Shahnawaz Miftah, Amisha Srivastava, Hyunmin Kim, Shiyi Wei, and Kanad Basu. 2025. SymbFuzz: Symbolic Execution Guided Hardware Fuzzing. In Proceedings of the IEEE/ACM International Symposium on Microarchitecture (MICRO). Association for Computing Machinery, New York, NY, USA, 1477–1490. doi:10.1145/3725843.3756131 [20] MITRE. [n. d.]. Common Weakness Enumeration. https://cwe.mitre.org/
Appendix
11
Table 7: Baseline 0 vs. CHARGE using GPT-4.1. Module
CWE
Bug
sha256_wrapper aes0_wrapper aes0_wrapper
1239 226 1258
dmi_jtag
1245
csr_regfile reglk_wrapper reglk_wrapper rsa_wrapper acct_wrapper dma riscv_peripherals aes_192 Results
1262 1234 1232 226 276 1245 1310 1240
P36 P39 P46 P47 P2 P84 P18 P48 P35 P95 P42 P57 P96 P14
Detection Result Baseline0 CHARGE ✗ ✓ ✗ ✓ ✗ ✓ ✗ ✓ ✗ ✓ ✗ ✗ ✗ ✗ ✗ ✓ ✗ ✓ ✓ ✓ ✗ ✓ ✗ ✓ ✗ ✗ ✗ ✓ 1/14 11/14
Compilable Baseline0 CHARGE 3/3 7/7 3/3 44/44
Unreachable Baseline0 CHARGE 0/3 0/7 0/3 0/44
5/5
25/25
0/5
0/25
4/5
33/33
0/4
0/33
3/3 3/3 5/5 6/6 0/3 3/3 3/3 3/3 41/45
21/34 14/14 19/20 28/28 6/9 33/34 13/21 39/48 282/317
0/3 0/3 0/5 0/6 N/A 0/3 0/3 0/3 0/41
8/21 0/14 5/19 4/28 1/6 3/33 1/13 0/39 22/282
Table 8: Baseline 0 vs. CHARGE using Gemini 2.5 Pro Module
CWE
Bug
sha256_wrapper aes0_wrapper aes0_wrapper
1239 226 1258
dmi_jtag
1245
csr_regfile reglk_wrapper reglk_wrapper rsa_wrapper acct_wrapper dma riscv_peripherals aes_192 Results
1262 1234 1232 226 276 1245 1310 1240
P36 P39 P46 P47 P2 P84 P18 P48 P35 P95 P42 P57 P96 P14
Detection Result Baseline0 CHARGE ✗ ✓ ✗ ✓ ✓ ✓ ✓ ✓ ✗ ✓ ✗ ✗ ✗ ✗ ✓ ✓ ✓ ✓ ✗ ✓ ✓ ✓ ✓ ✓ ✗ ✓ ✗ ✗ 6/14 11/14
Compilable Baseline0 CHARGE 8/8 24/24 6/6 65/65 6/6
63/63
5/9 27/28 3/3 3/3 3/3 3/3 24/24 0/4 9/9 97/106
Unreachable Baseline0 CHARGE 0/8 0/24 0/6 0/65 0/6
1/63
65/73
2/5
7/65
60/60 14/14 7/7 79/79 4/7 69/69 12/16 27/27 489/504
6/27 0/3 0/3 0/3 0/3 1/24 N/A 0/9 9/97
2/60 1/14 0/7 4/79 0/4 10/69 4/12 0/27 29/489
Table 9: Baseline 0 vs. CHARGE using Claude Sonnet 4.6 Module
CWE
Bug
sha256_wrapper aes0_wrapper aes0_wrapper
1239 226 1258
dmi_jtag
1245
csr_regfile reglk_wrapper reglk_wrapper rsa_wrapper acct_wrapper dma riscv_peripherals aes_192 Results
1262 1234 1232 226 276 1245 1310 1240
P36 P39 P46 P47 P2 P84 P18 P48 P35 P95 P42 P57 P96 P14
Detection Result Baseline0 CHARGE ✗ ✗ ✗ ✓ ✓ ✓ ✓ ✓ ✗ ✓ ✗ ✗ ✗ ✓ ✗ ✓ ✗ ✓ ✗ ✓ ✗ ✓ ✗ ✓ ✓ ✓ ✗ ✗ 3/14 11/14
12
Compilable Baseline0 CHARGE 30/30 74/74 24/31 108/108
Unreachable Baseline0 CHARGE 3/30 19/74 0/24 13/108
21/21
82/82
0/21
0/82
51/52
131/147
5/51
10/131
66/68 16/16 16/16 37/37 10/11 47/47 12/12 39/39 369/380
118/134 21/22 18/18 125/125 55/55 133/133 98/98 295/295 1258/1291
0/66 0/16 0/16 0/37 0/10 2/47 0/12 0/39 10/369
6/118 0/21 0/18 24/125 18/55 19/133 8/98 0/295 117/1258
Table 10: Asset identification results using GPT-4.1. Module sha256_wrapper aes0_wrapper aes0_wrapper aes0_wrapper dmi_jtag dmi_jtag csr_regfile reglk_wrapper reglk_wrapper rsa_wrapper acct_wrapper dma riscv_peripherals aes_192 Total Score Accuracy
CWE 1239 226 1258 1258 1245 1245 1262 1234 1232 226 276 1245 1310 1240
Bug P36 P39 P46 P47 P2 P84 P18 P48 P35 P95 P42 P57 P96 P14
Core Assets 2 2 4 4 3 2 6 3 4 3 3 2 2 1 41
Hierarchy+3Tuple 2 1.5 3 3 2.5 1 1.5 3 4 3 3 1.5 0 1 30 73.2%
3Tuple 2 1.5 1 1 2 1 1.5 1 4 3 2.5 1 0 0 21.5 52.4%
None 2 2 0.5 0.5 3 1 1.5 1.5 3 1 1 1 0.5 0 18.5 45.1%
Table 11: Asset identification results using Gemini 2.5 Pro. Module sha256_wrapper aes0_wrapper aes0_wrapper aes0_wrapper dmi_jtag dmi_jtag csr_regfile reglk_wrapper reglk_wrapper rsa_wrapper acct_wrapper dma riscv_peripherals aes_192 Total Score Accuracy
CWE 1239 226 1258 1258 1245 1245 1262 1234 1232 226 276 1245 1310 1240
Bug P36 P39 P46 P47 P2 P84 P18 P48 P35 P95 P42 P57 P96 P14
Core Assets 2 2 4 4 3 2 6 3 4 3 3 2 2 1 41
Hierarchy+3Tuple 2 2 4 4 3 2 3 2.5 4 3 3 2 2 1 37.5 91.5%
3Tuple 1.5 1.5 2 2 2 1.5 2.5 2 4 2.5 3 1.5 1 1 28 68.3%
None 1 0 2.5 2.5 3 1 0 2.5 4 1 3 2 2 0 24.5 59.8%
Table 12: Asset identification results using Claude Sonnet 4.6. Module sha256_wrapper aes0_wrapper aes0_wrapper aes0_wrapper dmi_jtag dmi_jtag csr_regfile reglk_wrapper reglk_wrapper rsa_wrapper acct_wrapper dma riscv_peripherals aes_192 Total Score Accuracy
CWE 1239 226 1258 1258 1245 1245 1262 1234 1232 226 276 1245 1310 1240
Bug P36 P39 P46 P47 P2 P84 P18 P48 P35 P95 P42 P57 P96 P14
Core Assets 2 2 4 4 3 2 6 3 4 3 3 2 2 1 41
13
Hierarchy+3Tuple 2 2 4 4 3 2 4 3 4 3 3 2 1 1 38 92.7%
3Tuple 2 1 4 4 3 1 5 2 3.5 2.5 3 1.5 2 1 35.5 86.6%
None 2 1 4 4 3 1.5 3.5 2 3 1 3 1 2 1 32 78.0%