Pith. sign in

REVIEW 5 major objections 7 minor 36 references

CHARGE: Leveraging CWE Hierarchies for Hardware Security SystemVerilog Assertion Generation

T0 review · 5 major / 7 minor · reviewed 2026-08-01 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read The paper argues that guiding an LLM along the CWE hierarchy—decomposing each weakness into a target, action, and condition—lets generated hardware assertions catch 27 of 42 known bugs in open-source SoC designs, expose a previously unrepor

desk verdict CHARGE is a solid, well-executed step on LLM-generated security assertions, with a real methodological idea (CWE-hierarchy-guided asset identification), but its headline number is softer than it looks because the benchmark and the prompts come from the same group. read the letter →

arxiv 2607.27776 v1 pith:4PMA562N submitted 2026-07-30 cs.CR

Xiao Tan , Cynthia Sturton This is my paper
classification cs.CR
keywords hardwaresecurityCWESystemVerilogassertionsLLMRTLverificationassetidentificationassertiongenerationformal
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper tries to show that security assertions for hardware can be generated automatically from buggy, unverified RTL by using the Common Weakness Enumeration (CWE) hierarchy as a stand-in for a design specification. Its framework, CHARGE, decomposes each CWE into a (target, action, condition) triple, walks the LLM down the parent-child chain from the root to the target weakness, collects assets at each level, and then synthesizes SystemVerilog assertions from the inferred behaviors. On three open-source SoCs, the generated assertions detect 27 of 42 documented bugs; on one SoC, 89% of the assertions compile in a formal verification tool and 92.2% are non-vacuous. The method also surfaces a previously unknown bug and writes correct properties where the reference hand-written ones were wrong. If this holds, the most labor-intensive part of hardware security verification—deciding what to check—can be partially automated without a trusted specification.

What carries the argument

The central object is the CWE hierarchy itself, stored as a tree rooted at CWE-1000 (Research Concepts) with parent-child ('Child Of') edges, plus the framework's hand-authored per-CWE scaffolding: a (target, action, condition) 3-tuple, a policy question, and an SVA template. The tree is walked from root to target, and at each node the LLM is prompted to name assets that fit the tuple fields. Ancestor assets become 'relevant assets' for the target, which is the mechanism that lets an abstract weakness's security intent surface concrete signals in the RTL. The 3-tuple and template translate the natural-language CWE description into a machine-checkable temporal property.

What would settle it

A decisive experiment would hold the LLM and RTL fixed and vary only the prompt content: run CHARGE with the hierarchy path intact, with ancestor nodes removed, and with the 3-tuples and policy questions auto-generated from CWE text. If bug-detection and non-vacuity rates do not drop when the hierarchy is removed, the hierarchy is not the operative mechanism; if they drop when the tuples are auto-generated, the hand-written prompts carry the load rather than the CWE structure.

Watch

Extended reading notes

Core claim

The paper's central claim is that the hierarchical structure of CWE entries, not just the individual weakness descriptions, is what makes LLM-based assertion generation accurate. CHARGE traverses the CWE tree from the root down to the target weakness, asking the LLM at each node to identify candidate assets matching the tuple fields. Assets named under abstract ancestors become 'relevant assets' for the concrete target, so sensitive signals (such as an output register that must be zeroized on reset) can be identified even when the buggy RTL omits the expected behavior. From the collected assets, a per-CWE policy question and SVA template are used to synthesize assertions that encode the CWE'

Load-bearing premise

The framework assumes that each CWE's security intent is faithfully captured by a hand-written (target, action, condition) triple, a policy question, and an SVA template, and that the CWE-1000 parent-child chain makes ancestor assets relevant to the target weakness; if that abstraction is wrong for a CWE, the generated assertions encode the authors' interpretation rather than the weakness's meaning.

Editorial extensions

