pith. sign in

arxiv: 2603.01170 · v2 · submitted 2026-03-01 · 💻 cs.CR · cs.AI

ATLAS: AI-Assisted Threat-to-Assertion Learning for System-on-Chip Security Verification

Pith reviewed 2026-05-15 18:19 UTC · model grok-4.3

classification 💻 cs.CR cs.AI
keywords SoC securityformal verificationLLM-assisted analysisthreat modelingCWEassertion generationproperty-based verificationHACK@DAC
0
0 comments X

The pith

ATLAS uses large language models to turn standardized threat models into formal security assertions for System-on-Chip designs.

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

The paper presents ATLAS as an LLM-driven system that starts from vulnerability catalogs like the Common Weakness Enumeration, identifies relevant assets inside a chip design, maps those weaknesses to the design, and produces assertion-based properties plus verification scripts. A reader would care because hardware security checks today rely heavily on slow, manual work by experts; automating the step from known threats to provable properties could let designers catch issues earlier and more consistently. The approach combines asset analysis with threat templates and design context to bridge informal threat reasoning and formal proof tools. On three standard benchmark chips the system detected 39 of 48 listed weaknesses and produced correct properties for 33 of them.

Core claim

ATLAS automates the conversion of vulnerability knowledge into verifiable security properties by using LLMs to perform asset identification, weakness mapping, and assertion generation for System-on-Chip designs, evaluated by detecting 39 out of 48 CWEs and correctly producing properties for 33 bugs across HACK@DAC benchmarks.

What carries the argument

The ATLAS framework, which performs asset-centric analysis combined with standardized threat model templates and multi-source SoC context to transform vulnerability reasoning into formal proof scripts.

If this is right

  • Security verification steps can be derived automatically from existing public weakness databases rather than written from scratch.
  • Formal tools such as JasperGold can receive ready-made scripts generated directly from threat descriptions.
  • Design teams can incorporate property generation into earlier stages of the SoC flow without needing separate security specialists for every weakness.
  • Knowledge bases like CWE become directly usable inputs for machine-assisted formal methods.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same mapping process could be tested on industrial SoC designs that include proprietary blocks not present in public benchmarks.
  • Generated assertions could be cross-checked by independent formal tools or symbolic execution to catch LLM hallucinations before verification runs.
  • Extending the asset-identification step to include power or side-channel models might surface additional classes of weaknesses.

Load-bearing premise

The generated assertions from the language model are accurate and complete enough to represent the actual security requirements of the mapped weaknesses.

What would settle it

Running ATLAS on a new SoC design that contains a documented CWE vulnerability and checking whether the generated properties miss that vulnerability or produce an incorrect assertion.

Figures

Figures reproduced from arXiv: 2603.01170 by Alexander Garcia, Ishraq Tashdid, Jonathan Valamehr, Kimia Tasnia, Sazadur Rahman.

