All too often I've been charging ahead writing formal assertions, and I forget to put one in a domain, writing:
Assert(...)
instead of
m.d.comb += Assert(...)
This sort of thing is silently ignored, so I go on merrily believing my formal verification worked, when in fact I simply never verified certain assertions.
If anything, this is especially nasty for Asserts, Assumes, and Covers that do not get added to a domain. Can there at least be a warning there? Is it possible?
All too often I've been charging ahead writing formal assertions, and I forget to put one in a domain, writing:
instead of
This sort of thing is silently ignored, so I go on merrily believing my formal verification worked, when in fact I simply never verified certain assertions.
If anything, this is especially nasty for Asserts, Assumes, and Covers that do not get added to a domain. Can there at least be a warning there? Is it possible?