<Raito_Bezarius>
tpw_rules: idk, I think there's a place for it as long as it's done in a nixpkgs way
<Raito_Bezarius>
Maybe this implies cutting down on the scope
<Raito_Bezarius>
But most of the lite packages are fairly mundane, well tested Python packages
<Raito_Bezarius>
It's not very different from e.g. the Azure Python package ecosystems for me
<tpw_rules>
you already have a very tiny scope, that's why i think that. i think i would want it expanded to be more useful, but then idk if it woudl fit
<tpw_rules>
i'll look at it in a little more depth though
<Raito_Bezarius>
Well this is then a scaling problem
<tpw_rules>
maybe we need to sit down and come up with a better story, i haven't paged litex in in a long time
<tpw_rules>
and Leon's approach did seem somewhat overcomplex
<tpw_rules>
one thing we also did there, partially for style and partially for flexibility, is wrangling SBT so that nix could build the vexriscv vores too
<tpw_rules>
cores*
<tpw_rules>
litex itself really needs a refactoring on all their pythondata repos too, but i haven't had the investment to do much except pitch it...
<Raito_Bezarius>
Yeah
<Raito_Bezarius>
I don't really care about building the Java stuff myself
<Raito_Bezarius>
All I want is to be unblocked to use Amaranth on my designs
<tpw_rules>
i ended up needing it for my stuff because they did not ship a compatible core for the demos. if one's not in the repo then it will just shell out to sbt
<tpw_rules>
i don't understand how amaranth relates?
<Raito_Bezarius>
I just want to mix LiteX core code and Amaranth code
<Raito_Bezarius>
And I want this properly set in Nix exprs
<tpw_rules>
ah
<tpw_rules>
would you do the advanced stuff like dragging in a CPU?
<Raito_Bezarius>
Ultimately yes, for now, I'd take it for a walk and see how it goes
<Raito_Bezarius>
I also want to push proper builders for gateware in nixpkgs itself
<Raito_Bezarius>
Like the Tillitis one
<Raito_Bezarius>
Either way, I think there's potential to do fun things and experiment :)
<tpw_rules>
for sure, i think i'm just more conservative about putting things in nixpkgs, personally
<tpw_rules>
but the random shelling in litex is what gets me, i'd want that all patched out. and that does hamper the utility of things like the vexriscv
<tpw_rules>
maybe we can work some with upstream on that, and keep pythondata stuff out of nixpkgs for now
<tpw_rules>
is my 2 cents thinking about this late at night
<Raito_Bezarius>
I think the biggest thing that drives me mad in litex
<Raito_Bezarius>
Is the integration tests intertwining
<Raito_Bezarius>
Like litedram depending on liteth depending on liteiclink depending on litescope depending on litedram
<Raito_Bezarius>
But yeah
<Raito_Bezarius>
Maybe the Python data stuff is just data also
<tpw_rules>
that might be why there's the wild-ass not checked and checked phases in nix-litex
<Raito_Bezarius>
Yes
<Raito_Bezarius>
I am pretty sure that's the case
<Raito_Bezarius>
I have a simple strategy to deal with it though
<Raito_Bezarius>
I just need to late bind the tests
<tpw_rules>
there are a couple iirc that shell out to wget
<Raito_Bezarius>
Didn't met them yet thankfully
<tpw_rules>
idk what that means
<Raito_Bezarius>
You use passthru.tests
<Raito_Bezarius>
To create a new test who can use the original drv and another dependency
<Raito_Bezarius>
To break the dependency loop
<Raito_Bezarius>
And run the integration test there
<Raito_Bezarius>
Because each phase are not their own drv, check phase doesn't have her the fully formed Python dep
<Raito_Bezarius>
But passthru.tests can do it
<tpw_rules>
that requires a bit of user intervention to run though
<Raito_Bezarius>
OfBorg will do it automatically
<Raito_Bezarius>
Which is what matters really
<tpw_rules>
ah, that's fair
<Raito_Bezarius>
@ wget
<Raito_Bezarius>
This is explaining some of my weird test failures
<Raito_Bezarius>
Some missing .v
<tpw_rules>
yeah it's kind of insane
<Raito_Bezarius>
Crazy stuff indeed...
<tpw_rules>
and sets my nix brain on fire. we need to work with upstream to fix it
<tpw_rules>
but i think leon has not had the time they wanted to work on nix-litex and coming up with a good story would be nice
<Raito_Bezarius>
Well LiteX is french
<Raito_Bezarius>
LiteX author *
<Raito_Bezarius>
I'm sure I can do smth
<tpw_rules>
are you as well?
<Raito_Bezarius>
Yes, I live in Paris
<tpw_rules>
oh, interesting
<Raito_Bezarius>
I probably need to reach out and measure a bit how the author is receptive to that
<tpw_rules>
i've talked to the author before, they're okay, just overworked lol
<Raito_Bezarius>
Hah :D
<Raito_Bezarius>
Can imagine
<tpw_rules>
i have already put through some patches for various bugs i found but did not try to fix stuff like that
<tpw_rules>
i've been putting my energy and hope toward amaranth instead
<tpw_rules>
but i'll put a few words on your PR at some point
jn has quit [Ping timeout: 256 seconds]
jn has joined #amaranth-lang
jn has joined #amaranth-lang
<whitequark[cis]>
<tpw_rules> "this isn't quite related but why..." <- I think this is actually an upstream Python requirement that other package managers are oddly lax about
<_whitenotifier-7>
[amaranth] github-merge-queue[bot] created branch gh-readonly-queue/main/pr-1108-18e5bcd6f72c0e95c9bc39ee04d25bdba2874532 - https://github.com/amaranth-lang/amaranth
<_whitenotifier-5>
[amaranth-lang/amaranth] wanda-phi 2d42d64 - tests: stop using implicit ports.
<_whitenotifier-5>
[amaranth-lang/amaranth-lang.github.io] github-merge-queue[bot] 279eb17 - Deploying to main from @ amaranth-lang/amaranth@2d42d649eeb180f23649e3ba72caf5bc54056d7e 🚀
<whitequark[cis]>
tpw_rules: with my Amaranth maintainer hat on, I like your abstraction because it's not going to break when things are changed internally
<whitequark[cis]>
tpw_rules: without that hat on, I'm not sure; afaict it introduces two conceptual operations, "get from pipeline" and "put into pipeline" (both "at time"), which is a little weird but feels fine to me
<whitequark[cis]>
it's more of a "conveyor" than a "pipeline" abstraction wise, right?
<whitequark[cis]>
like a thing that continuously moves where you have stations that can take and put things into it
<tpw_rules>
whitequark[cis]: i had thought about conveyor but wasn't sure if it was a common concept at all
<tpw_rules>
why would you call those operations weird? because there are two? it doesn't jive with the name?
<whitequark[cis]>
"put into the pipeline" isn't how people normally talk about pipelins
<whitequark[cis]>
s/pipelins/pipelines/
<tpw_rules>
i'll probably rename it to conveyor, i think you're right that naming it after pipelines isn't a favor
<cr1901>
Prob won't be here for the meeting; #43, #47 look fine. #44 looks fine, but am definitely against the alternative; I think m.Initial() is the way to go. m.Once() is fine as well and I kinda prefer it.
<whitequark[cis]>
you do need to be here for the meeting if you have strong opinions on #44
<whitequark[cis]>
we'll have to think about the implications of going with one or the other and I'm leaning towards m.initial += so far
<whitequark[cis]>
well, we'll probably have to postpone it if you'll be absent, though we may or may not discuss it anyhow. if there's a good technical reason to not go for m.initial += then that rules it out
<galibert[m]>
William D. Jones: what would you think about m.f.initial with m.f for all formal domain statements?
<galibert[m]>
You could have always and others too
<galibert[m]>
Note that the suggestion is for wq too obviously
<whitequark[cis]>
Assert isn't a formal statement anymore
<whitequark[cis]>
also m.d vs m.f are super hard to distinguish at a glance, much less if you have, say, dyxlexia
<cr1901>
I've typed and cleared my response several times, and I think re: #44, "I'll get over it", if m.initial is decided. It should not be blocked on me.
zyp[m] has joined #amaranth-lang
<zyp[m]>
I don't really understand formal verification well enough to have a qualified opinion, but the way I see it, the question boils down to what makes most sense of nesting control flow inside an initial block or nesting initial blocks inside control flow
<whitequark[cis]>
cr1901: I mean, the purpose of meetings is not to get everyone to compromise, it is to make a better language
<whitequark[cis]>
so you approaching it from this way kind of ignores the purpose of meetings
<whitequark[cis]>
we should encourage objections, because this challenges us to produce a better design
<whitequark[cis]>
but for this a dialogue needs to happen, not just "I dislike option A and I won't be at the meeting to explain why"
<cr1901>
zyp[m] got to the crux of the issue of me. I don't find "nesting initial blocks inside control flow" intuitive, even though nesting m.initial inside control flow would beparity w/ clock domains, and I'm having trouble expressing why I feel that initial is different from clock domains.
<galibert[m]>
I kinda dislike it too, the reason being I don’t see why that random initial thing deserves to be at top level of Module by itself, afaict nothing else that isn’t quite fundamental is
<cr1901>
And since I'm definitely not at 100% capacity (or even 50%), I'm not sure I _will_ come up with a better reason than "it doesn't feel right/intuitive to me"
<galibert[m]>
submodules and domain are fundamental, special-case formal statements not so much
<cr1901>
especially not within an hour thirty
<cr1901>
The meeting's in 30 minutes, I'll stick around
<Wanda[cis]>
essentially it's fundamental because initial behaves like another special domain
<Wanda[cis]>
"sync" is evaluated whenever a clock signal goes up; "comb" is evaluated at all times; "initial" is evaluated exactly once
<Wanda[cis]>
it's also not strictly just for formal: the RFC mentions we will probably want initial Print, as soon as Print lands
<galibert[m]>
sync and comb are in m.d, not m
<zyp[m]>
another alternative would be m.d.initial
<Wanda[cis]>
it's motivated by formal because that's the part that currently exists in the language
<zyp[m]>
as long as nobody wants to name an actual clock domain initial
<Wanda[cis]>
I like m.d.initial, though it does come with a compat break that would be ugly to handle
<cr1901>
>as you can still nest with m.Initial(): in with m.If(): Oh... you can have _both_ "nesting control flow inside an initial block" or "nesting initial blocks inside control flow" with m.Initial().
notgull has joined #amaranth-lang
notgull has quit [Ping timeout: 264 seconds]
<galibert[m]>
What are the semantics of the interaction with m.If and do we really want/need them given we have python-level if?
<Wanda[cis]>
very much yes, for the same reason that m.If exists in the first place
<galibert[m]>
Not following
<Wanda[cis]>
well you need it to branch on a signal instead of a Python-level value?
<galibert[m]>
You’re not going to change the initial conditions at some point in the future
<Wanda[cis]>
but the initial conditions can be determined only at runtime
<Wanda[cis]>
consider the case of using initial Assume to make sure initial state is consistent
<whitequark[cis]>
good evening. it is the time for our weekly Amaranth meeting
<galibert[m]>
Really not following there
<tpw_rules>
hello
jfng[m] has joined #amaranth-lang
<jfng[m]>
<Wanda[cis]> "I like m.d.initial, though..." <- aesthetically, `m.d.once` would uses the same amount of characters `m.d.comb` or `sync`
<jfng[m]>
o/
Chips4MakersakaS has joined #amaranth-lang
<Chips4MakersakaS>
hi
<cr1901>
I imagine you're going to wanna do #44 last
<zyp[m]>
I'm here in a minute
<whitequark[cis]>
I don't think we should be reserving any names in the domains
<whitequark[cis]>
for the agenda, I will start with the issues that are needed for the reference documentation project I'm been working on, and then we can move on to the rest
<Wanda[cis]>
meow.
<cr1901>
I'm here
<whitequark[cis]>
so... Wanda zyp cr1901 galibert tpw_rules jfng Chips4Makers (aka Staf Verhaegen), is that all?
<whitequark[cis]>
in RFC #27, I've deprecated add_process in favor of add_sync_process (and banned yield Tick() within the latter), because I incorrectly assumed that the latter will handle all of the needs for replacing registers with logic that arise
<whitequark[cis]>
there are two problems with it. first, yield (with no arguments) isn't really compatible with the new async interface, and things like wrappers for getting ValueCastable's proper values in simulation will be exclusively using the async interface, as it's burdensome to have two
<whitequark[cis]>
second, it doesn't cover all use cases for replacing registers, as a DDR register isn't representable using one add_sync_process with only yield
<whitequark[cis]>
you could represent it with two add_sync_process and one add_comb_process (which doesn't even exist now) to mux between them, but that's honestly just a worse solution in almost every way
<galibert[m]>
Now that version is a lot more convincing than #27 ever was. One way for testbench, one way for HLE, since they need different properties, that makes a lot of sense
<galibert[m]>
I'm sorry I didn't see that then
<whitequark[cis]>
np, it is a pretty confusing topic. I actually did have that wording in RFC 27 originally
<whitequark[cis]>
well when it was merged
<whitequark[cis]>
There are two main simulator modalities: add_testbench and add_sync_process. They have completely disjoint purposes:
<whitequark[cis]>
add_testbench is used for testing logic (asynchronous or synchronous). It is not used for behavioral replacement of synchronous logic.
<whitequark[cis]>
add_sync_process is used for behavioral replacement of synchronous logic. It is not for testing logic (except for legacy code), and a deprecation warning is shown when yield Settle() is executed in such a process.
<whitequark[cis]>
anyway. please respond with your comments or proposed disposition: merge or close
<zyp[m]>
merge
<cr1901>
merge
<galibert[m]>
bikeshedding: add_simulation?
<galibert[m]>
to make it darn obvious?
<galibert[m]>
merge in any case
<whitequark[cis]>
add_process already exists so we'd have to deprecate it
<whitequark[cis]>
we can do it later
<jfng[m]>
merge
<galibert[m]>
well it will point to code as being legacy
<whitequark[cis]>
I think just about no one is using it right now
<whitequark[cis]>
maybe you? most people don't do the kind of designs you do
<whitequark[cis]>
right now we have the notion of "signal reset values" which make no sense for comb signals which are never reset, but where the value is used initially. we also have a notion of memory init values. I propose making what the docs call "signal initial value" into `Signal(init=)`, and deprecating `Signal(reset=)`, with a wider cycle than usual
<whitequark[cis]>
this is a fairly invasive change, but I think we should do it earlier rather than later, and I think this is a major improvement for comprehension for newcomers to the language, which may otherwise easily assume that every `Signal` is a register, or something
<jfng[m]>
merge, and happy about it
<cr1901>
merge
<galibert[m]>
merge
<zyp[m]>
merge
<whitequark[cis]>
as for the deprecation timeline, I'm thinking time-based makes sense in this case: e.g. we remove it in 2026
<galibert[m]>
find/replace will take care of any issues
<whitequark[cis]>
yeh
<Wanda[cis]>
merge
<whitequark[cis]>
mainly relevant for maintained or sparsely-maintained code like minerva
<whitequark[cis]>
s/maintained/unmaintained/
<jfng[m]>
does this really need a special deprecation timeline ? e.g. a different one than the removal of Record ?
<whitequark[cis]>
I'm not sure
<Chips4MakersakaS>
merge
<whitequark[cis]>
we could do it two versions ahead instead of one ahead, but I'm concerned about unmaintained code
<galibert[m]>
Yeah, I also don't think the long deprecation is needed given how trivial the fix is
<whitequark[cis]>
in any case, we can decide on the deprecation timeline two versions from now, and not on this meeting
<Wanda[cis]>
Record had a long deprecation timeline too, for similar reasons
<whitequark[cis]>
right now, nothing prevents code to reach into the innards of AST nodes and modify them, because they're just normal attributes
<galibert[m]>
merge with a remark: immutable may make people (like me!) think you can't .eq a Signal
<whitequark[cis]>
we should either document that as legal, or forbid it
<whitequark[cis]>
oh, it won't be documented as just "immutable"
<galibert[m]>
so it needs to be very clear what immutable means in that context
<whitequark[cis]>
the docs will be way more specific; the issue is for our own discussion
<cr1901>
I've mutated sig.reset/sig.reset_less before. But doesn't appear to be in any code recently
<galibert[m]>
forbid, forbid, forbid
<cr1901>
So merge
<whitequark[cis]>
there's an additional issue with mutating in that lots of nodes do some sort of internal bookkeeping, especially Signal with all the value-castable stuff, and mutating will break it
<whitequark[cis]>
like casting reset values and such
<whitequark[cis]>
so if we go with mutable .reset we have to add a lot of code to handle this case
<Chips4MakersakaS>
also vote for immutable
<galibert[m]>
there would also be the question of until when things like .width are mutable, and there's no good answer
<jfng[m]>
merge (iirc, times where i did this was for quick&dirty workarounds to Record limitations)
<whitequark[cis]>
well ideally a Signal would actually have a .shape, not just a .width
<Chips4MakersakaS>
reset could be made mutable later it good use case pops up
<whitequark[cis]>
and the shape would return a proper shape-castable if that was used to create a signal
<Chips4MakersakaS>
*if
<whitequark[cis]>
and the reset value you can access will be properly cast, etc
<zyp[m]>
that'll interact a bit weirdly with RFC 15
<zyp[m]>
but that's off topic for now :)
<jfng[m]>
what is a use-case for mutating .reset ?
<whitequark[cis]>
maybe you change your mind later
<cr1901>
jfng[m]: I don't remember why I mutated reset, just that I've done it before
<whitequark[cis]>
so with m.FSM() actually creates internally an FSM state signal and then mutates its width, which may be difficult to work around
<whitequark[cis]>
but that's the only case I know where it's not trivial to fix
<zyp[m]>
I could argue that since we've already made signatures immutable, it follows that signals created from signatures should be
<Wanda[cis]>
it's... nontrivial enough that we actually considered adding a special late-bound statement to work around the problems
<whitequark[cis]>
yeah, we'll have to resolve that before we properly make Signal attributes immutable
<whitequark[cis]>
however m.FSM() is magic and can afford to continue being magic, we make no guarantees otherwise
<whitequark[cis]>
so it's not super relevant
<whitequark[cis]>
Wanda: your vote?
<Wanda[cis]>
I vote for immutability; we'll resolve the FSM issue one way or another
<whitequark[cis]>
resolution on 1067: make the entire Value hierarchy immutable after creation
<whitequark[cis]>
which we've been discussing before the meeting
<whitequark[cis]>
for context, I've been working on Assert and Assume in Python simulation and CXXRTL simulation, and once it gains a format string (for which groundwork has been laid already, in Yosys) it can become an extremely useful tool
<whitequark[cis]>
the idea is that at least Assert will graduate to be a part of the prelude together with Print, and a designer will be expected to heavily annotate invariants in their code with these statements
<whitequark[cis]>
this should significantly improve reliability of reusable code, and also make eventual transition to formal verification easier for those who choose it
<tpw_rules>
whitequark[cis]: hi, i'm sorry, i got pulled away without notifying you. i'll keep the meeting structure in mind in the future
<whitequark[cis]>
we currently have Assert, Assume, Cover, and Initial (as well as AnyConst and AnySeq, which should probably be re-engineered) under the amaranth.asserts umbrella, which is basically a list of things I didn't want to stabilize or advertise because of doubt about the design
<whitequark[cis]>
and Initial in particular cannot possibly make it since it's a yosys-specific hack
<galibert[m]>
because it's yosys-specific or because it's a hack?
<whitequark[cis]>
both!
<Wanda[cis]>
both
<whitequark[cis]>
in fact, the new implementation of Assert and Assume (and Cover) in yosys, the $check cell, doesn't even use $initstate
<whitequark[cis]>
so we can't migrate to the $check cell (which we need to, in order to gain formatting capability) without dealing with Initial somehow
<tpw_rules>
whitequark[cis]: (disposition on #47 is that i don't have enough background and am ambivalent, disposition on #43 is merge, #1067 is immutable)
<whitequark[cis]>
this is a bit of priority inversion on the meta-level; in itself Initial isn't hugely important but it's blocking very important work
<whitequark[cis]>
and I think we should deal with this ASAP
<galibert[m]>
ok, can you clarify what Initial is really supposed to be?
<whitequark[cis]>
tpw_rules: thank you
<Wanda[cis]>
so. I think initial is essentially a funny domain, and should behave as a domain
<Wanda[cis]>
ie. m.d.initial; if this is not feasible because we don't want special domain names (reasonable), I'd vote for going for the next closest syntax, m.initial +=
<tpw_rules>
what can `x` be in the RFC example? does it just check the `reset/init` field of that signal?
<whitequark[cis]>
galibert: when you use formal verification, you need to specify initial conditions, otherwise the SAT solver will come up with some invalid and impossible initial state which violates your design assumptions, or otherwise do things you don't care about
<zyp[m]>
my unqualified opinion is that m.d.initial, possibly with a different name, would be the most consistent solution
<whitequark[cis]>
tpw_rules: `x` is any expression
<jfng[m]>
the `with m.Initial()` syntax will increase rightward drift when chained with other control-flow statements
<galibert[m]>
Catherine: outside of uninitialized sram, doesn't every value in amaranth have a defined reset value?
<Wanda[cis]>
galibert: to return to the question you asked before the meeting interrupted, the reason you need `m.If` is because of what `Assume` does
<cr1901>
I don't really see it as a domain, because it nominally "stops existing" in a way that comb and sync domains don't. I think control flow enclosing initial is unintuitive in a way that control flow enclosing other domains are not.
<tpw_rules>
that is my other question
<zyp[m]>
galibert[m]: not inputs
<Wanda[cis]>
the FV tool essentially creates a starting universe for every possible set of values for all AnyConst and inputs, which don't have initial values assigned by amaranth by design
<galibert[m]>
Wanda: and what is assume doing?
<Wanda[cis]>
and the initial Assume is executed in each of the universes, and removes from consideration the universes in which it fails
<whitequark[cis]>
cr1901: the way `$check` cell is implemented internally is that it has a condition (the tree of `if`s ANDed together, in Amaranth, basically) and a trigger. the trigger can be "any inputs", "this clock", or "initial conditions"
<whitequark[cis]>
cr1901: although an implementation detail, I find this a useful way to think about the problem
<Chips4MakersakaS>
Maybe you could make it a domain that is not specific for formal ? Only when Assume is used it has special formal meaning.
<Chips4MakersakaS>
E.g `s = Signal(init=1)` would become `s = Signal(); m.d.initial += s.eq(1)`
<Wanda[cis]>
once again, it's not just for formal
<Wanda[cis]>
there will also be initial Prints
<whitequark[cis]>
cr1901: in our case, m.d.comb specifies a trigger, and m.d.sync specifies a trigger, so m.initial specifying a trigger also makes sense
<tpw_rules>
maybe i'm thinking too concretely, but if you have some block of logic with an input, the input would just be the initial value right?
<whitequark[cis]>
Chips4Makers (aka Staf Verhaegen): negative on allowing `eq` in initial, since this means arriving at the reset state may take an unbounded amount of work
<cr1901>
whitequark[cis]: I don't know much about the $check cell, but that clarifies things
<whitequark[cis]>
cr1901: well yeah it was just introduced
<cr1901>
Ahhh
catlosgay[m] has joined #amaranth-lang
<catlosgay[m]>
Wanda: I would argue that it is better to have a continuous assumption to constrain `AnyConst` than using initial, as formal tools based on induction (all but BMC) dont get to see that constraint in the inductive case otherwise. See https://github.com/YosysHQ/yosys/issues/3378 for an example of this type of issue i had ages ago
<galibert[m]>
Wanda: what if the Assume invalidates the If?
<Chips4MakersakaS>
Then I would not like to have the name of the domain be initial
<tpw_rules>
do you specifically tag your design inputs?
<whitequark[cis]>
galibert: that's just like writing `Assume(0)`
<Wanda[cis]>
galibert[m]: what does this mean? failing Assume destroys the current universe; if it's unreachable due to the if condition, then *shrug*
<whitequark[cis]>
Chips4Makers (aka Staf Verhaegen): justify that please?
<tpw_rules>
it does seem slightly weird that the initial construct/domain could not be used to set signal init values
<galibert[m]>
with m.If(some_input): m.initial += Assume(some_input == 0)
<whitequark[cis]>
catlos.gay: are you in effect suggesting we just not have `Initial` at all?
<zyp[m]>
tpw_rules: we just decided that reset/init values should be immutable
<Wanda[cis]>
galibert[m]: then the Assume just always fails when some_input isn't 0.
<tpw_rules>
zyp[m]: then Chips4MakersakaS's statement is meaningless as i interpret it
<Chips4MakersakaS>
For me the initial domain would mean that I can set values to a certain value; likely poisoned by Verilog.
<catlosgay[m]>
Apologies if im missing something, but does anyone here have a concrete example of where initial is helpful in formal? The only things I tend to find need to be special cased initially (other than things that already come from the reset values in the design) and disabling properties for the first N cycles until they make sense. This can be done with a standard counter or shift register type thing with reset
<galibert[m]>
zyp: that would be a way to have different POR-reset and domain-reset values
<_whitenotifier-5>
[amaranth-lang/rfcs] whitequark 14fade5 - RFC #27: Amend to deprecate `add_sync_process` rather than `add_process`.
<_whitenotifier-7>
[amaranth-lang/rfcs] whitequark 88bd8b9 - #47: Amend RFC #27 to deprecate `add_sync_process` rather than `add_process`
<_whitenotifier-5>
[amaranth-lang/amaranth-lang.github.io] whitequark db6beec - Deploying to main from @ amaranth-lang/rfcs@88bd8b9b5afbf146cb7f89e118cde33398ea72d7 🚀
<catlosgay[m]>
ahh yeah this gets into a slight limitation of the yosys based formal tools i think. with commercial tools, you explicitly specify a reset signal, but with yosys this isnt super easy, so its often easiest to add an initial block that assumes reset at the start or something. I would err towards avoiding initial for formal tbh, but there are probably some uses (such as designs without resets maybe? or confusing resets when there
<catlosgay[m]>
are mutiple clock domains?)
<tpw_rules>
don't we already have the init value for the resets?
<tpw_rules>
i guess there are easily situations where you would want those to be different
<whitequark[cis]>
catlos.gay: this points me to a solution: some way to mark a domain as "formal domain" I suppose, where multiclock transformations normally done by Yosys wouldn't be applied
<catlosgay[m]>
cr1901: I would write that with the assumptions guarded by coming out of reset. So you can have something like a register first_cycle that is reset to 1, and then assigned 0 in any other cycle. You then use that as the precondition for the assumptions
<whitequark[cis]>
and where the clock is the SMT clock
<whitequark[cis]>
so you would have m.d.formal += and you could write whatever you want there, including driving other domains as you see fit
<cr1901>
catlosgay[m]: I've only ever used yosys based formal tools, so everything I say should be viewed through that lens
<catlosgay[m]>
Catherine: yeah that has some use (and not much analogue in verilog, there is $global_clock? but I dont think I've ever seen it used)
<catlosgay[m]>
I can't provide much experience on multiclock designs unfortunately, my experience is mainly with things with a single clock domain
<cr1901>
This is the age-old "guarantee forward progress" check.
<whitequark[cis]>
catlos.gay: what about induction? what happens with interior registers in some design when the formal checker wants to fill it with garbage that can't be reached from any valid state and you try to avoid that?
<catlosgay[m]>
cr1901: multiclock in sby (and whatever the equivalent pass is in yosys, i forget) should be able to do this kind of transformation for you automatically, without you having to write that manually
<catlosgay[m]>
cr1901: I should add that things with negedge are way outside my wheelhouse too, modern asic stuff i have worked with tends to all be fairly clean single clock domain (but with clock gating), everything on posedge and shared async reset
<cr1901>
And no it doesn't do that transformation. If I don't include that line, during induction, the solver will happily fail any induction length by just holding the design in a single state for "n-1" steps
<catlosgay[m]>
cr1901: ahh ok, this is slightly away from any point im trying to make, as I say, im sure there is some use for this stuff, but i dont think its particularly standard
<Wanda[cis]>
(I'll be looking away from the machine for a while; please ping me when we're reaching a vote or something)
<whitequark[cis]>
I think I'm going to withdraw my RFC from a vote since I no longer think this is the right way forward
<whitequark[cis]>
I think we should simply break Assert/etc with the $check refactor and then fix Yosys tools to do formal in a better way
<Wanda[cis]>
(also my vote is almost certainly going to be: merge, m.initial += syntax, same non-guarantee of stability as current Initial)
<whitequark[cis]>
and for the time being Initial remains supported, with the understanding that we eventually rip it out with no replacement
<Wanda[cis]>
huh.
<catlosgay[m]>
Catherine: (about induction) yes this is an issue in proof convergence. If you know those states for those registers cant be reached, you should write an assertion that checks this. The presence of this assertion helps make the design more inductive and can help other properties prove faster
<Wanda[cis]>
that... works too
<whitequark[cis]>
we may polyfill some of the necessary logic in an Amaranth formal platform or something
<whitequark[cis]>
but from what catlos.gay has said, it seems like the only real reason `Initial` exists is immaturity of Yosys formal tools
<whitequark[cis]>
I'm not too surprised by this, and I think we shouldn't do churn chasing tools which aren't good enough for us
<whitequark[cis]>
we should fix the tools instead
<catlosgay[m]>
I havent looked at how setting up resets works in yosys lately, it may have improved, but i remember finding it confusing in the past (and how to do things depends on async vs sync reset etc iirc)
<catlosgay[m]>
which is why initial can be very useful for that (and ive used it in verilog stuff with yosys for this purpose)
<catlosgay[m]>
but when I use commercial tools, I don't use initial, preferring to gate things based on the reset signal instead
<cr1901>
catlosgay[m]: Ack re: nonstandard. By the time I learned formal I didn't have access to commercial tools
<cr1901>
(and haven't been exceptionally interested in forking out $ for them.)
<whitequark[cis]>
I think Amaranth should probably not encourage the use of sby and should probably provide a formal platform that actually makes sense and is easy to use without reading fifty blog posts of some well known transphobic zealot
<tpw_rules>
(yes)
<cr1901>
Heh
<Chips4MakersakaS>
A more widely feeling of me. What I liked about Amaranth is that all the base functionality was synthesizable; simulation is something on top at a higher level. You don't have the distinction like synthesizable/non-synthesizable VHDL/Verilog. Formal support seems to break that at the moment.
<Chips4MakersakaS>
I am not well versed in formal to know if this can be avoided.
<whitequark[cis]>
Chips4Makers (aka Staf Verhaegen): we are actually bringing formal and synthesizable closer together
<whitequark[cis]>
CXXRTL is a synthesis engine and it fully supports Assert/Assume/Cover
<whitequark[cis]>
(well it doesn't do anything for Cover)
<whitequark[cis]>
* for Cover, by default)
<cr1901>
catlosgay[m]: By "make the design more inductive", do you mean "low k can be rejected more quickly b/c of the extra asserts"?
<whitequark[cis]>
Chips4Makers (aka Staf Verhaegen): I agree with that this general direction is desirable, and my choice to withdraw the RFC is actually partly influenced by that
<catlosgay[m]>
cr1901: for k-induction yes. to be able to use a lower k, you need to block out any possible counterexamples for a higher k. if this assert blocks those counterexamples, the k you need is decreased. but you could need multiple such asserts to reduce k at all. for IC3 it helps more generally
<zyp[m]>
what's a good resource to learn formal?
<Chips4MakersakaS>
OK, and I think you could even make a debug on FPGA that checks the asserts. I do see it as debugging. But Assert's themselves can just be asserts and necessary need to be proven.
<Chips4MakersakaS>
*debug build
<Chips4MakersakaS>
necessary -> don't necessarily
<catlosgay[m]>
cr1901: in a bit I could share some thoughts/diagrams ive made about trying to get at the core of what makes model checking problems hard and how to improve the performance
<cr1901>
catlosgay[m]: Feel free to leave them at your leisure.
<whitequark[cis]>
this concludes the meeting. thanks everyone, we've had a very productive one today, and see you all in a week
<cr1901>
But also, I was under the impression that you can't lower k and make induction pass. All you can do is raise k and hope that the garbage states aren't reachable on an arbitrary "kth" step.
<cr1901>
(At least, this was my technique for solving failing "k" in a design where "k is failing, but I know this state wouldn't actually be reachable from reset after looking at the VCDs"
<cr1901>
e.g. "if you increase the induction length, and k-induction starts passing, that means the states in which k-induction failed for lower k aren't actually reachable and were just a side-effect of the SMT solver filling registers with garbage"
<cr1901>
/minddump
<cr1901>
TLDR: I don't know how to make k-induction pass by lowering k, only increasing it :P
<_whitenotifier-5>
[amaranth-lang/amaranth-lang.github.io] whitequark 0093473 - Deploying to main from @ amaranth-lang/rfcs@b31896d1ef3137f9115615e0d22b056ac0f40f5d 🚀
<_whitenotifier-7>
[amaranth] github-merge-queue[bot] created branch gh-readonly-queue/main/pr-1093-2d42d649eeb180f23649e3ba72caf5bc54056d7e - https://github.com/amaranth-lang/amaranth
<catlosgay[m]>
cr1901: indeed, you cant make failing k-induction pass by lowering k without changing the property, but you can "strengthen" the property with another assertion that reduces the k needed to prove the property
<_whitenotifier-5>
[amaranth-lang/amaranth-lang.github.io] github-merge-queue[bot] d73ab7d - Deploying to main from @ amaranth-lang/amaranth@4014f6429c97be16d0c0c8b944e3b85437bd0583 🚀
<tpw_rules>
whitequark[cis]: i'm strongly considering licensing the whole project as GPLv3+. however, i think there are components that could be extracted and contributed to amaranth or other libraries in some form. if i relicensed those components to BSD at a later date, do you foresee significant difficulty/reluctance to accept such contributions?
<whitequark[cis]>
as long as you submit then yourself and do the Signed-off-by dance, I see no reason to be concerned
<tpw_rules>
okay, thanks
<galibert[m]>
it's for fixed-timing conveyers with no interlock?
<tpw_rules>
yes, i had given a bit of thought to enables/interlocks but not enough to concretize it
<tpw_rules>
(not that those are the same thing)
<galibert[m]>
seems useful anyway
<tpw_rules>
i had also thought a bit about turning it into a context manager, or putting such a thing on top, but every time i've tried similar previously it's justifiably upset wq :)
<galibert[m]>
Don't upset wq please, she doesn't need that :-P
<galibert[m]>
The signals passed into the constructor are put() at time 0?
<tpw_rules>
yes
<tpw_rules>
just as a shortcut. you can even use negative times if you really wanted
<galibert[m]>
it's kind of a delay line, in fact
<galibert[m]>
Yeah, I really see potential there
<tpw_rules>
i had googled "amaranth pipeline" to get inspiration from the community and found https://gist.github.com/jrmoserbaltimore/226e71825e80e351a1dd0b73f08cb506, idk who they are or if they hang around here or what the plan is for that concept, but i think my thing could underpin that without needing to modify the language
<tpw_rules>
chiefly to make the API less weird looking
<tpw_rules>
(not that i would exactly take theirs, i think it would need rework)
<tpw_rules>
i.e. minimal and straightforward changes if you need to shuffle things around for timing
<tpw_rules>
is it possible for the new IR and relocation of Memory to be able to generate less horrible memory init sequences
<galibert[m]>
isn't the horribleness an intrinsic verilog property?
<tpw_rules>
various toolchains support various external methods, i thought doing it the bad way was an artifact of pumping everything through yosys and how that was done
<galibert[m]>
iirc quartus only supports the external mif files on Instance of altsyncram
<tpw_rules>
i don't think so, you only would really have it be 2 deep and i assume the intention is to not have 5 multipliers so you couldn't hook the same multiplier to 5 different signals without a big state machine anyway
<tpw_rules>
(sorry, six)
<tpw_rules>
for my money i would make arrays of the three multiplier inputs and output signal and use a for loop to index them and generate the state machine
<tpw_rules>
it feels ever so slightly dirty but interlacing for and with like that is really powerful and part of why amaranth is so good
<galibert[m]>
I use a for/with Matching interlacing to write an address decoder for a ram made of multiple blocks, it's just perfect
<tpw_rules>
yes, you could also use an if statement or case statement (with an external counter) instead of a state machine if you like
<zyp[m]>
yeah, I'm doing stuff like that elsewhere
<tpw_rules>
if it turned out you wanted to give the thing more latency, i think introducing a SignalConveyor would help
<tpw_rules>
zyp[m]: incidentally, i'd be interesting in using your fixed-width stuff once it lands
<whitequark[cis]>
Wanda: oh, right, we can remove the "Do not rely on the behavior of a with m.Case(): with no patterns." bit from the docs
<whitequark[cis]>
want to take care of it? I feel like I'm ever so likely to forget something important if I do it
<whitequark[cis]>
tpw_rules: re memory init, we have not been able to get a consensus on exactly how to represent this in Yosys and also Yosys actually wants to be able to peek into memories sometimes, which is something that'll have to be taken care of
<Wanda[cis]>
meow?
<Wanda[cis]>
uh
<Wanda[cis]>
hold on
<Wanda[cis]>
I'll try to initialize a valid Wanda and get back to you
<tpw_rules>
whitequark[cis]: i guess that example is essentially to build a table rather than use a multiplier
<tpw_rules>
took a bit of digesting to understand the motivation, but it's good to know it's called out
<tpw_rules>
also yeah i had kind of expected that, re. peeking. i know you had talked earlier that the communication mechanism currently can only use one file
<whitequark[cis]>
no, zero files
<whitequark[cis]>
it uses stdin/stdout
<tpw_rules>
yes, that's what i understood. just meant you can't separate two files using that, unless someone designed a higher level protocol
<whitequark[cis]>
yes
<whitequark[cis]>
re: example, I just came up with whatever I had in mind at the time that's self-contained
<whitequark[cis]>
it's surprisingly difficult to write good examples when you can't assume any particular knowledge
<tpw_rules>
i've tamed quartus enough for my purposes anyway and it does what i want, i just feel bad for it sometimes having to digest megabytes of junk
<tpw_rules>
(turns out the secret afaict is your memory has to be a power of two size)
<whitequark[cis]>
wtf
<whitequark[cis]>
it's quadratic unless the memory is POT?
<tpw_rules>
idk about quadratic, but it won't infer/use the memory init values else
<tpw_rules>
(not sure if the presence of init data has anything to do with the problem)
<whitequark[cis]>
it just ignores them???
<whitequark[cis]>
what the fuck is wrong with vendor toolchains
<Wanda[cis]>
<whitequark[cis]> "want to take care of it? I..." <- okay, yeah, sure, added on top of th elist
<whitequark[cis]>
Wanda: thank you
<tpw_rules>
i don't think it ignores them, but it for sure stops BRAM inference. idk if it will successfully infer a non-power-of-two BRAM if you don't have an initial block is what i am trying to say
<Wanda[cis]>
tpw_rules: what the fuck
<whitequark[cis]>
tpw_rules: I don't feel bad for Quartus digesting megabytes of junk because Quartus is bad and should feel bad
<tpw_rules>
but some people had been saying that quartus gets unhappy with initial values and maybe that's what they encountered
<whitequark[cis]>
the worst toolchain I've used, probably
<tpw_rules>
idk i hate installing vivado more
<whitequark[cis]>
they're like, the same order of magnitude in size
<whitequark[cis]>
but also how often do you install Vivado? I think I still use most of my testing using Vivado 2017.something
<whitequark[cis]>
which I've had since 2017
<Wanda[cis]>
... like twice a year for me
<whitequark[cis]>
ancestral vivado installation, passed from mother to daughter
<tpw_rules>
oh that explains it, the latest ones are up over 100GB
<Wanda[cis]>
maybe more
<tpw_rules>
5x larger than 2017
<whitequark[cis]>
well yes, I know, but isn't Quartus 20GB?
<whitequark[cis]>
(I think if you just install Vivado and not the whole Vitis suite it's more like 60GB)
<whitequark[cis]>
at that point it's kind of ... pour yourself some tea and go watch a video
<whitequark[cis]>
like, either way
<tpw_rules>
i need to get back into vivado wrangling at some point, i bought myself a kria board
<whitequark[cis]>
Vivado has its flaws, but at least it doesn't make my blood pressure go up every time I hear its name because I know it's going to be followed up by some incomprehensible dogshit behavior I then have to slowly find a workaround for over months
* whitequark[cis]
really dislikes Quartus
<tpw_rules>
sorry
<whitequark[cis]>
you're fine
<tpw_rules>
i genuinely appreciate that amaranth deals with it and tries to hide it
<whitequark[cis]>
I have a problem with Quartus, not with people using Quartus
<whitequark[cis]>
and my dislike of it is directly proportional to the effort required to support it that had to be spent for basically no reason other than Quartus being weird
<tpw_rules>
yeah my message is "that support is worthwhile and enjoyed"
<whitequark[cis]>
there's just so many things that Quartus does that nothing else has a problem with
<whitequark[cis]>
thank you
<tpw_rules>
not that you have a problem with me
<Wanda[cis]>
whitequark[cis]: I mean, you have to be present to press "retry" every time the downloader craps itself
<whitequark[cis]>
"say "megafunction" one more time! I dare you! I double dare you! <etc>"
<whitequark[cis]>
Wanda: oh, I just get the latest full archive from my headmate's NAS
<Wanda[cis]>
oh.
<Wanda[cis]>
yeah
<Wanda[cis]>
I suppose that works
<whitequark[cis]>
I still have to unpack it, which probably exhausts my disk space, but then I just clear an Android build tree
<tpw_rules>
my favorite part is that it's 100GB and extracts to 100.1GB bc it's just a gzip of gzips
<Wanda[cis]>
heh
<Wanda[cis]>
yeah
<Wanda[cis]>
but that's at least normal vendor brain, not intel vendor brain
<Wanda[cis]>
like... I haven't really used quartus in 12 years, but every time I hear about it, it's invariably something completely batshit
<Wanda[cis]>
... I should look into reversing quartus as a form of self-harm
<whitequark[cis]>
normal statements
<tpw_rules>
to me xilinx enjoyers are the weirdoes
<whitequark[cis]>
hm, so I didn't like Vivado either but then I watched my headmate (at a previous workplace) use the Vivado GUI to be extremely effective at all sorts of tasks
<whitequark[cis]>
she even wrote a custom synthesis pass entirely in Tcl
<whitequark[cis]>
and this has made me realize I was holding it wrong the whole time, and now I think it's a very useful and powerful tool that's actually pretty cleverly designed and with many good choices
<tpw_rules>
what was wrong? not using the GUI?
<whitequark[cis]>
of all the vendor toolchains, I think Vivado is probably the best one, from a purely technical perspective (and leaving aside how long you have to stare at the progress bars all the time)
<whitequark[cis]>
no, not related to the GUI. the GUI is mostly just driving the Tcl core
<whitequark[cis]>
I, hm
<whitequark[cis]>
I didn't vibe with it and now I befriended it and I do?
<tpw_rules>
oh. yeah my interactions with that part of quartus have not been lovely
<whitequark[cis]>
does that make any sense to you.
<whitequark[cis]>
"is she... friend of Vivado, you know?"
<tpw_rules>
i mean that's fair, you gotta learn its way
<Wanda[cis]>
lol
<whitequark[cis]>
lots of people just stop thinking whenever they see a 2-megabyte log file
<whitequark[cis]>
but if you don't stop thinking and actually read what it says, it becomes very comprehensible and useful
<whitequark[cis]>
even with Verilog
* tpw_rules
knows the quartus message IDs by heart pratically
<whitequark[cis]>
oof
<Wanda[cis]>
I'm sorry
<tpw_rules>
Design uses memory blocks. Violating memory block timing may
<Wanda[cis]>
I should RE the ancient altera CPLDs
* whitequark[cis]
shudders
<Wanda[cis]>
to add to my collection of reversed CPLDs
<Wanda[cis]>
then it'll be not just self-harm, but pointless self-harm, the best kind
<tpw_rules>
idk, i may become a vivado enjoyer. might be too nix-brained
<Wanda[cis]>
how does nix relate to all this?
<tpw_rules>
that's part of why i dislike the enormous disk size, it stresses nix out
<whitequark[cis]>
huh
<tpw_rules>
but that's been improving
<zyp[m]>
in the middle of the chip shortage I had a task at work replacing an ancient altera CPLD in an old project with something that was still obtainable, the code for it was written in AHDL
<whitequark[cis]>
zyp: I was waiting for someone to bring up AHDL
<whitequark[cis]>
I think AHDL is actually not that bad
<Wanda[cis]>
hmmm
<zyp[m]>
probably not, apart from the lack of modern tools that can handle it
<Wanda[cis]>
I should look into it
<Wanda[cis]>
all I know about it is that it exists
<zyp[m]>
I ended up rewriting it in verilog and sticking it into a machxo-256
<galibert[m]>
Wanda: just go and RE the original cyclone, a number of cave games uses one as a blitter:-)
<Wanda[cis]>
maybe some day
<Wanda[cis]>
that would definitely be massive self-harm
<galibert[m]>
Indeed
<whitequark[cis]>
>>> C(1, signed(1)).value
<whitequark[cis]>
-1
<whitequark[cis]>
is this ... correct?
<galibert[m]>
yes
<galibert[m]>
very much so
<whitequark[cis]>
well signed(1) has only two values: 0 and -1
<whitequark[cis]>
that's how two's complement works
<whitequark[cis]>
so how come C(..., signed(1)) returns an out-of-range value?
<whitequark[cis]>
wait
<galibert[m]>
-1 is not out of range?
<whitequark[cis]>
no, sorry, it's in-range...
<whitequark[cis]>
the issue is actually about the overflow behavior
<whitequark[cis]>
oh, ok, no, you're right
<whitequark[cis]>
this is completely correct
<whitequark[cis]>
(I'm writing docs and I've managed to confuse myself with weird arithmetic edge cases so much I keep forgetting not everything is a weird edge case)
<galibert[m]>
huhuhu indeed
GenTooMan has quit [Remote host closed the connection]