3 ms·
> You can’t write something like “a trace of X state transition must be possible within N cycles with the right inputs”. You can, although possibility properti
by pron 5y ago
> You can’t write something like “a trace of X state transition must be possible within N cycles with the right inputs”.
You can, although possibility properties aren't for beginners: https://youtu.be/TP3SY0EUV2A?t=818 https://youtu.be/TP3SY0EUV2A?t=818
But there often are easier ways to do sanity checks to "convince yourself you haven’t assumed all of the state away," usually either by asserting something believed to be false or by intentionally introducing an error in the spec, and letting TLC find a counterexample.
- smallpipe 5y agoI agree it’s workable, but it’s a bit of a hack. Commercial formal verification software for RTL has this built-in, and once you have 10+ people updating a spec, you need an automated way of checking for accidental constraints.
- pron 5y agoI don't think possibility properties are directly expressible in any linear-time logic, just branching-time logics, and those have their own issues, even though I think they're still sometimes used. A mistake that could be automatically checked is specifying a system that is equivalent to FALSE (and so implies anything). I hope TLC adds a feature that allows you to check if your system implies FALSE. In the meantime, checking the invariant ¬Init has the same effect.