add RFC for property labels

[rroohhh]

Rendered

[whitequark]

If the goal is to produce human friendly error messages, why are these tools not using the message field? I would say we should probably not add back name but figure out why is message not used.

[wanda-phi]

If the goal is to produce human friendly error messages, why are these tools not using the message field? I would say we should probably not add back name but figure out why is message not used.

SystemVerilog assertions do not have messages in the first place; relying on messages thus limits us to yosys-based tooling

on the other hand, the example given in the RFC could definitely be fixed on sby side

[whitequark]

SystemVerilog assertions do not have messages in the first place; relying on messages thus limits us to yosys-based tooling

From my memory of talking to Jannis, they sort of do, in that assert x else $error is treated specially, or something along those lines. This is also how the Yosys $check cell is implemented, and both parsing and emitting should respect that.

[rroohhh]

I care more about Jasper than sby at the moment to be honest.
Jasper names the properties at elaboration time and $error can include formatting, so I guess that is why its not used?

[whitequark]

@jix, would you happen to have advice here? I've never used Jasper.

[wanda-phi]

We have discussed this RFC on the 2025-05-26 core subsystem meeting. The disposition was to postpone.

The motivation in the RFC (sby needs it to print a good message) was deemed insufficient, as we already have messages attached to properties. Likewise for the secondary motivation of using Jasper — if a workaround is needed, we can just generate labels from messages in some part of the stack.

More importantly, Amaranth currently doesn't have well-defined formal semantics — there is no formal verification mode in Amaranth at all, and all formal-specific language features are essentially RTLIL legacy with no clear definition other than "what yosys and sby do". Any kind of RFC proposing features with FV justification thus has to be blocked by necessity until a formal model is proposed.

[jix]

I don't have any good advice regarding tool compatibility, I've also never used Jasper. I can confirm that using labels to identify properties seems what most FV users I've interacted with rely on, but I've also seen else $error being used in multiple places, but IIRC always in combination with also giving a label. I have no idea which tools the instances of that were originally targeting, though.

The SV spec defines the omission of an else ... "action block" to result in a call to $error if the assertion fails, so in that sense manually calling $error from the "action block" should be expected to work as intended, since it's defined to be the same thing (modulo the exact message used). With half of the spec only making sense for simulation, and non-simulation tools widely deviating from the spec even where they could follow it (whether for good or for questionable reasons) that all does end up being somewhat meaningless in practice though.

[whitequark]

Thanks @jix!