Remove cover message in FIRRTL

[sequencer]

This PR removes message field in cover, according to reply from @ekiwi:

How is this message supposed to be displayed by different backends like SymbiYosys or Jasper Gold?
The reason cover does not have a message was that there did not seem to be a way to display it with the existing tools. If you want to give your cover points a name, you should be able to just use cover(...).suggestName("name")

Basically, there is no message field in System Verilog Spec defined at 19.5 Defining coverage points, for both MFC and SFC, they are not using message here, and Chisel is always generating empty message for cover(see chipsalliance/chisel#2912).

[mwachs5]

are these completely missing from the grammar at the end? should this PR add this (along with assert and assume) to formalize this?

[sequencer]

yes, I'm working on clear them up.

[sequencer]

I just found BNF doesn't include verification statements. I'll create another PR for it.

[dtzSiFive]

Thanks for chasing these and updating the spec / grammar!

FWIW SFC emits cover message as a comment presently, at least the 1.5.3 I have locally.

I have an outstanding PR changing MFC to do the same (user complained about it when moving to MFC), before noticing this PR and the discussion on the Chisel PR.

Having useful text to explain/associate with a verification statement is useful, but the "optional name" can serve that purpose, at least mechanically (not as friendly to read when turned into a label).
OTOH it's still inconsistent with the other verification ops (eep, if we like this behavior lets clear that up regardless) and I wouldn't expect this to help re:tools...

Regardless, there is a little utility to the field presently, but is that enough to warrant keeping it? Thoughts/preferences?

[ekiwi]

OTOH it's still inconsistent with the other verification ops

Afaik, the Chisel frontend does not actually use the message field for assert and assume. Instead a printf is generated along the verification op. This works pretty well for the chiseltest formal and simulation backends (Verilator, treadle, etc.). Not sure how it works with the commercial tools though since I do not have access to them.

Regardless, there is a little utility to the field presently, but is that enough to warrant keeping it? Thoughts/preferences?

I think it was a mistake to make this a part of the op. Some sort of optional meta-data field (would have been an annotation, now with CIRCT, it should probably part of the IR) might be better. Most importantly, we should have a good use-case description and things should be consistent.

[mwachs5]

I don't thing we can put a message string (with spaces, emojis) in the "optional name" . If we have users actively complaining that they are taking the time to write messages and they see it being dropped, it's something I'd want to keep in any user facing apis for cover, tbd how that is lowered. It's not the same as a printf... they are not asking that message to get printed out every time they hit the cover statement. Forcing it to be represented as a printf in the IR that we need to remove and turn into a comment seems convoluted.

If we do have it as a string in the IR for cover, we need to be clear if it is the kind of string that can take in fields from data (like printf does) or just a static string.

So I guess I am saying I am in favor of keeping in the spec as a string that can be lowered into a comment, unless optional name allows arbitrary characters in the string

[ekiwi]

So I guess I am saying I am in favor of keeping in the spec as a string that can be lowered into a comment, unless optional name allows arbitrary characters in the string

I think such a functionality can be useful, but it just seems like an arbitrary limitation that it would only work for cover. We could add a addComment method in Chisel, similar to suggestName which would work on stop, printf, cover, assert and assume (and maybe on ports, modules or similar stable elements in the future). Then we could add a construct to FIRRTL that allows comment strings to be directly attached to these statements. This would provide a more universal mechanism that users can rely on instead of a one-off thing for cover.

[dtzSiFive]

If we do have it as a string in the IR for cover, we need to be clear if it is the kind of string that can take in fields from data (like printf does) or just a static string.

Agreed!
(The cover message is as non-printf-like as the others described in the FIRRTL spec, so probably can clarify these together)

Agreed optional name seems a poor substitute, so short-term I'm in favor of keeping the message field (and lowering to comment) for that purpose. That said the spec could capture the meaning of this field for cover more explicitly, presently it is only explicit about asserts with behavior for cover/assume implied.
Longer-term we probably want to design ops/constructs that capture what we need, so we don't have to do the printf-encode-recover dance....?

Discussing/designing new verification operations, and perhaps a mechanism for attaching comments to operations, both seem like great tasks to pursue!

Very much agree re:providing good interface to users in Chisel and aiming to not have cover be a one-off.
Support for comments throughout the stack is interesting, we should make sure it's consistent and predictable-- does a comment on a port mean it can't be removed, and if it doesn't block such do we have a good story for how to combine comments, etc., are they "best effort"? I see you mentioned "stable elements", did you mean elements not likely to be removed / munged through the compilation process?

As an aside, this sort of mechanism may be (ab?)used to try to specify SV attributes, FWIW...

[ekiwi]

Longer-term we probably want to design ops/constructs that capture what we need, so we don't have to do the printf-encode-recover dance....?

That is a IR design philosophy question. Personally I found it much easier to leave message printing and formatting support restricted to one statement (printf) and not include it in things like assert. This kept the firrtl compiler as well as the firrtl spec simple. One thing that we are missing, is a way to associate a printf with e.g. an assert. That might be something to add to the firrtl spec similar to how SystemVerilog supports a printf on a failed assert (but of course in a much simpler manner since we are working on an IR, not a user facing language). It could look like this:

assert(clk, UInt(1), all_good) : assertion_1
on assertion_1 printf(clk, UInt(1), "not all is well and a=%x", a)

an alternative could be to treat assertions as UInt<1> signals that are true when the assertion fires, but that may have unintended consequences and might make it harder to recover which printf belongs to which assertion:

assert(clk, UInt(1), all_good) : assertion_1
printf(clk, assertion_1, "not all is well and a=%x", a)

[seldridge]

I am of the opinion that we should leave in the cover message, rename it to "comment", disallow format strings in comments (it must be a pure string), and specify that FIRRTL compilers should lower this to a comment in the backend language target. If a comment is not possible/available, the message should be elided.

As to whether or not anchored comments should be first-class, there's many ways of handling this:

1. Comments become operands of operations that support them. (How hardware dialect modules work in CIRCT.)
2. Comments are unstructured data attached to an operation. (Roughly what a DocStringAnnotation is today and how SystemVerilog attributes are represented in CIRCT.)
3. Comments are operations and must be anchored via another means, e.g., with a region operation.

[darthscsi]

It seems a first-class way to attach comments to declarations and statements would be helpful here and for other use cases (comments on wires and regs, for example). Until that appears, it probably makes sense to keep it on covers, but renamed appropriately to indicate it's actual meaning.