If this is right

  • Security assertions can be generated for unverified RTL without a trusted design specification, so property writing can begin before a full spec exists.
  • The framework can act as an independent check on manually written property sets; in this evaluation it produced correct properties where three reference properties were wrong.
  • Because new CWEs can be incorporated by inheriting ancestor 3-tuples, the method can scale as the CWE database grows without rewriting prompts for every entry.
  • Generated standard-SVA properties can be fed into any SVA-compatible formal verification tool, making the approach portable across verification flows.
  • The same generated assertions can flag bugs absent from the original bug list, as with the newly reported key-reset issue, extending the value of benchmark suites.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • Inference: hierarchy-guided asset identification likely transfers to software CWEs, where abstract ancestor concepts also name resources that a flat description would miss; the paper does not explore this direction.
  • Inference: the framework's accuracy depends on the hand-written tuples and policy questions, so an obvious next step is to generate or validate those automatically from CWE text, which would also separate the hierarchy's contribution from the prompt design.
  • Inference: because the measured hierarchy benefit differs across the LLMs tested, a finer-grained analysis of which ancestor levels add the most value could let future work prune or extend the traversal path.
  • Inference: the reported correction of three reference properties suggests benchmark suites themselves benefit from cross-checking with generated assertions, a use case the paper notes but does not develop.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

5 major / 7 minor

Summary. This paper presents CHARGE, an automated framework that maps MITRE CWE descriptions into hand-authored 3-tuples (target, action, condition), policy questions, and SVA templates, and uses three LLM prompts to identify security-critical assets from unverified RTL, infer expected behaviors, and emit SystemVerilog assertions. The proposed use of the hierarchy is to traverse CWE-1000 parent-child paths from a pillar down to the target CWE, collecting assets at ancestor nodes. The evaluation is on Hack@DAC 2018/2019/2021 designs with reference properties from the Verification Benchmarks repository: after excluding six of 48 benchmark bugs, CHARGE reports detecting 27 of 42 known bugs with GPT-4.1, with 89% of Hack@DAC21 SVAs compiling in JasperGold and 92.2% non-vacuous. The authors also report three corrections to manually written reference properties and one previously unreported key-reset bug in aes0_wrapper. Ablations across three LLMs show higher asset-identification scores with hierarchy+3-tuple than with 3-tuple only or neither, and higher end-to-end bug detection for CHARGE than a single-prompt baseline.

Significance. The paper has concrete, partially machine-checked strengths: JasperGold FPV is used to check compilability and violations; each CWE-module pair is run three times; three LLMs are evaluated; code is publicly available; and CHARGE finds three errors in existing manually written properties plus a previously unknown bug, which are useful falsifiable results. If the 27/42 detection rate is robust, the paper demonstrates a practical way to substitute CWE structure for design specifications in LLM-based security assertion generation, and it would be of interest to the hardware security and verification communities. However, the central claim that the CWE hierarchy itself improves assertion generation is not yet fully isolated: the end-to-end ablation removes the entire pipeline rather than only the hierarchy, the ground-truth benchmark overlaps with the authors, and the detection labels are assigned by the authors without a blinded protocol. These issues are addressable with additional experiments and disclosure, but they currently limit the certainty with which the central claim can be accepted.

