Synopsys Cloud
Cloud native EDA tools & pre-optimized hardware platforms
Request a Free Trial →
Who wouldn't appreciate a head start in life? Imagine the convenience of always being at the front of every queue, or better yet, starting a long-haul flight from the UK to California already over the Rocky Mountains, avoiding the tediousness of the entire journey. While certain privileges like money or fame might grant you front-of-the-line access in some scenarios, we're still waiting for a technological leap like teleportation to make those long flights feel shorter.
This longing for a head start stems from our dislike for wasted time, for those moments where we could be productive but end up idle. This sentiment is particularly relevant in the field of verification runs in Formal verification, where minimizing wait time for results is always a priority.
Typically, a Formal run starts from a reset state. This approach is logical, as it provides a known, stable starting point, preventing misleading failures from incorrect initial states. However, in designs with considerable sequential depth, this could complicate the tool's task of covering all possible states. Consider a bug deep within the design's state space, simple in nature but occurring after numerous cycles. Beginning from the reset state means the tool has to traverse significant sequential depth to detect this bug. While Formal tools are equipped to navigate through this efficiently, we might wonder if there's a way to give them an even greater advantage.
There are two intriguing methods to tackle this. The first involves providing the tool with a specific state to start from, in the form of an FSDB. This method, deriving an initial state from a simulation, offers a valid and advantageous starting point. Ideal for bug hunting, this approach does have its limits, as proofs obtained may not hold universally.
An alternative strategy is to abstract the initial state entirely. This method boosts verification by granting the tool more flexibility. The Formal tool will always attempt to fail your assertions, so by allowing it to select any starting values for your registers, it will choose those that are most likely to cause failure. Whether you opt for a completely unknown initial state or preload certain values, this can significantly accelerate the tool's response time. The caveat, however, is the potential for spurious failures. Utilizing this technique demands specially crafted properties, such as inductive assertions, which state that if a condition is true now, it should remain true in the future.
For example, an inductive assertion like "A==B |=> A==B" requires alignment of A and B before activation. This approach can drastically reduce spurious failures, transforming checks that previously needed thousands of cycles to fail into ones that fail in just a couple of cycles.
Abstracting the initial state is a powerful technique to reduce Formal tool runtime, yielding rapid results. However, it's crucial to understand the implications of using an unknown initial state and the potential for spurious failures it brings. As with most things in life, these advantages don't come without their trade-offs.
Continue Reading
Blog
4 min read
/
Nov 18, 2024
AI Startups are Using the Cloud to Accelerate Chip Design and Time-to-Market
