<whitequark[cis]>
this RFC concerns functionality that was present at one point as an ad-hoc implementation, but was removed since it was rather yosys-specific
* anuejn
is here
<whitequark[cis]>
in practice people were using these labels (with poorly defined syntax) as a replacement for error messages, so we added error messages instead and removed the labels
<whitequark[cis]>
I'm not too keen on adding them back since all of the reasons for which they were removed still hold
<whitequark[cis]>
from my perspective, this is just adding a poorly designed interface to work around deficiencies in other tools
<whitequark[cis]>
in particular, I don't think that the motivating example is actually motivating much: sby can and should be fixed to display a proper message from the $check cell, and Jannis expressed interest in making that happen. so that example should be fixed in sby, not in Amaranth
<vup>
for me the main motivation is not sby, but jasper
<vup>
which seems hard to get changed being a proprietary tool
<whitequark[cis]>
for Jasper, if it really is completely unable to display anything but the label, we could take the error message and translate it (with the appropriate escaping) to the label it needs, somehow taking care to not mess up sby output (as is seen in the drawbacks section). this wouldn't need an RFC, and won't result in littering code with workarounds for tools that will stay even after the tool is fixed
<whitequark[cis]>
if the main motivation is Jasper then the motivation section should include the UI excerpts for Jasper
<whitequark[cis]>
otherwise it's not really clear what is gained
<whitequark[cis]>
I also suspect that "any non-whitespace character" alphabet for the label is wrong: does it handle { as a part of the label? what about "? what about Unicode? I'm sure some special characters will break it. we should not have aspects of language that are defined by ambiguous deference to the behavior of other tools
<whitequark[cis]>
okay
<whitequark[cis]>
I think the label should be derived from the message, and probably only in case someone is using Jasper
<whitequark[cis]>
this can probably be done either as a simple Yosys script, or as a write_verilog parameter
<vup>
ah yeah, any non-whitespace character is imprecise. I think was generated (in my head) from a combination of what yosys accepts and what the systemverilog reference manual accepts. iirc systemverilog accepts arbitrary identifiers (same as module names, etc), as labels, but yosys does not allow the escaped identifiers as labels
<vup>
will amaranth ever support formatting in the assertion message?
<Wanda[cis]>
we do already
<whitequark[cis]>
it already does
<vup>
oh
<vup>
how would this be handled when deriving the label from the message
<whitequark[cis]>
probably turn the format string into the label as-is
<whitequark[cis]>
there's no good way to handle it
<vup>
yeah. I feel like there would be some tension between writing informative messages for assertions (for usage in simulation / with sby) and avoiding formatting when using jasper for formal. But of course this stands in opposition to having to write both, a label and a message with my suggestion
<whitequark[cis]>
from my perspective this is a workaround for a jasper issue, so it's difficult to motivate it as a language design addition
<Wanda[cis]>
hm
<whitequark[cis]>
I particularly dislike how the semantics is defined entirely in terms of "whatever Jasper happens to need" without regard to other tools
<Wanda[cis]>
how "supported" are the Cover cells?
<Wanda[cis]>
so. Asserts are interesting when you trigger them and they fail. so are Assumes.
<Wanda[cis]>
and when that happens, you have signal state and you can output a message
<vup>
well from what I have read, using the labels seems to be a common thing. But I only have access to jasper, so I cannot speak for any other (proprietary) tools with certainty.
<vup>
But yeah I understand how this is low motivation for a lanugage addition, that could probably be done as a yosys script.
<Wanda[cis]>
but Covers are interesting when they're not hit, ever
<Wanda[cis]>
and this means no signal state
<Wanda[cis]>
I guess these are just not supposed to have a variable format argument?
<whitequark[cis]>
I think so? we don't really have a working design for cover cells
<whitequark[cis]>
but yes, probably
<whitequark[cis]>
(I wonder if you could still have meaningful substitutions in them in case your design is generic and parameterized by constants)
<Wanda[cis]>
those would be lowered in elaboration, I think?
<whitequark[cis]>
mm, right
<whitequark[cis]>
yeah
<Wanda[cis]>
either way
<Wanda[cis]>
it may be useful to have short identifiers for properties if you view them in a big-ass table of all properties in your design? like the CI tools tend to output from junit stuff
<whitequark[cis]>
we can add that, provided the design is more fleshed out than "Jasper needs this"
<zyp[m]>
I have no experience with formal tools, but to me it can make sense to both have identifiers and messages and not attempting to shoehorn one into the other
<whitequark[cis]>
at the very least I would expect the interaction with pysim to be defined in some useful way
<whitequark[cis]>
the accepted grammar for them also should be defined in terms of Unicode character data
<whitequark[cis]>
also, the implementation should be done in a way that works well with sby
<Wanda[cis]>
okay, so, my opinion
<Wanda[cis]>
in short, I think a) short labels could be useful in addition to formatted messages, b) this RFC should be tabled until we have well-defined FV semantics in the first place
<Wanda[cis]>
I don't think pysim will have anything much to do with the labels, besides maybe printing them together with the actual message (presumably as part of a hierarchical identifier that also includes the modules it's contained in)
<Wanda[cis]>
and this is fine; labels are for formal tools to consume and pysim is not a formal tool
<Wanda[cis]>
now, as for why they are useful: format messages inherently assume you have design state and are geared towards simulation; if shit fails, you print an error message with the stuff you were doing when it failed, and halt
<Wanda[cis]>
for formal, you may have such a failure case (if you can construct a failing path), but you can also just fail to prove some properties without a counterexample
<Wanda[cis]>
so you'd want something more like "long list of short identifiers" for all the non-proven stuff
<whitequark[cis]>
these are all good points
<whitequark[cis]>
it sounds reasonable to me
<Wanda[cis]>
actually, one place where I could find the labels useful in pysim is junit-style output, mostly for cover stuff
<Wanda[cis]>
just list all covers in code, and whether they were hit during the sim or not (maybe with one instance of the formatted message if yes)
<vup>
(you could also have infinite length counterexamples for liveness properties, where it also might be tricky to print a useful message)
<Wanda[cis]>
we do not have liveness properties at this point, so I consider this moot
<whitequark[cis]>
we're almost out of time. does any else disagree with Wanda's proposal here?
<zyp[m]>
no, that sounds reasonable to me
<cr1901>
Sounds fine to me
<vup>
sounds fine to me aswell
<Wanda[cis]>
in summary, my vote is postpone; I could vote merge on this if it was part of a larger RFC that defined how formal works in amaranth, or proposed junit output for pysim like I outlined, or otherwise didn't built on undefined semantics
<whitequark[cis]>
I concur
<whitequark[cis]>
Wanda, could you update the RFC issue please?
catlosgay[m] has joined #amaranth-lang
<catlosgay[m]>
i think labels and formatted messages make sense
<catlosgay[m]>
and the label thing in jasper is more a verilog thing than specifically jasper
<catlosgay[m]>
but its often useful to be able to refer to specific properties (e.g. to convert assertions to assumptions when doing compositional verification, to disable specific assumptions in certain scenarios, to waive failing assertions in certain scenarious etc) and format messages don't make sense for that whereas labels do