major comments (5)
  1. [§6.1, Table 2; §6.2.2, Table 4; Ref. [25]] The ground truth for bug detection and for the 'core assets' scoring is the Verification Benchmarks repository (Ref. [25]), whose author list overlaps with this paper (Xiao Tan and Cynthia Sturton are co-authors of both). Because the hand-written CWE 3-tuples, policy questions, and SVA templates (Secs. 3.1, 4.2, 4.3) are also from the same group, the reported 27/42 and the Table 4 asset scores could reflect shared knowledge of the benchmark's expected signal names and conventions instead of a general property of CWE hierarchies. I am not claiming misconduct, but this is a correctness risk. Please disclose the overlap, archive the prompts before any benchmark iteration, evaluate on an externally maintained bug list or a benchmark developed by another group, and make the labeling protocol available. Independent annotation of at least the 42 detection calls is necessary.
  2. [§6.2.1, Tables 3-4] Baseline 0 removes the entire CHARGE pipeline (hierarchy, 3-tuple, policy question, SVA template, three-step prompting), so the end-to-end improvement in Table 3 does not isolate the hierarchical component. Baseline 1 isolates the hierarchy for asset identification, but it measures only name-overlap with the reference properties; it does not show that the hierarchy improves end-to-end bug detection. The conclusion that gains 'primarily arise from hierarchical reasoning and structured decomposition' is therefore stronger than the experiments support. Please add an ablation that keeps the 3-tuples/templates/policy questions fixed and varies only whether the ancestor-path hierarchy is included, and report bug detection for that variant; alternatively, soften the central claim.
  3. [§6 and §6.4.2, Table 2] The headline 27/42 depends on excluding six of the 48 repository bugs (four 'no violation found', one clock glitch, one hardcoded HMAC key). The exclusions may be justified, but the denominator is load-bearing. Please add a sensitivity table showing detection over the full 48 bugs, over 42, and over any subset that excludes cases judged to be benchmark errors; treat the four 'no violation found' cases both as missed detections and as unknown. Also, Sec. 6.4.2 reports two undetected cases as due to 'CWE Mismatch' in the Verification Benchmarks; if those are benchmark mislabels, they should be counted in the exclusion/sensitivity discussion. Without this, the reader cannot assess how robust 27/42 is.
  4. [§6.1] The labels in Table 2 — 'Asset', 'Behavior', and the final bug-detection call — are assigned by the authors through manual inspection of the RTL and the 'Bug Description' in the benchmark, with no documented inter-rater agreement, no blinding, and no release of the counterexample traces. JasperGold checks that an assertion is violated, but the attribution of that violation to a specific known bug is a human judgment. Please report a labeling protocol with at least two independent annotators (e.g., Cohen's kappa), and publish the counterexamples/traces used for each detection call so the 27/42 result is auditable.
  5. [§3.1, §3.3, §4.2, §4.3] The entire framework rests on the unvalidated assumption that each CWE's security intent is faithfully represented by a hand-authored 3-tuple, a policy question, and an SVA template, and that parent-child CWE paths make ancestor assets relevant. If an artifact misrepresents a CWE, the generated assertions encode the authors' interpretation rather than CWE semantics. The paper provides no independent validation of these artifacts or sensitivity to their wording. Please release all 64 prompt artifacts (or confirm they are on GitHub) and run a rewording sensitivity analysis, or state clearly that the evaluation validates the whole hand-authored prompt set, not the CWE-hierarchy abstraction alone.
minor comments (7)
  1. [§2.1] The section heading 'Assertioned Based Verification' should be 'Assertion-Based Verification'; Section 2.2 also contains the typo 'becasue'.
  2. [§3.3, Figure 1] Using the real CWE ID 'CWE-1999' for a 'hypothetical' child CWE is confusing, especially if that ID is already assigned by MITRE. Use an unassigned placeholder or clearly mark the example as fictional.
  3. [§6.1, Listing 2] The assertion syntax in Listing 2 (e.g., '|= >' spacing and bracket placement) should be normalized to standard SVA formatting for readability.
  4. [Table 1] The column title 'CWE covered' and the rows 'Convertible'/'Partially Convertible' would be clearer with explicit totals (64 covered, 46 not covered, 110 total).
  5. [Appendix Tables 7-9] The 'N/A' entries in the 'Unreachable' column should be explained (e.g., no compilable baseline assertions for acct_wrapper with GPT-4.1).
  6. [Abstract and §6.2.1] The abstract says '92.2% are non-vacuous' but Table 3 reports 'Unreachable' (7.8% for GPT-4.1). State explicitly how 'Unreachable' relates to non-vacuity and give the denominator counts.
  7. [§6.4.2] The final root-cause bullet, 'the expected behavior ... is not within the training data of the LLM,' is speculative. Label it as a conjecture or provide supporting prompt/output examples.

Circularity Check

2 steps flagged · score 6.0 of 10

Bug-to-CWE remapping in Sec 6.6 fits target CWEs to the ground-truth bug descriptions before 'predicting' those same bugs, and the asset-identification oracle is the authors' own Verification Benchmarks; JasperGold checks and three corrected properties keep the core method partly independent.

  1. fitted input called prediction [Section 6.6, 'Bug-to-CWE Mapping Algorithm leveraging CWE Hierarchy']
    "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 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."

    The target CWE is the primary input that drives asset identification, behavior mining, and SVA generation. For these seven benchmark bugs, that input is chosen by prompting an LLM with the very bug description and code snippet that CHARGE is later credited with handling. The CWE label is therefore fit to the ground-truth bug rather than selected independently, so any subsequent 'detection' of those bugs is partially forced by construction—the answer was used to choose the prompt. This is the fitted-input-called-prediction pattern.

  2. self citation load bearing [Section 6.1 (Table 2 'Asset' column) and Section 6.2.2 (Baseline 1); reference [25]]
    "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..."

    The oracle for the asset-identification claim is the 'manually written properties in Verification Benchmarks'—reference [25], authored by the same group (Rogers, ... Xiao Tan, ... Cynthia Sturton) that hand-authored CHARGE's CWE 3-tuples, policy questions, and SVA templates. The Baseline 1 score and the Table 2 'Asset' column are defined as overlap with those self-authored property bodies, so the hierarchy's measured benefit is recall against the same group's own interpretation rather than an independent standard. This makes a load-bearing part of the evaluation self-referential.

full rationale

CHARGE is an LLM pipeline rather than a formal derivation, so the circularity question is about the evaluation chain. The strongest independent evidence is that generated SVAs are run in Cadence JasperGold FPV against the buggy Hack@DAC designs, and CHARGE contradicts the benchmark by correcting three reference properties and finding an undocumented bug—outcomes that would not occur if the pipeline merely reproduced the benchmark. However, two evaluation steps reduce to the paper's own inputs. First, Section 6.6 selects target CWEs for seven bugs by prompting the LLM with the ground-truth bug description and code snippet; those CWEs then drive the same pipeline whose outputs are counted as successes, so those detections are fitted predictions. Second, the asset-identification metric (Table 2 'Asset' column and Baseline 1 scores) defines success as overlap with the assets in the manually written Verification Benchmarks property bodies [25], a repository authored by the same group that hand-wrote CHARGE's CWE 3-tuples, policy questions, and templates. This measures agreement with the authors' own interpretation rather than an independent oracle. The four 'no violation found' exclusions and the hardcoded-HMAC exclusion further adjust the denominator. Together these make the headline 27/42 and the claim that hierarchy improves asset identification partially self-referential, though the JasperGold checks and three corrected properties keep the core method from being entirely circular.

Assumptions & free parameters 1 free parameters · 4 assumptions · 0 invented entities

CHARGE introduces no new physical or mathematical entities; its input-side scaffolding (3-tuples, policy questions, SVA templates, hierarchy JSON) is hand-built by the authors and reused, which is the main source of hand-chosen 'parameters'. The CWE hierarchy itself is external (MITRE), but the framework's interpretation of it is not independently benchmarked.

free parameters (1)
  • CWE 3-tuple / policy-question / SVA-template wording
    Hand-authored once per CWE and reused verbatim; these prompt strings directly determine every generated asset, behavior, and assertion, but are not separately validated against an independent oracle.
assumptions (4)
  • domain assumption CWE-1000 hierarchy parent-child edges encode semantic refinement, and assets relevant to an ancestor CWE remain relevant to descendant target CWEs.
    Stated in Sec 3.3 and used in Step 1 (Sec 4.1); the paper provides motivating examples but no general proof or independent audit of transferability.
  • ad hoc to paper A target CWE's security policy can be represented by a hand-authored 3-tuple plus policy question plus SVA template.
    The tuple/question/template are created by the authors (Secs 3.1, 4.2, 4.3) and are not derived from the CWE database itself.
  • domain assumption The Verification Benchmarks repository's manually written properties and bug-to-CWE assignments can serve as an evaluation oracle.
    Used as ground truth throughout Sec 6; [25] includes the current authors, and some of its properties are shown by this paper to be incorrect.
  • domain assumption LLM-generated expected behaviors, prompted to ignore the buggy RTL's behavior, are an acceptable proxy for the CWE's security intent.
    Sec 4.2 relies on this; Sec 6.4.3 shows cases where the buggy RTL still misleads the LLM.

how reviews work

0 comments
Cite this review

Pith. "Pith review of CHARGE: Leveraging CWE Hierarchies for Hardware Security SystemVerilog Assertion Generation." pith.science (2026). https://pith.science/paper/4PMA562N

@misc{pith2026260727776,
  author       = {Pith},
  title        = {Pith review of: CHARGE: Leveraging CWE Hierarchies for Hardware Security SystemVerilog Assertion Generation},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/4PMA562N}},
  note         = {Machine review of arXiv:2607.27776}
}
read the original 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.

