<ignaloidas>
just not sure how exactly it should be integrated, it's a tool that's really only useful if adding/modifying new cells, and it can take a long time on more complicated cells, which rules out using it on runtime
<ignaloidas>
but with this a SAT verification backend should be way simpler to write
<Wanda[cis]>
how would this work when a cell has, say, 100 inputs? like a wide match cell
<ignaloidas>
it's only workable to ~20 inputs+outputs, but building stuff out of smaller blocks works just fine
<ignaloidas>
though match will be fairly hard to handle
<ignaloidas>
also, meant ~20 input+output bits, because of undef that's 10 actual inputs/outputs
<whitequark[cis]>
that seems too limited to be useful, I think it needs to be based on abstract interpretation if it goes upstream
catlos has joined #prjunnamed
<catlos>
given an SMT solver is going to be doing an encoding down to a SAT solver the same as this anyway is there much benefit to using a SAT solver rather than just using an SMT solver that performs better than z3 on BV (bitwuzla or similar)?
catlos has quit [Client Quit]
<whitequark[cis]>
i feel like we should just use bitwuzla and improve the interface to the SMT solver which currently has massive, glaring inefficiencies
<whitequark[cis]>
I get that writing a SAT lowering from scratch is fun but if the goal is to improve performance then the first step should be to batch requests so that you only need one or two writes to the pipe
<whitequark[cis]>
the main reason I didn't already use bitwuzla is that it's not in Debian
<whitequark[cis]>
(batch requests and compare performance)
<whitequark[cis]>
I should just build bitwizla as wasm
<Wanda[cis]>
Cat behavior
<whitequark[cis]>
you know, the usual
<Wanda[cis]>
(I agree)
<whitequark[cis]>
s/bitwizla/bitwuzla/
<whitequark[cis]>
in any uncertain situation build to wasm
<ignaloidas>
from my point of view, it would be easier to add new cells for verification with this than by using SMT, as you don't really need knowledge on how the SMT functions work, just to be able to write down the behavior in Rust
<ignaloidas>
I will finish my implementation over the next couple of weeks and put it as a WIP, so some more discussion can be had there
<Wanda[cis]>
no, this is just plain not a workable solution
<Wanda[cis]>
you have no means of symbolically executing a Rust function, do you?
<Wanda[cis]>
which means it's all based on evaluating truth tables, and that just doesn't work for large cells
<ignaloidas>
Sure, but you can build large cells out of smaller cells fairly ergonomically
<ignaloidas>
I honestly don't think it's that bad, and from what I've got so far it feels simpler than dealing with a bunch of SMT bv functions
<Wanda[cis]>
then how are you going to handle large cells, exactly?
<ignaloidas>
e.g. adders are built out of a bunch of 2-bit adders chained together
mei[m] has joined #prjunnamed
<mei[m]>
so, your approach is useful for... only the simplest type of cell that we have fully handled already?
<mei[m]>
like, this doesn't work for any cells with behavior actually complicated enough where it's worth it to be trying to reduce complexity, does it?
<Wanda[cis]>
okay, but what are you going to do about match cells, which were the motivating example?
<ignaloidas>
encoding for an adder is ~30 lines of code in the SMT encoding with complex rules around undef and such, where my impl is way simpler and understandable
<mei[m]>
like, yes, if you're generating cnf yourself it might be a good idea to write a function that generates a little chunk of cnf from a LUT2
<ignaloidas>
for match cells I've thought off of a simpler encoding that doesn't truly benefit from generated clauses
<ignaloidas>
*shrug* I'm doing this mostly for fun anyways, it's probably best to discuss if it's worth integrating once I'm done with it to a satisfactory point
<Wanda[cis]>
fair; I do believe it'd be better to discuss the tricky part first, but if you want to experiment, have fun
<whitequark[cis]>
I don't feel that the implementation complexity is the limiting factor with the existing SMT verifier
<whitequark[cis]>
it presents some issues, but you can use Rust functions to build a really simple eDSL for defining behavior of e.g. match cells in terms of and/or/imply/etc
<whitequark[cis]>
this is in fact what the current implementation does! it just does it poorly, and would benefit from some (a lot) of refactoring
<whitequark[cis]>
in light of this I feel that the proposed truth table based solution is strictly worse
<Wanda[cis]>
I agree
<Wanda[cis]>
we should invent a better interface for combinational cell behavioral description, I think
<whitequark[cis]>
yeah
<Wanda[cis]>
something where you'd pass a context object to a lowerer, and the lowerer would call logic primitives on the context
<Wanda[cis]>
then you could use it to do SMT, SAT, or even build truth tables (potentially useful for LUT lowering actually)
<whitequark[cis]>
yes
<whitequark[cis]>
the primitives would probably be and, not, xor, mux?
<whitequark[cis]>
although, shifts
<whitequark[cis]>
yeah it'd be more complex than that
<whitequark[cis]>
yeah we need to sit down and design this properly at some point
<Wanda[cis]>
mhm
<whitequark[cis]>
but the target interface is something that we can get this started/prototyped on
<Wanda[cis]>
that's the thing I was mostly thinking of, yes