chformal: Add -coverenable option

[georgerennie]

This inserts $cover cells to cover the enable signal (precondition/antecedent) for the selected formal cells. This allows you to check that your properties are not vacuous.

This will not cover preconditions that you write as part of the statement (e.g. this will cover a for if (a) assert(b), but not for assert(!a || b)). This should also work with preconditions arising from SVA in the verific front end (if the preconditions are converted to the enable signal as I believe they are?) but I do not have a copy to check (it does not as sequential properties are more complex).

[jix]

This seems like a very useful addition. While this is similar to select */t:$assert %ci:+$assert[EN]; supercover, supercover adds $cover cells for both the signal and the inverted signal and it ignores constant signals. I think adding an option to supercover to only cover one polarity and one to not ignore constant signals might be useful in general, but the required select statement is complicated enough that a dedicated option for chformal like this still seems warranted.

I added a test and changed it so it keeps the src attribute without prepending anything. That attribute is supposed to only contain source locations. Current versions of sby with smtbmc will display both the source location as well as the cell name. By using NEW_ID_SUFFIX("coverprecond") we still get a cell name that does point to the coverprecond feature specifically.

As you merged the yosys master back into your PR branch, I'm not sure if things go well if I merge this back again. I decided to cherry pick your commit, which also keeps my changes on top next to your commit. If you force push my https://github.com/jix/yosys/tree/chformal_coverprecond to your branch I can merge this PR (GitHub might also allow me to push to your PR branch, but I saw you're actively using this branch outside of this PR).

[georgerennie]

Sure, I can force push your branch. I had a thought about this feature the other day. Although I originally said I thought this might work with SVA implications from the verific frontend, I think it won't actually because you can have sequences on the right hand side of the implication (and I'm not certain the precondition is used as the enable for an assertion anyway).

Thus I think it might be worth renaming this feature to something like -coverenable, to make it clear that this just covers the enable signal of a direct assertion/assumption/etc.

The final remarks section in the yosyshq precondition cover app note also mentions potentially being able to automatically cover SVA preconditions in the future so it would be best not to confuse this feature with that one.

[georgerennie]

Any chance of this (and #3126) getting merged any time soon @jix?

[jix]

Yeah, I just needed a reminder 😅️ For this one I still want to review any differences in generated enable signals between the open source and the verific frontend, just so we can document any differences in the resulting behavior when using this. I should be able to do that before the next release.