Figures

Figures reproduced from arXiv: 2607.27776 by the authors.

Figure 1
Figure 1. Explanation of CHARGE’s Usage of CWE Hierarchies [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 1
Figure 1. Here the target CWE is CWE-226 "Sensitive Information [PITH_FULL_IMAGE:figures/full_fig_p005_1.png] view at source ↗
Figure 2
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 represen… view at source ↗

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

36 extracted references · 7 linked inside Pith

  1. [25]

    Jayden Rogers, Niyaz Shakeel, Xiao Tan, Samantha Espinosa, Divya Mankani, Cade Chabra, Kaki Ryan, and Cynthia Sturton. 2025. Hardware Security Bench- marks for Open-Source SystemVerilog Designs. InProceedings of the Secure Devel- opment Conference (SecDev). IEEE. https://github.com/HWSec-UNC/verification- benchmarks

    2025

  2. [1]

    Fung, Jonathan Valamehr, Mohammad Bidmeshki, Piotr Sapiecha, Steve Brown, Krish- nendu Chakrabarty, Ramesh Karri, and Benjamin Tan

    Baleegh Ahmad, Wei-Kai Liu, Luca Collini, Hammond Pearce, Jason M. Fung, Jonathan Valamehr, Mohammad Bidmeshki, Piotr Sapiecha, Steve Brown, Krish- nendu Chakrabarty, Ramesh Karri, and Benjamin Tan. 2022. Don’t CWEAT It: Toward CWE Analysis Techniques in Early Stages of Hardware Design. InPro- ceedings of the 41st IEEE/ACM International Conference on Comp...

    arXiv 2022

  3. [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

    arXiv 2025

  4. [3]

    Dinesh Reddy Ankireddy, Sudipta Paria, Aritra Dasgupta, Sandip Ray, and Swarup Bhunia. 2025. LASSO: LLM-Aided Security Property Generation for Assertion- based SoC Verification. In2025 ACM/IEEE 7th Symposium on Machine Learning for CAD (MLCAD). 1–10. doi:10.1109/MLCAD65511.2025.11189178

    arXiv 2025

  5. [4]

    Fung, Ahmad-Reza Sadeghi, and Jeyavijayan Rajendran

    Ghada Dessouky, David Gens, Patrick Haney, Garrett Persyn, Arun Kanuparthi, Hareesh Khattri, Jason M. Fung, Ahmad-Reza Sadeghi, and Jeyavijayan Rajendran

  6. [5]

    Calvin Deutschbein, Andres Meza, Francesco Restuccia, Ryan Kastner, and Cyn- thia Sturton. 2021. Isadora: Automated Information Flow Property Generation for Hardware Designs. InProceedings 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, ...

    arXiv 2021

  7. [6]

    Calvin Deutschbein and Cynthia Sturton. 2020. Evaluating Security Specifica- tion Mining for a CISC Architecture. In2020 IEEE International Symposium on Hardware Oriented Security and Trust (HOST). 164–175. doi:10.1109/HOST45689. 2020.9300291

    arXiv 2020

  8. [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

    arXiv 2026

Show all 36 references
  1. [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

    2025 arXiv

  2. [9]

    Hack@DAC 2018 Phase 2 Buggy SoC. [n. d.]. https://github.com/hackdac/ hackdac_2018_beta

    2018

  3. [10]

    Hack@DAC 2019 Alpha Stage SoC. [n. d.]. https://github.com/HACK-EVENT/ hackatdac19

    2019

  4. [11]

    Hack@DAC 2021 SoC. [n. d.]. https://github.com/HACK-EVENT/hackatdac21

    2021

  5. [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 System- on-Chip (SoC) Verification. arXiv:2601.02624 [cs.CR] https:/...

    2026 arXiv

  6. [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

    2024

  7. [14]

    Ryan Kastner, Francesco Restuccia, Andres Meza, Sayak Ray, Jason Fung, and Cynthia Sturton. 2022. Automating hardware security property generation: invited. InProceedings of the 59th ACM/IEEE Design Automation Conference(San Francisco, California)(DAC ’22). Association for Com...

    2022

  8. [15]

    Kevin Laeufer, Jack Koenig, Donggyu Kim, Jonathan Bachrach, and Koushik Sen

  9. [16]

    Bhabesh Mali, Karthik Maddala, Vatsal Gupta, Sweeya Reddy, Chandan Karfa, and Ramesh Karri. 2024. ChIRAAG: ChatGPT Informed Rapid and Automated Assertion Generation. In2024 IEEE Computer Society Annual Symposium on VLSI (ISVLSI). 680–683. doi:10.1109/ISVLSI61997.2024.00130

    2024

  10. [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

    2023 arXiv

  11. [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 Verifica- tion: A Novel SystemVerilog Assertion Dataset.ACM Tr...

    2025 doi

  12. [19]

    Samit Shahnawaz Miftah, Amisha Srivastava, Hyunmin Kim, Shiyi Wei, and Kanad Basu. 2025. SymbFuzz: Symbolic Execution Guided Hardware Fuzzing. InProceedings of the IEEE/ACM International Symposium on Microarchitecture (MICRO). Association for Computing Machinery, New York, NY,...

    2025

  13. [20]

    MITRE. [n. d.]. Common Weakness Enumeration. https://cwe.mitre.org/

  14. [21]

    Sujit Kumar Muduli, Gourav Takhar, and Pramod Subramanyan. 2020. Hyper- Fuzzing for SoC Security Validation. In2020 IEEE/ACM International Conference On Computer Aided Design (ICCAD). 1–9

    2020

  15. [22]

    Shengyi Pan, Lingfeng Bao, Xin Xia, David Lo, and Shanping Li. 2023. Fine- grained Commit-level Vulnerability Type Prediction by CWE Tree Structure. In2023 IEEE/ACM 45th International Conference on Software Engineering (ICSE). 957–969. doi:10.1109/ICSE48619.2023.00088

    2023

  16. [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

    2023 arXiv

  17. [24]

    Restuccia, A

    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]

    2021 arXiv

  18. [26]

    Kaki Ryan and Cynthia Sturton. 2023. Sylvia: Countering the Path Explosion Problem in the Symbolic Execution of Hardware Designs. InProceedings of the 23rd Conference on Formal Methods in Computer-Aided Design (FMCAD). TU Wien Academic Press, New York, NY, USA, 110–121. https:...

    2023

  19. [27]

    Kaki Ryan and Cynthia Sturton. 2025. SylQ-SV: Scaling Symbolic Execution of Hardware Designs with Query Caching. InProceedings of the International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS). ACM

    2025

  20. [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 Communica- tion Protocols. arXiv:2504.17226 [cs.AR] https://arxiv.org/abs/2504.17226

    2025 arXiv

  21. [29]

    SymbiYosys (sby). [n. d.]. Front-end for Yosys-based formal verification flows. https://github.com/YosysHQ/sby?tab=readme-ov-file

  22. [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

    2026

  23. [31]

    Shams Tarek, Dipayan Saha, Sujan Kumar Saha, Mark Tehranipoor, and Farimah Farahmandi. 2024. SoCureLLM: An LLM-driven Approach for Large-Scale System- on-Chip Security Verification and Policy Generation. Cryptology ePrint Archive, Paper 2024/983. https://eprint.iacr.org/2024/983

    2024

  24. [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. InProceedings of the Conference on Design, Automation and Test in Europe (DATE). European Design ...

    2010

  25. [33]

    Zhang and C

    R. Zhang and C. Sturton. 2020. Transys: Leveraging Common Security Properties Across Hardware Designs. InIEEE S&P. IEEE

    2020

  26. [34]

    Rui Zhang and Cynthia Sturton. 2020. Transys: Leveraging Common Security Properties Across Hardware Designs. In2020 IEEE Symposium on Security and Privacy (SP). 1713–1727. doi:10.1109/SP40000.2020.00030 Appendix 11 Table 7: Baseline 0 vs. CHARGE using GPT-4.1. Module CWE Bug D...

    2020

  27. [2018]

    RFUZZ: Coverage-Directed Fuzz Testing of RTL on FPGAs. InICAAD. 1–8. doi:10.1145/3240765.3240842

  28. [2019]

    InProceedings of the 28th USENIX Conference on Security Symposium(Santa Clara, CA, USA) (SEC’19)

    Hardfails: insights into software-exploitable hardware bugs. InProceedings of the 28th USENIX Conference on Security Symposium(Santa Clara, CA, USA) (SEC’19). USENIX Association, USA, 213–230

Pith tools

Reviewed August 1, 2026 · model on record in the stance chip above.