<Wanda[cis]>
Catherine: so as a general question provoked by the stream RFC, do we want to have a way to include well-formedness assertions with `lib.wiring`-based interfaces?
<Wanda[cis]>
like, there are a few properties regarding streams that sound like they would translate directly to some Assert statements (plus a few helper registers), and maybe we'd want these Assert statements to materialize automatically when you use a simulation or formal platform?
<jfng[m]>
<whitequark[cis]> "anyway. I think my broader..." <- the -soc CSR register API benefited greatly from the RFC process
<jfng[m]>
granted, this feature was built upon another which existed for a few years already (the CSR bus) and didn't go through an RFC
<jfng[m]>
i think we can relax the policy of "every non-trivial change" has to go through an RFC we've been having lately
<jfng[m]>
and still do RFCs for the bigger features, where we can get the most value from a consensus-driven process
<whitequark[cis]>
<Wanda[cis]> "Catherine: so as a general..." <- that seems like a pretty big feature that would intersect with any formal verification platform we'll have, and also clock domains in interfaces
<whitequark[cis]>
so the answer is "probably not right now"
<whitequark[cis]>
<jfng[m]> "and still do RFCs for the bigger..." <- would e.g. the GPIO peripheral qualify as a bigger feature?
<jfng[m]>
no
<jfng[m]>
but the BSP generator certainly would
<jfng[m]>
AXI support would too, probably
<whitequark[cis]>
sounds fine by me
<jfng[m]>
i'm still in favor of still doing an RFC for peripherals, when in doubt
<whitequark[cis]>
I'm not exactly opposed to that, we just need more maturity (of both the Amaranth SoC codebase and process participants)
omnitechnomancer has quit [Quit: Idle timeout reached: 172800s]
cr1901_ is now known as cr1901
antoinevg[m] has joined #amaranth-lang
<antoinevg[m]>
<jfng[m]> "i'm still in favor of still..." <- 100% yes please.
notgull has joined #amaranth-lang
<anuejn>
whitequark[cis]: I really like the streams rfc
<anuejn>
it is quite similiar (although not syntactically) to what we are currently doing and has similiar rules
<anuejn>
but it is much better specced
<antoinevg[m]>
I really liked the folding of first and last into the payload.
<anuejn>
and in some places has smart design descisions (like not polluting the streams namespace with payload signals) which removes the footgun of changing first, last, or similiar stuff outside of transactions
<anuejn>
antoinevg[m]: very much this
<anuejn>
I quite often shot myself in the foot with this
<anuejn>
I do not understand the "transformers" thingy quite yet and am very confused by the name
<anuejn>
(but that might be just because we have a totally different stream related concept, we call transformers)
<anuejn>
But since that is only an outlook, I am very fine with it :)
<anuejn>
congratulations to this great piece of design
<anuejn>
one thing though: I would love to see utilities in the standard library for formally verifying that a thing complies with the stream invariants
<anuejn>
That might increase the number of third-party cores, that are actually compliant greatly
<anuejn>
but probably that is for another RFC
notgull has quit [Ping timeout: 264 seconds]
<whitequark[cis]>
<anuejn> "one thing though: I would love..." <- we don't have first clasa FV support yet
<whitequark[cis]>
but yeah
<whitequark[cis]>
* we don't have first class FV support yet
<Wanda[cis]>
I think the invariants are simple enough that you could just use the exact same naïve asserts that you'd want in sim?
<whitequark[cis]>
oh, I mean we don't have an FV runner
<Wanda[cis]>
but yeah actually coming up with infra for this need some thinking
ldcd[m] has quit [Quit: Idle timeout reached: 172800s]
<_whitenotifier-6>
[amaranth-lang/amaranth-lang.github.io] whitequark c3f8b3c - Deploying to main from @ amaranth-lang/rfcs@ea8b1d29af93181cdeab57cbbace643d5895665e 🚀