Add message to cover

[sequencer]

I thought this should be a bugfix according to the spec? not quite sure why message is omit in cover.

I use --lowering-options=verifLabels(see llvm/circt#1693) in mfc to test this, but seems firtool doesn't understand the message, and adds cover__$id as label.

Contributor Checklist

• Did you add Scaladoc to every public function/method?
• Did you add at least one test demonstrating the PR?
• Did you delete any extraneous printlns/debugging code?
• Did you specify the type of improvement?
• Did you add appropriate documentation in docs/src?
• Did you state the API impact?
• Did you specify the code generation impact?
• Did you request a desired merge strategy?
• Did you add text to be included in the Release Notes for this change?

Type of Improvement

API Impact

Backend Code Generation Impact

Desired Merge Strategy

Release Notes

Reviewer Checklist (only modified by reviewer)

• Did you add the appropriate labels?
• Did you mark the proper milestone (Bug fix: 3.4.x, [small] API extension: 3.5.x, API modification or big change: 3.6.0)?
• Did you review?
• Did you check whether all relevant Contributor checkboxes have been checked?
• Did you do one of the following when ready to merge:
  • Squash: You/ the contributor Enable auto-merge (squash), clean up the commit message, and label with Please Merge.
  • Merge: Ensure that contributor has cleaned up their commit history, then merge with Create a merge commit.

[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")

[sequencer]

i see. In this case, I think we should remove the message field in spec to avoid misleading to users.

[seldridge]

It looks like the spec had a message for covers since they were originally added: chipsalliance/firrtl#1653

I can see this going one of two ways:

1. FIRRTL (and Chisel) are free to define a message for covers. It doesn't matter if formal tools can show these or not as a valid lowering (for some backend) is to just drop the message. We could invent a lowering for these. Extracting a name from the message seems wrong, though, as this creates divergence between how assert/assume and cover treat their message.
2. The assert/assume/cover optional name need to be accessible from Chisel. suggestName is probably the closest thing to that right now. Does this work today?

MFC should pull the label from the optional name if it is provided. I think the issue right now is that that isn't accessible from Chisel.

I think (2) makes sense and we should not have a message for cover while also making the label accessible from Chisel.