草榴社区

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.