We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and
privacy statement. We’ll occasionally send you account related emails.
Already on GitHub?
to your account
Issue by RobertBaruch
Sunday Jan 12, 2020 at 22:23 GMT
Originally opened as m-labs/nmigen#303
All too often I've been charging ahead writing formal assertions, and I forget to put one in a domain, writing:
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?
The text was updated successfully, but these errors were encountered:
Comment by whitequark
Sunday Jan 12, 2020 at 22:24 GMT
Absolutely possible, and we should do this. We already do this for Elaboratables.
Sorry, something went wrong.
No branches or pull requests