Ensuring that computer hardware behaves exactly as intended is a complex process. Formal Property Verification (FPV) uses precise statements, called assertions, to rigorously check hardware designs against their specifications. However, writing these assertions is a tedious, manual task, prone to human error. Could AI automate this crucial step? Researchers explored this question in "Automatic High-quality Verilog Assertion Generation through Subtask-Focused Fine-Tuned LLMs and Iterative Prompting." They developed AssertCraft, a tool that leverages Large Language Models (LLMs) like those powering ChatGPT to generate assertions automatically from hardware design documents. Because LLMs struggle with the multi-step reasoning required for this task, the researchers introduced a clever two-stage approach. First, they "fine-tuned" an LLM on a dataset of existing assertions and comments, training it to understand the relationship between human-language descriptions and formal assertions. Second, they implemented an "iterative prompting" method where a custom compiler provides feedback to the LLM, enabling it to correct errors in its generated assertions. This back-and-forth refinement process significantly improves the quality of the generated assertions. The results are promising. AssertCraft achieved a remarkable 7.3-fold increase in functionally correct assertions compared to a standard LLM. Furthermore, it demonstrated near-perfect coverage in many test cases, meaning it successfully generated assertions that checked most aspects of the hardware’s behavior. This research shows the potential of AI to automate complex hardware verification tasks, leading to faster development cycles and more reliable hardware. While challenges remain in refining the accuracy and coverage of LLM-generated assertions, this work points toward a future where AI plays a critical role in ensuring the bug-free operation of the chips powering our world.