<catlos>
as much as the class part of SV sucks, the constrained random gen stuff is actually kinda magical to use i like it
<catlos>
does need some care though because i dont think the generators are doing anything too crazy and can end up really slow (i haven't done anything on this kinda verification in like 4 years but i remember cases where it was significantly cheaper to guess and check a random value a few times until i got a value meeting the constraints than try to get the CRV solver to generate a correct value by construction)
<catlos>
jix: i think a lot of the fancier projected sampling/counting is newer anyway right? constrained random generators have been in the simulators for quite a long time now (at least the stuff from kuldeep meel's group)
<catlos>
https://github.com/will-keen/constrainedrandom also worth noting there are various open source implementations of these ideas but my impression is they mainly get used by the asic companies that want to reduce how many seats they are paying for with the commercial sims
catlos has quit [Quit: Leaving]
<vancz>
ok the book later clears the story up a bit regarding the simulation model and non/blocking assignment, in the sequential logic chapter
<galibert[m]>
<vancz> "x'D" <- Is that a decimal constant with undefined number of bits?
<whitequark[cis]>
we've just spent a while discussing egraphs in depths
<whitequark[cis]>
this is the obviously correct step to take, in my viee
<Wanda[cis]>
yup, was wondering when that'd happen
<whitequark[cis]>
s/viee/view/
<Wanda[cis]>
yeah I figured we'd likely end up using those
<galibert[m]>
What are they, a cool data structure?
<Wanda[cis]>
a cool compiler IR data structure
<Wanda[cis]>
which is apparently hard to implement
<Wanda[cis]>
but cranelift managed and it appears to be working quite well for them
<Wanda[cis]>
you know the "choice node / cell / whatever" that was proposed here at several points? the "use either this input or the other input of this cell as the output, we know they are equal" cell?
<galibert[m]>
Yeah
<Wanda[cis]>
egraphs are about having this as a core part of the representation instead
<galibert[m]>
Weird
<Wanda[cis]>
mei has spent a fair amount of time ranting to me about it over the last year
<Wanda[cis]>
though I don't fully understand how it works
<whitequark[cis]>
Wanda[cis]: there are some additional nuances that make it actually work
<mei[m]>
Wanda[cis]: I've found it hard to implement because when I tried it was literally the cutting edge of the research and it wasn't documented well and I had to page in everything to understand what the invariants are supposed to be
<whitequark[cis]>
many of which we've already sort of stumbled into as desired outcomes in prjunnamed
<mei[m]>
(we've watched this together with cat today)
<whitequark[cis]>
interestingly it likely won't save us from tree rebalancing and other associativity related issues
<whitequark[cis]>
since cranelift found the computational complexity intractable
<Wanda[cis]>
hmm
<Wanda[cis]>
yeah I wouldn't expect that to work
catlos has joined #prjunnamed
<catlos>
I wonder if the fact that prjunnamed tracks signals by bit adds some complexity or worse performance than in the word level e graph settings too (unless you would be tracking equivalences just at the operator level?)
<catlos>
im sure jix has thoughts from implementing an IR with e-graphs at its core for imctk too
<jix>
are you considering e-graphs or aegraphs?
<jix>
e-graphs are from 1980 and are relatively simple, aegraphs are what cranelift uses and what they came up with relatively recently
catlos has quit [Ping timeout: 246 seconds]
catlos has joined #prjunnamed
<jix>
I've been using e-graphs but I'm not that happy with the overall combination of choices I made in for the IR in the imctk prototype
<jix>
for e-graphs there are also two variants of invariant maintenance, the classic eager one and the lazy/batched one that I think egg introduced
<jix>
can't really say much about aegraphs, they sounded interesting but their motivation didn't seem related to anything I needed
<jix>
(in where they differ from egraphs)
<jix>
oh and I think some older literature doesn't call it egraph but describes it as an algorithm for congruence closure, but that's maintaining/restoring the invariants
<whitequark[cis]>
<jix> "are you considering e-graphs..." <- aegraphs
<whitequark[cis]>
<jix> "can't really say much about..." <- the whole aegraph talk seems very directly related to unnamed
<jix>
yeah I think the differences between egraphs and aegraphs are along the lines of the differences between the requirements of imctk vs prjunnamed we discussed before
<jix>
(aegraphs could also be useful in a FV setting during translation between representations, but I'm not sure they're worth it if you're using plain egraphs to accumulate and propagate facts already anyway)
<whitequark[cis]>
yeah, makes sense!
catlos has quit [Ping timeout: 260 seconds]
<mei[m]>
<catlos> "I wonder if the fact that..." <- yeah, I have some ideas in this area
<mei[m]>
generally I think that the Union node should accept mixed values
<mei[m]>
(mixed as in, not the output of a single cell)