Key Takeaways: While AI can write properties from a specification, the specifications that exist today are rarely good enough to be able to generate anything useful from them. Automatic generation of properties does not reduce the need for people who are fluent in the language, or the application of formal tools. Introduction into a methodology will probably be different for each company today, with no well-proven methodologies to learn from. A top-down semiconductor development flow has long been a goal for chip design, and shift left is certainly making that increasingly possible. The problem is that the starting point — the specification — is often incomplete or nonexistent, because the chip industry has been notoriously bad at writing specifications. There are several ways to insert AI into existing flows. But just because something can be done doesn’t mean it should be. This is one of the big challenges facing AI adoption. Many existing tasks could be done more efficiently using an agentic flow, but it’s not clear whether that is the right thing to do. This limitation becomes especially apparent when AI starts to help with something that has been woefully inadequate in the past — the creation of good, complete specifications. The big question is whether AI can enable designs, or verification environments, to be automatically derived from a specification. Perhaps a more correct goal is whether AI can help create better specifications. With better specifications, downstream design becomes a lot easier. “AI can generate a SystemVerilog assertion in seconds,” says Ben Cohen, verification technologist and book author. “Whether that assertion means anything depends entirely on what it was generated from, and in practice that source is rarely a single, clean, natural-language specification. It is just as often an ambiguous paragraph that needs clarifying before it can be trusted.” Solving this problem should be considered a high priority. “The increasing complexity of modern SoC designs is making AI-assisted artefact generation and verification closure a practical requirement rather than a research option,” says Simon Davidmann, AI and EDA researcher at the University of Southampton. “The verification problem is, in practice, already at the scale where it cannot be addressed without AI assistance. The 5-to-1 ratio of verification engineers to designers in processor development is not a workforce planning anomaly, but a signal that the complexity has outgrown the methods.” Going from specification to anything is not a reality today. “If we are actually going to make this reality, we need more discipline in terms of writing the spec,” says Ravindra Aneja, director of applications engineering at Synopsys . “If we really want to make it a reality, we have to work on it. As an industry, are we there? No, we are not there. I don’t think we are at a place where, either starting a new design or doing a derivative design, you can say the spec is good enough.” Are we even thinking about it in the right way? “A prose specification document is not something a formal tool can reason over directly, because formal engines operate on precise, unambiguous, machine-checkable statements, not natural language,” says Ashish Darbari, CEO of Axiomise . “What AI can help with is narrowing that gap, translating prose into candidate formal statements faster, which is really what deriving properties from specification means in practice. The properties are the formalization of the spec, not a separate step after it. So rather than thinking of it as spec first, then properties, then formal proof, it is more accurate to say the property set is the machine-readable spec, and formal is working on the spec once that translation has happened.” Sometimes, specifications are purposely ambiguous. “Human designers interpret them with domain knowledge, prior experience, and the ability to ask clarifying questions,” says Southampton’s Davidmann. “AI models receive the