LASP: LLM Assisted Security Property Generation for SoC Verification
Abstract
As the complexity of System-on-Chips (SoCs) increases, ensuring their security presents escalating challenges. Formal property verification is one of the most robust methods to model and check security behaviors using model checkers. However, the generation of these security properties is a labor-intensive endeavor. Large language models (LLMs) have been applied in multiple fields due to their excellent ability to understand natural language. Hence, this paper presents a novel framework that utilizes LLMs to automate the generation of security properties directly from Register Transfer Level (RTL) designs. By extracting critical features and security assets from both the design specifications and RTL, the framework systematically produces tailored security properties for specific hardware designs. These properties are systematically cataloged in a security property database, providing an essential resource for ongoing and future hardware verification efforts. The effectiveness of this innovative framework is validated through its application to various open-source hardware designs, confirming its ability to significantly improve SoC security verification by efficiently generating robust security properties.
Integrity signals
Registry
Cites
Statistics
Claims the paper makes
Claims other papers make about this one
Each is checked against this paper’s own text: does it say what the citing paper says it does?
Domain-specific context engineering proves especially valuable in specialized applications.
“Domain-specific context engineering proves especially valuable in specialized applications, with executionaware debugging frameworks achieving up to 9.8% performance improvements on code generation benchmarks and hardware design applications benefiting from specialized testbench generation and security property verification [1370, 881, 44].”
From A Survey of Context Engineering for Large Language Models (2025) · cites this paper as [44]
Hardware design applications benefit from specialized testbench generation and security property verification.
“Domain-specific context engineering proves especially valuable in specialized applications, with executionaware debugging frameworks achieving up to 9.8% performance improvements on code generation benchmarks and hardware design applications benefiting from specialized testbench generation and security property verification [1370, 881, 44].”
From A Survey of Context Engineering for Large Language Models (2025) · cites this paper as [44]
Execution-aware debugging frameworks achieve up to 9.8% performance improvements on code generation benchmarks.
“Domain-specific context engineering proves especially valuable in specialized applications, with executionaware debugging frameworks achieving up to 9.8% performance improvements on code generation benchmarks and hardware design applications benefiting from specialized testbench generation and security property verification [1370, 881, 44].”
From A Survey of Context Engineering for Large Language Models (2025) · cites this paper as [44]
Cites
Vaswani, A., Shazeer, N., Parmar, N., Uszkoreit, J., Jones, L., Gomez, A. N., Kaiser, L., & Polosukhin, I. (2017) · arXiv · doi:10.48550/arxiv.1706.03762 · Cited by 120,404 · see citing works
Fault Injection Attacks on Cryptographic Devices: Theory, Practice, and Countermeasures
Barenghi, A., Breveglieri, L., Koren, I., & Naccache, D. (2012) · Proceedings of the IEEE · doi:10.1109/jproc.2012.2188769 · Cited by 610 · see citing works
Pyverilog: A Python-Based Hardware Design Processing Toolkit for Verilog HDL
Takamaeda-Yamazaki, S. (2015) · Lecture notes in computer science · doi:10.1007/978-3-319-16214-0_42 · Cited by 203 · see citing works
Nahiyan, A., Xiao, K., Yang, K., Jin, Y., Forte, D. J., & Tehranipoor, M. M. (2016) · ACM/IEEE Design Automation Conference (DAC) · doi:10.1145/2897937.2897992 · Cited by 106 · see citing works
SoC Security Verification using Property Checking
Dipu, N. F., Rahman, F., Tehranipoor, M. M., & Farahmandi, F. (2019) · IEEE International Test Conference (ITC) · doi:10.1109/itc44170.2019.9000170 · Cited by 56 · see citing works
Self-citationUnlocking Hardware Security Assurance: The Potential of LLMsPreprint
Meng, X., Srivastava, A., Arunachalam, A., Ray, A., Silva, P., Psiakis, R., Makris, Y., & Basu, K. (2023) · arXiv.org · doi:10.48550/arxiv.2308.11042 · Cited by 55 · see citing works
SoFI: Security Property-Driven Vulnerability Assessments of ICs Against Fault-Injection Attacks
Wang, H., Li, H., Rahman, F., Tehranipoor, M. M., & Farahmandi, F. (2021) · IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems · doi:10.1109/tcad.2021.3063998 · Cited by 53 · see citing works
Self-citationChIRAAG: ChatGPT Informed Rapid and Automated Assertion Generation
Mali, B., Maddala, K., Gupta, V., Reddy, S., Karfa, C., & Karri, R. (2024) · IEEE Computer Society Annual Symposium on VLSI · doi:10.1109/isvlsi61997.2024.00130 · Cited by 40 · see citing works
Using LLMs to Facilitate Formal Verification of RTLPreprint
Orenes-Vera, M., Martonosi, M., & Wentzlaff, D. (2023) · arXiv (Cornell University) · doi:10.48550/arxiv.2309.09437 · Cited by 40 · see citing works
Towards Property Driven Hardware Security
Hu, W., Althoff, A., Ardeshiricham, A., & Kastner, R. (2016) · International Workshop on Microprocessor Test and Verification (MTV) · doi:10.1109/mtv.2016.12 · Cited by 34 · see citing works
Evolutionary Large Language Models for Hardware Security: A Comparative Survey
Akyash, M., & Kamali, H. M. (2024) · ACM Great Lakes Symposium on VLSI (GLSVLSI) · doi:10.1145/3649476.3660390 · Cited by 26 · see citing works
SpecLLM: Exploring Generation and Review of VLSI Design Specification with Large Language Model
Li, M., Fang, W., Zhang, Q., & Xie, Z. (2025) · International Symposium of Electronics Design Automation (ISEDA) · doi:10.1109/iseda65950.2025.11100410 · Cited by 21 · see citing works
Fang, W., Li, M., Li, M., Yan, Z., Liu, S., Zhang, H., & Xie, Z. (2024) · arXiv (Cornell University) · doi:10.48550/arxiv.2402.00386 · Cited by 18 · see citing works
DIVAS: An LLM-based End-to-End Framework for SoC Security Analysis and Policy-based Protection
Paria, S., Dasgupta, A., & Bhunia, S. (2023) · arXiv · doi:10.48550/arxiv.2308.06932 · Cited by 17 · see citing works
Automatic Asset Identification for Assertion-Based SoC Security Verification
Ayalasomayajula, A., Dipu, N. F., Tehranipoor, M. M., & Farahmandi, F. (2024) · IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems · doi:10.1109/tcad.2024.3387875 · Cited by 12 · see citing works
Self-citationFormal Approaches to Hardware Trust Verification
Farahmandi, F., Huang, Y., & Mishra, P. (2017) · Springer eBooks · doi:10.1007/978-3-319-68511-3_8 · Cited by 5 · see citing works
Self-citation
Flagged first, then by citations
1 of the 17 references couldn’t be matched to a known paper.
Cited by
Sorted by citations
Large Language Models for EDA: Future or Mirage?
He, Z., Pu, Y., Wu, H., Qiu, T., & Yu, B. (2025) · ACM Transactions on Design Automation of Electronic Systems · doi:10.1145/3736167 · Cited by 21 · see citing works
Schemato – An LLM for Netlist-to-Schematic Conversion
Matsuo, R., Uhlich, S., Venkitaraman, A., Bonetti, A., Hsieh, C.-Y., Momeni, A., Mauch, L., Capone, A., Ohbuchi, E., & Servadei, L. (2025) · ACM/IEEE Workshop on Machine Learning for CAD (MLCAD) · doi:10.1109/mlcad65511.2025.11189059 · Cited by 17 · see citing works
A Survey of Context Engineering for Large Language Models
Mei, L., Yao, J., Ge, Y., Wang, Y., Bi, B., Cai, Y., Liu, J., Li, M., Li, Z.-Z., Zhang, D., et al. (2025) · arXiv · doi:10.48550/arxiv.2507.13334 · Cited by 13 · see citing works
Towards Automated Verification of IP and COTS: Leveraging LLMs in Pre- and Post-Silicon Stages
Paria, S., Dasgupta, A., & Bhunia, S. (2025) · IEEE VLSI Test Symposium (VTS) · doi:10.1109/vts65138.2025.11022781 · Cited by 8 · see citing works
LASSO: LLM-Aided Security Property Generation for Assertion-based SoC Verification
Ankireddy, D. R., Paria, S., Dasgupta, A., Ray, S., & Bhunia, S. (2025) · ACM/IEEE Workshop on Machine Learning for CAD (MLCAD) · doi:10.1109/mlcad65511.2025.11189178 · Cited by 7 · see citing works
LLMs for Hardware Verification: Frameworks, Techniques, and Future Directions
Qayyum, K., Ahmadi-Pour, S., Jha, C. K., Hassan, M., & Drechsler, R. (2024) · Proceedings - Asian Test Symposium/Proceedings · doi:10.1109/ats64447.2024.10915476 · Cited by 5 · see citing works
AI-Assisted Hardware Security Verification: A Survey and AI Accelerator Case Study
Hasan, K. T., Hasan, M. A., Alam, N., Islam, M. T., Das, U., & Farahmandi, F. (2026) · IEEE VLSI Test Symposium (VTS) · doi:10.1109/vts69484.2026.11563216 · Cited by 4 · see citing works
Self-citationLISA: LLM Informed Systemverilog Assertion generation with RAG and Chain-of-Thought
Paul, S., Banerjee, A., Ghosh, S., Surendran, S., & Gajavelly, R. K. (2025) · IEEE Computer Society Annual Symposium on VLSI · doi:10.1109/isvlsi65124.2025.11130226 · Cited by 3 · see citing works
LAMBDA: LLM-Assisted Malicious Bug Detection and Analysis in Hardware Designs
Paria, S. (2025) · IEEE International Test Conference (ITC) · doi:10.1109/itc58126.2025.00091 · Cited by 3 · see citing works
FV-PAL: Scalable Formal Verification through Partitioning and LLM-Guided Property Generation
Paria, S., Dasgupta, A., Ankireddy, D. R., Chakraborty, P., & Bhunia, S. (2025) · IEEE International Conference on Computer Design: VLSI in Computers and Processors (ICCD) · doi:10.1109/iccd65941.2025.00114 · Cited by 3 · see citing works
Harnessing the Power of LLMs for Enhancing Hardware Security
Paria, S., & Bhunia, S. (2026) · SN Computer Science · doi:10.1007/s42979-026-04799-8 · Cited by 3 · see citing works
Knowledge Graphs, the Missing Link in Agentic AI-based Formal Verification
Viswambharan, V. N., Radhakrishna, K. K., Gadde, D. N., & Kumar, A. (2026) · IEEE International Conference on IC Design and Technology (ICICDT) · doi:10.1109/icicdt69693.2026.11669279 · Cited by 2 · see citing works
ATLAS: AI-Assisted Threat-to-Assertion Learning for System-on-Chip Security Verification
Tashdid, I., Tasnia, K., Garcia, A., Valamehr, J., & Rahman, S. (2026) · ACM/IEEE Design Automation Conference (DAC) · doi:10.1145/3770743.3804400 · Cited by 1 · see citing works
Werthwein, M., Annighöfer, B., & Daw, Z. (2025) · Integrated Communications, Navigation and Surveillance Conference (ICNS) · doi:10.1109/icns65417.2025.10976786
Context-Enhanced Architectural Specification Generation for SoC Designs
Ahmed, M. R., Nur, S. N., & Ewetz, R. (2025) · ACM/IEEE Workshop on Machine Learning for CAD (MLCAD) · doi:10.1109/mlcad65511.2025.11189058
Automatic SystemVerilog Assertion Generation: Challenges and Opportunities
Afsharmazayejani, R., Pearce, H. A., & Tan, B. (2025) · Conference proceedings - Canadian Conference on Electrical and Computer Engineering · doi:10.1109/ccece64018.2025.11364438
SuperSAGA: A Supervisor-Subordinate Agentic workflow for the Generation of Assertions
Paul, S., Banerjee, A., Ghosh, S., Surendran, S., & Gajavelly, R. K. (2026) · Asia and South Pacific Design Automation Conference (ASP-DAC) · doi:10.1109/asp-dac66049.2026.11420235
Closing the Loop: Overcoming the Tool-Feedback Gap in Agentic Hardware Design
Tarighat, M., Gubbi, K. I., Javidnia, N., Marosok, N., Shabgahi, S. Z., Halm, M., Nejad, M. P. S., Rafatirad, S., Koushanfar, F., & Homayoun, H. (2026) · International Symposium on Quality Electronic Design (ISQED) · doi:10.1109/isqed69900.2026.11534671
PALM: Program Analysis and LLM Methods for Crafting SystemVerilog Assertions
Afsharmazayejani, R., & Tan, B. (2026) · Design, Automation, and Test in Europe · doi:10.23919/date69613.2026.11539183
Survey and Roadmap for Efficiency-Accuracy Cooptimization Towards Embodied AI Chip Design
Zhao, J., Yu, H., & Li, Y. (2026) · International Symposium on Intelligent Robotics and Systems (ISoIRS) · doi:10.1109/isoirs70157.2026.11545322
Can Agents Secure Hardware? Evaluating Agentic LLM-Driven Obfuscation for IP Protection
Ghimire, S., Mirfasihi, P., Chowdhury, M. A., Pugazhenthi, V., Dharavath, H. K., Firouzi, F., Yasaei, R., Satam, P., & Salehi, S. (2026) · IEEE VLSI Test Symposium (VTS) · doi:10.1109/vts69484.2026.11563377
Coverage-Driven RTL Assertion Generation with Formal Exploration and Neuro-Symbolic RefinementPreprint
Yan, Z., Zheng, Z., & Zhang, H. (2026) · arXiv (Cornell University) · doi:10.48550/arxiv.2608.18482
Towards Reliable LLM-Assisted Verification Artifact Generation in EDA
Qayyum, K., Ain, Q. U., Hassan, M., Afnan, A., & Drechsler, R. (2026) · IEEE International Conference on Omni-layer Intelligent Systems (COINS) · doi:10.1109/coins69995.2026.11715594
LLM-Based Security Verification: Vulnerability Detection and Analysis
Guo, R., Uddin, A., Sarker, P. P., Das, U., Tehranipoor, M., & Farahmandi, F. (2026) · Springer eBooks · doi:10.1007/978-3-032-34116-7_5
Self-citationThreat Modeling and Property Generation in SoC Security
Hasan, M. A., Ibnat, Z., Tarek, S., Ahmed, B., Ayalasomayajula, A., Das, U., Tehranipoor, M., & Farahmandi, F. (2026) · Springer eBooks · doi:10.1007/978-3-032-34116-7_6
Self-citation
- Authors
- Ayalasomayajula, A., Guo, R., Zhou, J., Saha, S. K., & Farahmandi, F.
- Affiliations
- University of Florida (US)
- Venue
- 2024 ACM/IEEE 6th Symposium on Machine Learning for CAD (MLCAD)
- Publisher
- IEEE
- Published
- 2024-09-09
- Pages
- 1-7
- OpenAlex
- W4404102090
- Cited by
- 15
- References
- 17
- Citations by year
- 2026: 7 · 2025: 7 · 2024: 1
- FWCI
- 9.75
- Type
- conference paper
- Language
- en
- Open access
- closed
- Locations
- ACM/IEEE Workshop on Machine Learning for CAD (MLCAD) (publishedVersion)
- Topics
- Physical Sciences › Computer Science › Computational Theory and Mathematics › Formal Methods in Verification
- Physical Sciences › Computer Science › Hardware and Architecture › Physical Unclonable Functions (PUFs) and Hardware Security
- Physical Sciences › Computer Science › Hardware and Architecture › Embedded Systems Design Techniques
- Keywords
- system-on-chip security, formal verification, model checking, large language models, register-transfer level design, hardware security
About these checks
Registry, retraction, Cites and statistics results are computed, not judged, with one exception: a printed reference that no index lists is read once by a model before it counts as a citation error. Claims are extracted by a model and kept only when their quote appears verbatim in the text; each cited source is then checked, with a model’s help, for whether it says what the claim relies on. Those verdicts can be wrong — read the claim’s quote and the cited source before relying on one.
Statistics and arithmetic are recomputed, not judged.
Confidence bands are shown only for fields calibrated on our annotated test set. None is calibrated yet, so no band is shown.
What counts as a claim ›How we measure confidence ›How we check this ›
Are you an author, or do you see a problem with this page? Request a review
