3 ms·
I 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
by smallpipe 5y ago
I 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.