<whitequark[cis]>
okay, this is something i think is very exciting
<whitequark[cis]>
try cargo test --features verify
<whitequark[cis]>
yes
leocassarani[m] has joined #prjunnamed
<leocassarani[m]>
So you're able to run Z3 after every optimisation pass to verify the changes you've staged are equivalent to the state of the design?
<whitequark[cis]>
actually, once we have a proper X-prop model it will be not equivalence but refinement
<whitequark[cis]>
i.e. a check that no X could've been introduced where one wasn't there before
<whitequark[cis]>
(actually#2, Z3 is probably one of the worst choices for the SMT solver here and we should be using bitwuzla, but it's not in Debian and i'm too tired to figure out where to get it)
<leocassarani[m]>
From a performance point of view?
<whitequark[cis]>
if you can call "never finishes" a type of "poor performance" yes
<leocassarani[m]>
Yeah I suppose you can lol
<leocassarani[m]>
Is this meant to replace the prjunnamed_smt2 subcrate, or are they doing different things?
<whitequark[cis]>
replace
<whitequark[cis]>
it's just not quite possible yet because of the way things are wired together
<leocassarani[m]>
It's really cool work
<whitequark[cis]>
thank you
<whitequark[cis]>
it will be even cooler once i add sequential verification
<whitequark[cis]>
the core observation here is that even though our flops don't have names, we don't need names in order to reliably match up before- and after-transformation flops
<whitequark[cis]>
this is because we know precisely what is being replaced with what
<whitequark[cis]>
i'm going to start with an assumption that "if you replace a flop with another flop, their (hidden) state bits are the same"
<whitequark[cis]>
which is going to be a slight improvement on yosys, which can generally do this but using a fragile equiv_make thing which in practice usually falls over
<whitequark[cis]>
(up until now i've been relying on yosys equiv_* passes for validating transformations, and they fall over on any design with flops where those aren't connected to POs. no idea why)
<leocassarani[m]>
Will you be able to run SMT verification even "post-synthesis" — that might be the wrong term, but I'm talking about the step where you go from generic to target-specific cells?
<whitequark[cis]>
i tried to design the interface to make this possible but because of some really annoying rust bullshit that is kind of tricky
<whitequark[cis]>
there is nothing technically challenging about it, it's just the combination of "`&dyn` pointers" and "non-`&dyn`-safe trait objects" that makes this hard
<whitequark[cis]>
i think the most likely approach here will be either an unmap pass which turns LUTs into target independent cells, or a way for the target to provide a tiny Design implementing any given target cell
<whitequark[cis]>
or we fix the trait
<leocassarani[m]>
I might be a little lost but when you talk about targets providing a tiny Design for their target cells, is that sort of like Yosys's cell library Verilog files?
<Wanda[cis]>
whiteboxes, yes
<Wanda[cis]>
but I think we're just going to fix the trait with the power of violence (interning)
<leocassarani[m]>
I mean I've noticed there isn't a single unsafe block in the whole project yet
<whitequark[cis]>
that's quite intentional
<leocassarani[m]>
Yeah hopefully you don't need unsafe to make the types work
<Wanda[cis]>
there's not a single one in combine, either
<_whitenotifier-4>
[prjunnamed/prjunnamed] whitequark 3b11753 - netlist: print designs with pending changes with diff markup.
<whitequark[cis]>
okay check this out. if you print the design before running apply() (or if LEC fails and it prints an unapplied design), you get this:
<leocassarani[m]>
So nice that you get a counterexample as well
<whitequark[cis]>
well yeah, how else would you actually use it?
<leocassarani[m]>
True, I think I was reacting to how you've done the quality of life work to express the counterexample in terms of your design's nets instead of exposing SMT internals, but I realise it's not a complex transformation
<whitequark[cis]>
oh, yeah
<whitequark[cis]>
I don't actually like SMT internals very much so I don't want to show them anywhere
<whitequark[cis]>
if you really have to, RUST_LOG=easy_smt=trace
mei[m] has joined #prjunnamed
<mei[m]>
I wonder if you'd get better performance lowering directly to sat instead of smt
<whitequark[cis]>
im not being paid enough for that,
<whitequark[cis]>
like i am using smt-lib to avoid tying myself to a specific solver
<whitequark[cis]>
what's happening here is that the decision pass builds, well, decision trees, which rely on the law of excluded middle (it makes the assumption that 1 and or %0+1 %0+1 are the same thing, which they are not in presence of undef)
<mei[m]>
<whitequark[cis]> "what's happening here is that..." <- %0+1 is bit 1 of the %0 cell? how is `or a a` always 1?
<whitequark[cis]>
* what's happening here is that the decision pass builds, well, decision trees, which rely on the law of excluded middle (it makes the assumption that 1 and (or x (not x)) are the same thing, which they are not in presence of undef)
<whitequark[cis]>
sorry, that was just wrong
<whitequark[cis]>
and yes
<mei[m]>
also, is the semantics of the match cell documented anywhere? because i'm having trouble inferring it from the syntax
<mei[m]>
is it a sequence of patterns that turn into one-hot if they match?
<mei[m]>
which way do concats go?
<whitequark[cis]>
concats are { msb ... lsb }
<mei[m]>
okay, i think i see the general idea of the match
<whitequark[cis]>
match cell has a sequence of alternates; [000] is equivalent to 000
<mei[m]>
what are the square brackets?
<mei[m]>
surely not a memory reference ;3
<whitequark[cis]>
you could also have [000 111] if you want to accept either of those
<whitequark[cis]>
both of them will correspond to the same one-hot bit
<mei[m]>
oh, the rust types go `patterns: Vec<Vec<Const>`
<mei[m]>
the inner vec is list of alternatives?
<whitequark[cis]>
yes
<mei[m]>
hm so, maybe X as input to a match cell should result with all X's on the output of the match?
<whitequark[cis]>
what about match X { X }?
<Wanda[cis]>
mei: so my thinking is that our X model is not fit for purpose
<Wanda[cis]>
we don't have law of excluded middle. law of excluded middle turns out to be useful in transformations. ergo, shit's fucked.
<Wanda[cis]>
so we have just talked about it a fair bit IRL
<Wanda[cis]>
let me repeat it here
<Wanda[cis]>
argument
<Wanda[cis]>
1. Verilog's X model (which we are currently using with minor modifications that don't matter) is Like That because it attempts to model physical reality of signals not necessarily being 0 or 1
<Wanda[cis]>
2. there are, indeed, circumstances where this is useful; if you are dealing with asynchronous logic, you very much want to be sure a transitioning value doesn't end up fucking you over because some logic optimization assumed a signal cannot possibly be neither 0 nor 1
<Wanda[cis]>
3. however, for the vast majority of useful logic, assuming that a value is, in fact, 0 or 1 is reasonable; in fact, this applies to everything within a properly designed synchronous clock domain, because all your inputs should go through synchronizers, and synchronizers by their nature convert (hardware) X values to either 0 or 1
<Wanda[cis]>
4. still, people will inevitably try to synthesize some dodgy asynchronous crimes and yell at us that we broke it with some cute optimization
<mei[m]>
Wanda[cis]: seems like an issue of proper documentation
<Wanda[cis]>
5. hence, we likely need to know for each signal whether it can be a true hard X (because it comes from dodgy async stuff) or not, and apply differing X semantics
<whitequark[cis]>
(nobody reads the documentation for their synthesis tool)
<whitequark[cis]>
(if Maya's experience taught me anything, it's that people will not even look at the text of the diagnostics in front of them. they'll stare at a log telling them what's wrong and ask "huh, what's wrong??")
<mei[m]>
god that's infuriating
<whitequark[cis]>
yep.
<mei[m]>
must be why rustc is investing big time on making diagnostics as readable and monkey-level explained as possible
<whitequark[cis]>
she was offered to be paid quite a bit to teach a course that would boil down to "dumbass. here is how you read the diagnostics vivado prints"
<Wanda[cis]>
6. how *exactly* it will work, I do not know; possible tools involve two different X values, annotating cell with async-safeness-required, LLVM-like freeze cell, etc.
<mei[m]>
I would suggest:
<mei[m]>
1. pick semantics for match and friends that are convenient in the presence of X's, so that legalizations can always be applied
<mei[m]>
2. mark optimizations as whether they are async-safe
<mei[m]>
alternatively i guess you can have a less optimal async-specific legalizer for match's?
* whitequark[cis]
is having a POSIX flashback
<mei[m]>
that basically lowers to a basic-ass if-else tree
<mei[m]>
so, where does the match cell come from? does it have a verilog counterpart with specified X semantics?
<whitequark[cis]>
uhm, i designed it (originally for amaranth... ish)
<whitequark[cis]>
* amaranth... ish. we ended up actually changing amaranth a little but in ways that don't matter)
<Wanda[cis]>
<mei[m]> "so, where does the match cell..." <- I'll rant about verilog bullshit when done eating
<mei[m]>
uh oh
<Wanda[cis]>
actually hold on
<Wanda[cis]>
haven't I already ranted to you about it?
<Wanda[cis]>
I think you were very upset
<Wanda[cis]>
anyway.
<mei[m]>
Wanda[cis]: ✨️ dissociative amnesia ✨️
<Wanda[cis]>
unnamed match cells come from Amaranth NIR match cells which were designed to lower Amaranth HDL Switch/Case which were designed for RTLIL processes which are a loose and shitty fanfic of Verilog case statement.
<Wanda[cis]>
Amaranth doesn't help us in any way because it doesn't have an X model
<Wanda[cis]>
RTLIL doesn't help us in any way because processes are comically underspecified things, particularly when it comes to X behavior (you cannot do basically anything with them other than lowering them which makes them stop being processes and start being plain mux cells)
<Wanda[cis]>
this leaves Verilog.
<Wanda[cis]>
in Verilog.... well, you know a language is good when it has both == and === operators
<mei[m]>
godddddd
<Wanda[cis]>
== is X-propagating; 1 == x returns x
<Wanda[cis]>
=== just fucking compares the raw thing; 1 === x is 0, x === x is 1
<Wanda[cis]>
needless to say, === cannot be realized in hardware. if you use it as part of your RTL, you're not going to see the Light of Heaven.
<Wanda[cis]>
so, how Verilog case statement works is... consider case (abc) def: [...]; ghi: [...]; endcase. this will execute first branch if abc === def; otherwise, it will execute second branch if abc === ghi; otherwise, it will do nothing
<Wanda[cis]>
an if-else works the same way (does cond === 1 effectively)
<sdomi>
i've heard mei[m] actively groaning in close vicinity what's up
<mei[m]>
was verilog designed within 10 days or something?
<whitequark[cis]>
oh, you should read HOPL paper on Verilog
<whitequark[cis]>
it has some exquisite stuff
<Wanda[cis]>
okay since Cat just asked me about this.
<Wanda[cis]>
there are two more case statements in Verilog!
<Wanda[cis]>
casez is like case, except it treats the Z value (the fourth logic value in Verilog which we do not have) as a don't-care, on both sides of the comparison (ie. both in the switch value and case value)
<Wanda[cis]>
and casex is like that, except it treates both X and Z as don't-cares
<Wanda[cis]>
sdomi: we are discussing Verilog.
<mei[m]>
so... does verilog have good reasons to have separate Z and X?
<sdomi>
Wanda[cis]: yeah, i noticed, my remark was meant to be humorous. sorry
<Wanda[cis]>
mei[m]: so it is sometimes kinda useful. but not very.
<mei[m]>
is it useful at all outside of simulation?
<Wanda[cis]>
see, Verilog doesn't have conditional assignments to wires (as opposed to VHDL)
<mei[m]>
i am making the most flabbergasted of faces right now
<Wanda[cis]>
so the only way to write a tristate buffer, which are very useful, is to do assign io = oe ? o : 1'bz;
<Wanda[cis]>
you kinda need that special value in the expression to express "actually you know maybe don't actually drive this wire right now"
<Wanda[cis]>
and then when you look at the VCD trace you see Z instead of X for undriven wires
<mei[m]>
is this the sort of thing that's fully out of scope for unnamed, or something that's to be lowered to a mux?
<whitequark[cis]>
unnamed has iob cells that implement it
<Wanda[cis]>
which is very useful! it lets you distinguish two different cases of fucking yourself over due to Verilog not complaining about multiple drivers for a wire
<Wanda[cis]>
mei[m]: for the love of god, no, you *don't* fucking represent this as a mux
<Wanda[cis]>
this is unhinged
<Wanda[cis]>
it's not a mux. it's a tristate driver. a conditional continuous assignment, if you prefer
<galibert[m]>
Verilog is peak performance
<Wanda[cis]>
... yosys represents it as a mux, by the way.
<leocassarani[m]>
While also printing out a warning about how it doesn't support tristates
<mei[m]>
Wanda[cis]: yeah but it's not implementable in fpga so you need to legalize it by taking all the conditional assignments to a wire and turning them into one big mux
<Wanda[cis]>
then it implements completely wrong semantics for it in most of the passes because it is, in fact, not an actual mux
<jn>
LALSD, funny name
<Wanda[cis]>
so it has a pass that converts that to a proper tribuf cell
<mei[m]>
does yosys do mux with loopback?
<Wanda[cis]>
which you are expected to run right after frontend
<Wanda[cis]>
because apparently recognizing the single allowed mux pattern in frontend would be too hard.
<Wanda[cis]>
mei[m]: I don't understand the question
<Wanda[cis]>
mei[m]: it actually is
<Wanda[cis]>
you can have them on the edge of the FPGA, for driving external signals
<Wanda[cis]>
it is, in fact, quite useful
<mei[m]>
as in. is the yosys representation of a tristate buffer a = mux ctl { a in }
<Wanda[cis]>
also fun fact: older FPGAs actually did have internal tristate buses
<Wanda[cis]>
so a tristate buffer is a perfectly implementable cell on those
<mei[m]>
Wanda[cis]: ok well that's basically a vendor cell that doesn't represent the tristateness in any way to the toolchain
<Wanda[cis]>
mei[m]: no, it is io = mux oe o Z
<mei[m]>
okay, i can see how one would come up with that but
<mei[m]>
jesus christ
<Wanda[cis]>
yosys doesn't enforce the single-assignment rule, btw.
<Wanda[cis]>
becuse yosys is based on verilog
<mei[m]>
b-but
<Wanda[cis]>
for the love of god, do not base your synthesizer IR on Verilog. even if you only synthesize Verilog.
<mei[m]>
that's completely unworkable for an IR!!
<Wanda[cis]>
well, guess why this project exists
<mei[m]>
how the fuck did they get anything dne
widlarizerEmilJT has joined #prjunnamed
<widlarizerEmilJT>
sure is, mei, sure is
<Wanda[cis]>
painfully.
<Wanda[cis]>
speaking from experience
<widlarizerEmilJT>
we have coping datastructures that waste computation to work around RTLIL
<whitequark[cis]>
it involves so much suffering
<whitequark[cis]>
every major pass i've tried to design or designed has its own IR on top of RTLIL
<Wanda[cis]>
widlarizerEmilJT: I wrote a fair amount of them
<widlarizerEmilJT>
I know, I check the blames and copyright headers
<mei[m]>
okay i do acknowledge that masochism is a thing that exists but this has gotta be the first time i saw it in a software design context
<whitequark[cis]>
...
<whitequark[cis]>
you'll enjoy ... several of my other projects
<whitequark[cis]>
for example, the "cross compile everything" projects (i think i have at least five?)
<whitequark[cis]>
the linux distro i maintained with Maya a decade ago, the ocaml windows, android, and ios ones, yowasp, i probably forget something
<mei[m]>
is the purpose here suffering, or the elimination thereof?
<mei[m]>
* is the purpose of those suffering, or the elimination thereof?
<whitequark[cis]>
yes
<mei[m]>
taking away the suffering of others?
<widlarizerEmilJT>
It all, including RTLIL, seems creating a solution to a yet-unsolved-in-some-sense problem, just with various level of forethought
<widlarizerEmilJT>
* RTLIL, seems like cases of creating a
<galibert[m]>
Is the conclusion that Verilog is unimplementable if one tries to follow the standard exactly so one just shouldn’t ?
<Wanda[cis]>
I'm sorry, what?
<galibert[m]>
I’m not sure, feels like the rules around x and z are not entirely usable in practice
<Wanda[cis]>
like. yes. Verilog cannot possibly be implemented. but for other reasons that don't follow from the discussion.
<Wanda[cis]>
you're confusing "unimplementable" with "unusable"
<galibert[m]>
Or at least trying to ends up all pain no gain
<jix>
what are good reasons for supporting x for synthesis?
<whitequark[cis]>
synthesis with don't cares allows more efficient use of resources
<whitequark[cis]>
that's basically it
<Wanda[cis]>
actually Verilog is only slightly unimplementable. SystemVerilog, however, is entirely unimplementable.
<Wanda[cis]>
in the self-contradictory spec sense.
<galibert[m]>
I’d be very interested in more specifics if you feel like rambling
<jix>
there are other ways to represent don't cares that seem less problematic (but I have no idea if they're good for synthesis)
<Wanda[cis]>
jix: wanna elaborate?
<Wanda[cis]>
galibert: so you may think that SystemVerilog is a language, or a standards document, or something like that
<Wanda[cis]>
this is completely wrong
<Wanda[cis]>
do you know how, say, Marvel comic book universe works?
<jix>
you can treat them as unconstrained and unknown values (but still values that are 0 or 1)
<galibert[m]>
Lemme grab some virtual popcorn
<jix>
you'd represent them similar to inputs but allow replacing them with fixed values
<mei[m]>
but then they need to have a consistent value
<Wanda[cis]>
you have a bunch of authors that kinda reuse characters and settings from one another, but don't really communicate all that well and you and up with a fuckton of massively distributed plotholes
<Wanda[cis]>
which you then work around by invoking multiverse or some other bullshit
<galibert[m]>
From what I understand when things collide they just say it’s a different universe
<galibert[m]>
Yeah that
<Wanda[cis]>
IEEE 1800 is a blurry snapshot of a weighted average of the SystemVerilog multiverse.
<galibert[m]>
Beautiful image
<jix>
or atually there are two ways you could specify what refinements passes are allowed to do, either you allow replacing them with fixed values on the input side or you say the set of observable input output behaviors may not get larger
<jix>
mei[m]: yeah, is that a problem?
<Wanda[cis]>
accepting this truth is actually the only way to get anything done with SystemVerilog
<mei[m]>
less optimization freedom
<jix>
do you actualy need that freedom?
<Wanda[cis]>
the only way you could possibly write a SystemVerilog tool is by accepting that you, too, are a fanfic writer. and if you're good enough at this, your fanfic will be promoted to canon one day.
<Wanda[cis]>
sure, it'll be in direct conflict with a bunch of other canonimplementations, but who cares
<galibert[m]>
Cat proposed three different X that are essentially don’t care, don’t know and NaB
<galibert[m]>
So sv is even less portable that C
<leocassarani[m]>
Maybe it makes sense to think of Verilog as a series of dialects? Like how people think of Lisp. Lots of different implementations, with a shared set of core assumptions and constructs, but lots of variation in syntax, platform, and use cases.
<Wanda[cis]>
that is essentially correct
<leocassarani[m]>
s/lots/huge/, s/of//
<Wanda[cis]>
you're reasonably safe if you stick to the basics
<Wanda[cis]>
but try anything clever, and it becomes very non-portable
<mei[m]>
leocassarani[m]: the difference is that there's no standard document claiming to define "Lisp"
<whitequark[cis]>
ANSI INCITS 226-1994 (S2018)?
<leocassarani[m]>
I mean, ANSI Common Lisp is a thing that exists
<leocassarani[m]>
But I agree that the analogy breaks down at some point
<Wanda[cis]>
Verilog at least attempts to be a standards document. it still fails at it in places, but eh.
<mei[m]>
whitequark[cis]: they explicitly call it merely a dialect of lisp
<whitequark[cis]>
right
<Wanda[cis]>
there is, for example, IEEE 1364.1, which specifies what is the synthesizable subset of Verilog
<Wanda[cis]>
and how it should map to hardware, in broad strokes
<Wanda[cis]>
there is no corresponding document for SystemVerilog. nobody has any fucking clue what the synthesizable subset of SystemVerilog is supposed to be. you just kinda guess it based on vibes.
<galibert[m]>
I must admit that a language where you supposed the drop half the source input to work, with which half depending on the tool, is something that hasn’t stopped fascinating me
<jix>
fwiw & iirc 1364.1 says x bits are only allowed in direct assignments, not in subexpressions, and one way to read it is that they are don't cares in the sense that they are either 0 or 1 at the point of the assignment
<Wanda[cis]>
uh?
<Wanda[cis]>
wasn't that about z?
<Wanda[cis]>
oh.
<Wanda[cis]>
ther is, indeed, something
<jix>
"The value x shall not be used with any operators or mixed with other expressions." my interpretation always was that the idea was that you don't perform any operation on it while its still x
<Wanda[cis]>
I mean
<Wanda[cis]>
that's kinda a meaningless statement
<mei[m]>
like, if you assign an X, that's still an X
<Wanda[cis]>
or hm.
<Wanda[cis]>
okay
<jix>
mei[m]: nope it says it's a don't care if you assign it
<Wanda[cis]>
I guessss it could be interpretted as effectively a freeze?
<jix>
I mean it's not clear at all, hence "my interpretation"
<Wanda[cis]>
at the point of assignment
<Wanda[cis]>
jix: hey welcome to the world of Verilog fanfic writers
<_whitenotifier-4>
[prjunnamed/prjunnamed] whitequark 1403c4f - decision: lower decision trees without violating refinement rules.
<jix>
from a formal verification perspective it also makes much more sense to only allow frozen x values as part of the input as that's the semantics you get with FV tools
<jix>
including commercial ones from what I've been told
<Wanda[cis]>
hm.
<Wanda[cis]>
I guess that's an X model
<Wanda[cis]>
kill off the X value as it exists entirely, and add an undef cell instead which is frozen by definition
<Wanda[cis]>
... of course, getting to actually use it in optimizations may be tricky
<Wanda[cis]>
hmm
<jix>
I wouldn't even be surprised if the rewrites you can do by knowing that there is no x propagation help more than the freedom to assign inconsistent values to x bits
<whitequark[cis]>
is that really true?
<jix>
I'm not sure, but I wouldn't be surprised
<whitequark[cis]>
i can't think of any place where being aware of x-prop means we can't make better decisions
<whitequark[cis]>
even the example above resulted in better synthesis
<whitequark[cis]>
oh, Wanda points out that this could be useful in LUT packing
<jix>
my reasoning is that every rewrite that's a valid refinement with x-prop semantics and no constant x bits or partially defined operations is an equivalence under 2-valued logic but not the other way around
<_whitenotifier-4>
[GitHub] Approachable is better than simple.
<mei[m]>
did whitenotifier get into its daily affirmations mode?
<whitequark[cis]>
i'm setting up some webhooks and whenever you add one it does this