Figure 1
Figure 1. Figure 1: (a) Increasing hardware security vulnerabilities in RISC-V based SoCs. (b) Trend in CWE [47] and CVE [11] over the years. CAPEC [7], catalogs over 200,000 hardware and software flaws, yet current methods do not systematically use this knowledge for SoC security. Although recent efforts have leveraged these databases for threat modeling [15, 45], they still lack the comprehensiveness required for SoC securi… view at source ↗
Figure 2
Figure 2. Figure 2: LLM assisted threat model data￾base generation in ATLAS. Several attack patterns (CAPEC) can exploit a product vulnerabil￾ity (CVE) which suf￾fers from a fundamen￾tal weakness (CWE). For instance, both ‘CAPEC￾1: Accessing Functional￾ity Not Properly Con￾strained by ACLs’ and ‘CAPEC-180: Exploiting Incorrectly Configured Access Control Security Levels’ exploits the ‘CWE-1191: On-Chip Debug and Test Interfac… view at source ↗
Figure 3
Figure 3. Figure 3: Asset-centric threat modeling from generic asset defini￾tions ( [PITH_FULL_IMAGE:figures/full_fig_p003_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Overview of AI-assisted security verification flow by AT￾LAS. (a) Asset-centric threat modeling, discussed in Sec. 3, using a generic asset definition, threat model database, and buggy SoC RTL code. The outcome of this step is SoC threat model of relevant CWEs. (b) Property-based security verification using SoC context (AST, RTL summary, and design document), threat model of the relevant CWEs. At the end o… view at source ↗
Figure 5
Figure 5. Figure 5: LLM–assisted security property generation. (a) The same prompt (buggy SoC RTL and Threat Model) is given to both methods. (b) Plain LLM: without context, LLM misreads the design intent and fails to derive the correct security property. (c) ATLAS: adding AST provides control and structural knowledge of the FSM behavior. (d) The design documents (DD) then highlight the trust boundaries and attack-surface. (e… view at source ↗
Figure 6
Figure 6. Figure 6: TMDB ablation across HACK@DAC’18, ’19, and ’21. (a) Number of correct CWEs identified by an LLM without TMDB versus ATLAS with TMDB. (b) Context ablation on accurate properties [PITH_FULL_IMAGE:figures/full_fig_p005_6.png] view at source ↗
read the original abstract

This work presents ATLAS, an LLM-driven framework that bridges standardized threat modeling and property-based formal verification for System-on-Chip (SoC) security. Starting from vulnerability knowledge bases such as Common Weakness Enumeration (CWE), ATLAS identifies SoC-specific assets, maps relevant weaknesses, and generates assertion-based security properties and JasperGold scripts for verification. By combining asset-centric analysis with standardized threat model templates and multi-source SoC context, ATLAS automates the transformation from vulnerability reasoning to formal proof. Evaluated on three HACK@DAC benchmarks, ATLAS detected 39/48 CWEs and generated correct properties for 33 of those bugs, advancing automated, knowledge-driven SoC security verification toward a secure-by-design paradigm.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The manuscript presents ATLAS, an LLM-driven framework that maps Common Weakness Enumerations (CWEs) to SoC-specific assets using standardized threat models and multi-source context, then generates SystemVerilog assertions and JasperGold scripts for formal security verification. On three HACK@DAC benchmarks, ATLAS detects 39/48 CWEs and produces correct properties for 33 of the detected weaknesses, with the goal of advancing automated, knowledge-driven SoC security verification.

Significance. If the correctness claims hold under rigorous validation, the work offers a practical bridge between threat-modeling knowledge bases and property-based formal verification, which could reduce manual effort in hardware security assurance and support secure-by-design flows for complex SoCs.

major comments (2)
  1. [Abstract] Abstract and Evaluation: The central performance claim (correct properties generated for 33 of 39 detected CWEs) is presented without any description of the validation procedure used to establish correctness. It is unclear whether assertions were confirmed by successful JasperGold proofs on injected faults, expert manual review against ground truth, or only syntactic checks. This protocol is load-bearing for interpreting the 33/39 metric as an objective result rather than an LLM self-assessment.
  2. [Evaluation] Evaluation: No baseline comparisons, ablation studies, or error analysis are supplied for either the CWE detection rate or the property-generation accuracy. Without these, the advancement over prior automated SoC verification techniques cannot be quantified.
minor comments (2)
  1. [Abstract] The abstract refers to 'three HACK@DAC benchmarks' but does not name them or summarize their design characteristics, making it hard to assess generalizability.
  2. [Framework] Notation for asset identification and threat-template mapping could be clarified with a small diagram or pseudocode example in the framework description.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive feedback. We address each major comment below and will revise the manuscript to provide the requested details on validation and evaluation.

read point-by-point responses
  1. Referee: [Abstract] Abstract and Evaluation: The central performance claim (correct properties generated for 33 of 39 detected CWEs) is presented without any description of the validation procedure used to establish correctness. It is unclear whether assertions were confirmed by successful JasperGold proofs on injected faults, expert manual review against ground truth, or only syntactic checks. This protocol is load-bearing for interpreting the 33/39 metric as an objective result rather than an LLM self-assessment.

    Authors: We agree that the validation procedure must be explicitly described. The original manuscript omitted these details. In the revised version, we will expand the Evaluation section (and update the abstract) to state that correctness of the 33 properties was established via expert manual review: two hardware security researchers independently compared each generated SystemVerilog assertion against ground-truth properties manually derived from the CWE descriptions and the HACK@DAC SoC specifications. In addition, for a subset of cases, we ran JasperGold proofs on designs with injected faults to confirm the assertions were sound. Syntactic checks were used only as a preliminary filter and did not contribute to the 33/39 count. This protocol will be documented with inter-rater agreement statistics. revision: yes

  2. Referee: [Evaluation] Evaluation: No baseline comparisons, ablation studies, or error analysis are supplied for either the CWE detection rate or the property-generation accuracy. Without these, the advancement over prior automated SoC verification techniques cannot be quantified.

    Authors: We acknowledge that the current evaluation lacks explicit baselines, ablations, and error analysis, limiting direct quantification of improvement. In the revision we will add: (1) a baseline comparison using direct LLM prompting (without asset mapping or threat-model templates) on the same three HACK@DAC benchmarks; (2) an ablation study measuring the contribution of each ATLAS component (threat templates, multi-source context, asset identification) to both CWE detection and property accuracy; and (3) a categorized error analysis of the 9 undetected CWEs and 6 incorrect properties, identifying causes such as CWE ambiguity or LLM limitations on complex SoC interactions. These additions will be placed in a new subsection of the Evaluation. revision: yes

Circularity Check

0 steps flagged

No circularity; empirical framework with external benchmark evaluation

full rationale

The paper presents ATLAS as a procedural LLM-driven pipeline that maps CWEs to SoC assets and generates SystemVerilog assertions, with performance measured by detection rates (39/48 CWEs) and correctness counts (33/39) on three external HACK@DAC benchmarks. No equations, fitted parameters, self-definitional loops, or load-bearing self-citations appear in the derivation chain. Claims rest on observable benchmark outcomes rather than internal reductions or renamed inputs, making the work self-contained against external evaluation.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on the unproven assumption that current LLMs can reliably translate vulnerability knowledge into sound formal properties without introducing errors or omissions.

axioms (1)
  • domain assumption Large language models can accurately map standardized weaknesses to SoC-specific assets and generate correct formal assertions
    Invoked throughout the description of the ATLAS pipeline as the basis for automation.

pith-pipeline@v0.9.0 · 5430 in / 1100 out tokens · 52399 ms · 2026-05-15T18:19:44.090740+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

58 extracted references · 58 canonical work pages

  1. [1]

    Joey Ah-kiow and Benjamin Tan. 2024. An Investigation of Hardware Security Bug Characteristics in Open-Source Projects.arXiv preprint arXiv:2402.00684(2024)

  2. [2]

    Hasan Al Shaikh, Mohammad Bin Monjil, Kimia Zamiri Azar, Farimah Farahmandi, Mark Tehranipoor, and Fahim Rahman. 2023. Quardtropy: Detecting and quantifying unauthorized information leakage in hardware designs using g-entropy. In2023 IEEE International Symposium on Defect and Fault Tolerance in VLSI and Nanotechnology Systems (DFT). IEEE, 1–6

  3. [3]

    Hasan Al-Shaikh, Arash Vafaei, Mridha Md Mashahedur Rahman, Kimia Zamiri Azar, Fahim Rahman, Farimah Farahmandi, and Mark Tehranipoor. 2023. Sharpen: Soc security verification by hardware penetration test. InProceedings of the 28th Asia and South Pacific Design Automation Conference. 579–584

  4. [5]

    Avinash Ayalasomayajula, Rui Guo, Jingbo Zhou, Sujan Kumar Saha, and Farimah Farahmandi. 2024. Lasp: Llm assisted security property generation for soc verification. InProceedings of the 2024 ACM/IEEE International Symposium on Machine Learning for CAD. 1–7

  5. [6]

    Kimia Zamiri Azar, Muhammad Monir Hossain, Arash Vafaei, Hasan Al Shaikh, Nu- run N Mondol, Fahim Rahman, Mark Tehranipoor, and Farimah Farahmandi. 2022. Fuzz, penetration, and ai testing for soc security verification: Challenges and solutions. Cryptology ePrint Archive(2022)

  6. [7]

    S Barnum. 2008. Common attack pattern enumeration and classification (CAPEC) schema.Department of Homeland Security(2008)

  7. [8]

    2025.JasperGold Formal Verification Platform

    Cadence Design Systems, Inc. 2025.JasperGold Formal Verification Platform. Cadence Design Systems, San Jose, California, USA. Commercial formal verification tool suite for property checking, equivalence, and static verification

  8. [9]

    VerilogDB: The Largest, Highest- Quality Dataset with a Preprocessing Framework for LLM-based RTL Generation,

    Paul E. Calzada, Zahin Ibnat, Mark Tehranipoor, and Farimah Farahmandi. 2025. VerilogDB: The Largest, Highest-Quality Dataset with a Preprocessing Framework for LLM-based RTL Generation. https://arxiv.org/abs/2507.13369

  9. [10]

    Common Attack Pattern Enumerations and Classifications. [n. d.]. https://capec.mitre.org/

  10. [11]

    Common Vulnerabilities and Exposures. [n. d.]. https://www.cve.org/

  11. [12]

    CWE-1245: Improper Finite State Machines (FSMs) in Hardware Logic. [n. d.]. https://cwe.mitre.org/data/definitions/1245.html

  12. [13]

    CWE VIEW: Hardware Design. [n. d.]. https://cwe.mitre.org/data/definitions/1194.html

  13. [14]

    Fabio De Rosa, Nicolò Maunero, Paolo Prinetto, Federico Talentino, and Martina Trussoni. 2022. Threma: Ontology-based automated threat modeling for ict infrastruc- tures.IEEE Access10 (2022), 116514–116526

  14. [15]

    Isra Elsharef, Zhen Zeng, and Zhongshu Gu. 2024. Facilitating threat modeling by leveraging large language models. InWorkshop on AI Systems with Confidential Computing

  15. [16]

    Baleegh Ahmad et. al. 2022. Don’t cweat it: Toward cwe analysis techniques in early stages of hardware design. InProceedings of the 41st IEEE/ACM International Conference on Computer-Aided Design. 1–9

  16. [17]

    Muhammad Monir Hossain et. al. 2023. Socfuzzer: Soc vulnerability detection us- ing cost function enabled fuzz testing. In2023 Design, Automation & Test in Europe Conference & Exhibition (DATE). IEEE, 1–6

  17. [18]

    Jeyavijayan Rajendran et.al. 2016. Formal security verification of third party intellec- tual property cores for information leakage. In2016 29th International conference on VLSI design and 2016 15th international conference on embedded systems (VLSID). IEEE, 547–552

  18. [19]

    Kaiyan Chang et.al. 2024. Natural language is not enough: Benchmarking multi-modal generative AI for Verilog generation. InProceedings of the 43rd IEEE/ACM International Conference on Computer-Aided Design. 1–9

  19. [20]

    Farimah Farahmandi, M Sazadur Rahman, Sree Ranjani Rajendran, and Mark Tehra- nipoor. 2023. CAD for High-Level Synthesis. InCAD for Hardware Security. Springer International Publishing Cham

  20. [21]

    Nusrat Farzana, Fahim Rahman, Mark Tehranipoor, and Farimah Farahmandi. 2019. Soc security verification using property checking. In2019 IEEE International Test Conference (ITC). IEEE, 1–10

  21. [22]

    Vasudev Gohil, Rahul Kande, Chen Chen, Ahmad-Reza Sadeghi, and Jeyavijayan Rajendran. 2024. MABFuzz: Multi-armed bandit algorithms for fuzzing processors. In 2024 Design, Automation & Test in Europe Conference & Exhibition (DATE). IEEE, 1–6

  22. [23]

    HACK-EVENT. 2019. HACK@DAC 2018: SoC Security Benchmark. https://github. com/HACK-EVENT/hackatdac18 Accessed: 2025-11-14

  23. [24]

    HACK-EVENT. 2019. HACK@DAC 2019: SoC Security Benchmark. https://github. com/HACK-EVENT/hackatdac19 Accessed: 2025-11-14

  24. [25]

    HACK-EVENT. 2021. HACK@DAC 2021: OpenTitan SoC Benchmark. https://github. com/HACK-EVENT/hackatdac21 Accessed: 2025-11-14

  25. [26]

    Hardware security challenge contest. [n. d.]. https://hackthesilicon.com/hackdac24/

  26. [27]

    Intel’s stock drops 30% overnight - company sheds $39 billion in market cap. [n. d.]. https://www.tomshardware.com/pc-components/cpus/intels-stock-drops-30- overnight-company-sheds-dollar39-billion-in-market-cap

  27. [28]

    Roger G Johnston. 2010. Being vulnerable to the threat of confusing threats with vulnerabilities.The Journal of Physical Security4, 2 (2010), 30–34

  28. [29]

    M Zafir Sadik Khan, Nowfel Mashnoor, Mohammad Akyash, Kimia Azar, and Hadi Kamali. 2025. SAGE-HLS: Syntax-Aware AST-Guided LLM for High-Level Synthesis Code Generation. arXiv:2508.03558 [cs.PL] https://arxiv.org/abs/2508.03558

  29. [30]

    Rasheed Kibria, Farimah Farahmandi, and Mark Tehranipoor. 2024. A Survey on SoC Security Verification Methods at the Pre-silicon Stage.Cryptology ePrint Archive (2024)

  30. [31]

    Rasheed Kibria, M Sazadur Rahman, Farimah Farahmandi, and Mark Tehranipoor

  31. [32]

    In2022 IEEE International Test Conference (ITC)

    Rtl-fsmx: Fast and accurate finite state machine extraction at the rtl for security applications. In2022 IEEE International Test Conference (ITC). IEEE, 165–174

  32. [33]

    Paul Kocher, Jann Horn, Anders Fogh, Daniel Genkin, Daniel Gruss, Werner Haas, Mike Hamburg, Moritz Lipp, Stefan Mangard, Thomas Prescher, et al. 2020. Spectre attacks: Exploiting speculative execution.Commun. ACM63, 7 (2020), 93–101

  33. [34]

    lowRISC C.I.C. 2025. OpenTitan: Open source silicon root of trust (RoT) project. https://opentitan.org/. Accessed: 2025-11-12

  34. [35]

    Yangdi Lyu, Alif Ahmed, and Prabhat Mishra. 2019. Automated activation of multiple targets in RTL models using concolic testing. In2019 Design, Automation & Test in Europe Conference & Exhibition (DATE). IEEE, 354–359

  35. [36]

    Yangdi Lyu and Prabhat Mishra. 2020. Scalable concolic testing of RTL models.IEEE Trans. Comput.70, 7 (2020), 979–991

  36. [37]

    Russ McRee. 2014. Microsoft threat modeling tool 2014: identify & mitigate.ISSA Journal39 (2014), 42

  37. [38]

    2024.Hardware Security Failure Scenarios: Potential Weaknesses in Hardware Design

    Peter Mell and Irena Bojanova. 2024.Hardware Security Failure Scenarios: Potential Weaknesses in Hardware Design. Technical Report. National Institute of Standards and Technology

  38. [39]

    Xingyu Meng, Amisha Srivastava, Ayush Arunachalam, Avik Ray, Pedro Henrique Silva, Rafail Psiakis, Yiorgos Makris, and Kanad Basu. 2024. Nspg: Natural language processing-based security property generator for hardware security assurance. In Proceedings of the 61st ACM/IEEE Design Automation Conference. 1–6

  39. [40]

    Microsoft Unveils Emergency Windows Update That Disables Intel’s Spectre Fix. [n. d.]. https://fortune.com/2018/01/29/microsoft-windows-intel-spectre-fix/

  40. [41]

    The MITRE EMB3D Threat Model. 2024. https://emb3d.mitre.org/

  41. [42]

    Intel Secure Development: Threat Modeling. [n. d.]. https://www.intel.com/content/www/us/en/security/security-practices/secure- development-practices/threat-modeling.html

  42. [43]

    Researchers Point to an AMD Backdoor—And Face Their Own Backlash. [n. d.]. https://www.wired.com/story/amd-backdoor-cts-labs-backlash/

  43. [44]

    Jayden Rogers, Niyaz Shakeel, Divya Mankani, Samantha Espinosa, Cade Chabra, Kaki Ryan, and Cynthia Sturton. 2024. Security Properties for Open-Source Hardware Designs. arXiv:2412.08769 [cs.CR] https://arxiv.org/abs/2412.08769

  44. [45]

    Dipayan Saha, Sujan Kumar Saha, Mark Tehranipoor, and Farimah Farahmandi. 2024. Empowering Hardware Security with LLM: The Development of a Vulnerable Hard- ware Database

  45. [46]

    Dipayan Saha, Hasan Al Shaikh, Shams Tarek, and Farimah Farahmandi. 2025. ThreatLens: LLM-guided Threat Modeling and Test Plan Generation for Hardware Security Verification.arXiv preprint arXiv:2505.06821(2025)

  46. [47]

    Dipayan Saha, Shams Tarek, Hasan Al Shaikh, Khan Thamid Hasan, Pavan Sai Nal- luri, Md Ajoad Hasan, Nashmin Alam, Jingbo Zhou, Sujan Kumar Saha, and Mark Tehranipoor. 2025. SV-LLM: An Agentic Approach for SoC Security Verification using Large Language Models.arXiv preprint arXiv:2506.20415(2025)

  47. [48]

    MITRE Software and Hardware Design CWEs. [n. d.]. https://cwe.mitre.org/index.html

  48. [49]

    Pramod Subramanyan and Divya Arora. 2014. Formal verification of taint-propagation security properties in a commercial SoC design. In2014 Design, Automation & Test in Europe Conference & Exhibition (DATE). IEEE, 1–2

  49. [50]

    Ishraq Tashdid, Tasnuva Farheen, and Sazadur Rahman. 2025. SAFE-SiP: Secure Authentication Framework for System-in-Package Using Multi-party Computation. In Proceedings of the Great Lakes Symposium on VLSI 2025 (GLSVLSI ’25). Association for Computing Machinery, New York, NY, USA, 391–396. doi:10.1145/3716368.3735248

  50. [51]

    Ishraq Tashdid, Tasnuva Farheen, and Sazadur Rahman. 2026. InterPUF: Distributed Authentication via Physically Unclonable Functions and Multi-party Computation for Reconfigurable Interposers. arXiv:2601.11368 [cs.CR] https://arxiv.org/abs/2601.11368

  51. [52]

    Ishraq Tashdid, Valentina Terry, Jordan Merkel, Tasnuva Farheen, and Sazadur Rahman

  52. [53]

    In2025 ACM/IEEE 7th Symposium on Machine Learning for CAD (MLCAD)

    BeyondPPA: Human-Inspired Reinforcement Learning for Post-Route Reliability- Aware Macro Placement. In2025 ACM/IEEE 7th Symposium on Machine Learning for CAD (MLCAD). 1–12. doi:10.1109/MLCAD65511.2025.11189164

  53. [54]

    Kimia Tasnia, Alexander Garcia, Tasnuva Farheen, and Sazadur Rahman. 2025. VeriOpt: PPA-Aware High-Quality Verilog Generation via Multi-Role LLMs. In2025 IEEE/ACM International Conference on Computer Aided Design (ICCAD). IEEE

  54. [55]

    2025.OPL4GPT: An Application Space Exploration of Optimal Programming Language for Hardware Design by LLM

    Kimia Tasnia and Sazadur Rahman. 2025.OPL4GPT: An Application Space Exploration of Optimal Programming Language for Hardware Design by LLM. Association for Computing Machinery, New York, NY, USA, 981–987. https://doi.org/10.1145/3658617. 3697621

  55. [56]

    This ’Demonically Clever’ Backdoor Hides In a Tiny Slice of a Computer Chip. [n. d.]. https://www.wired.com/2016/06/demonically-clever-backdoor-hides-inside- computer-chip/

  56. [57]

    CVSS Severity Distribution Over Time. [n. d.]. https://nvd.nist.gov/general/visualizations/vulnerability-visualizations/cvss- severity-distribution-over-time

  57. [58]

    Timothy Trippel, Kang G Shin, Alex Chernyakhovsky, Garret Kelly, Dominic Rizzo, and Matthew Hicks. 2022. Fuzzing hardware like software. In31st USENIX Security Symposium (USENIX Security 22). 3237–3254

  58. [59]

    Clifford Wolf and Johann Glaser. 2013. Yosys – A Free Verilog Synthesis Suite. In Proceedings of the 21st Austrian Workshop on Microelectronics (Austrochip). Linz, Austria, 47–52