<ignaloidas>
came across an interesting edge case with undefs while going over the cells, right now shifts are all undef if the shift value has any undefs, even though with some partial undefs you could argue some of the bits are known
<ignaloidas>
for example consider %0:8 = shl 00011100 01X #1
<ignaloidas>
the shift ammount is either 2 or 3, and as such the most accurate end result is X11X000
<ignaloidas>
but the const shift right now gives all X
<ignaloidas>
I'm not sure if this is truly worth the bother that caring about cases like this is, but it kinda feels like the undef semantics are wrong for this
<Wanda[cis]>
this is the kind of stuff that's simply not worth modeling
<Wanda[cis]>
verilog also gives an all-X value for this, and there's no real use in assuming a stricter definition
<ignaloidas>
feels inconsistent to me, you can get different results depending on whether you run optimization first, or lower it to muxes first
<whitequark[cis]>
yep
<whitequark[cis]>
that's expected, muxes are special
<ignaloidas>
that's how I encountered this in the first place, by lowering shifts into chained muxes
<whitequark[cis]>
you need a guard for undefs around the whole shift then yeah
<ignaloidas>
yep, and I can do that, just feels kinda bad losing information that's technically there :D
<whitequark[cis]>
well if you don't then you'll be inconsistent with basically every tool out there
<whitequark[cis]>
so what inconsistency is woree
<whitequark[cis]>
s/woree/worse/
<ignaloidas>
similar stuff with adc - %0:4 = adc 1111 XXXX 1 is technically 1XXXX
<ignaloidas>
but yeah, understand the consistency with the rest of the ecosystem argument
<ignaloidas>
just ahhh, the horrible edge cases where you could do better but mustn't
<whitequark[cis]>
i don't feel like it's that horrible?
<whitequark[cis]>
tracking this stuff has a cost, like not being able to use SMT shifts
<ignaloidas>
for my SAT work that doesn't really matter, my primitives are undef-aware, though everywhere else it is indeed quite a pain
<ignaloidas>
the edge cases feel horrible to me because it kinda defies expectations, e.g. with the adc case, a higher bit is defined, even though one whole input is fully undef
<whitequark[cis]>
the way I think of undef is that it's a bound, not a precise contract
<whitequark[cis]>
"we make at most this much undefined, because we want to make these transformations"
Chips4MakersakaS has joined #prjunnamed
<Chips4MakersakaS>
Things is that most flows based on proprietary tools contain custom TCL scripts which may not be vetted so much and thus be bug free.
<Chips4MakersakaS>
<whitequark[cis]> "I think there are cases where..." <- Also for ASIC I feel that the code base should be bug free enough, with proper CI and regression tests so that LEC should not be needed all the way through. Big gripe I have with the proprietary EDA tools and flows.
<mei[m]>
i disagree. if you're betting millions on the output being correct, you want formal verification. you do not want to be betting that you haven't accidentally triggered an unexplored edgecase
<Chips4MakersakaS>
I'm not stopping anyone from including LEC in their flow along the way. What I am saying that one should strive to make your EDA tools and flows dependable even when no LEC is included in the flow; just like GCC/LLVM.
<Chips4MakersakaS>
lets's say: ... just like GCC/LLVM/rustc/...
<mei[m]>
oh, yeah, definitely
<widlarizerEmilJT>
Naturally, yes, but for LLVM there's alive2, an optional add-on to basically do LEC
<widlarizerEmilJT>
To me knowledge it doesn't work by verifying an optimization's implementation generally but by turning it on for a run of the compiler quite like LEC
<widlarizerEmilJT>
To my* knowledge. I'm not british
povikMartinPovie has joined #prjunnamed
<povikMartinPovie>
> one should strive to make your EDA tools and flows dependable even when no LEC is included in the flow
<povikMartinPovie>
I haven’t seen anyone propose otherwise. It would be foolish to take the availability of LEC across the flow as an excuse for leaving correctness bugs in
catlos has joined #prjunnamed
<povikMartinPovie>
If anything it can help to make the tool robust even if you don’t enable it
<povikMartinPovie>
So I don’t see much to discuss there
<catlos>
fwiw i was under the impression that ASIC tools introducing bugs and thus LEC failures is pretty rare these days. from the perspective of a user LEC failure is a really annoying situation to be in because it tends to be very difficult to debug and even if you can debug you then have to try to get the tool fixed or whatever
<catlos>
but if i had millions at risk on a tapeout I would run LEC too lol
<povikMartinPovie>
Yeah, me to
catlos has quit [Remote host closed the connection]
catlos has joined #prjunnamed
<catlos>
when I say bugs i more mean unexpected correctness bugs. it is no suprise that ASIC tools contain bugs, but I think people tend to be conservative with the RTL they write etc to stick to parts that are believed to be robust (ofc I am not saying this is the ideal scenario)
catlos has quit [Ping timeout: 272 seconds]
catlos has joined #prjunnamed
catlos has quit [Remote host closed the connection]
catlos has joined #prjunnamed
catlos has quit [Remote host closed the connection]
catlos has joined #prjunnamed
<ignaloidas>
I feel like a big part of of people not regularly using LEC is that it is usually quite a bit slower than the normal flow. I hope to make it fast enough to not feel the difference by using SAT solvers which are generally way faster than SMT ones
<ignaloidas>
compilers for software kinda have to use SMT instead of SAT because building more useful properties for software out of just booleans gets hard real quick
<ignaloidas>
but I think for hardware, it's a lot simpler to build useful properties with just booleans, so SAT becomes more viable
<catlos>
all SMT solvers solve BV theories by reduction to SAT anyway so its in many ways a moot point, the difference is only in the efficiency to get to the SAT encoding (and the quality of the SAT encoding) but all you are doing is reinventing what the SMT solvers do anyway
<catlos>
also fwiw most commercial LEC tools predate the proliferation of SMT solvers so are largely built as rewriters with SAT solvers underneath (which is what an SMT solver is anyway, but I mean that they aren't calling out to dedicated SMT solvers)
<catlos>
(at least this is my impression, I don't know the LEC tools super well so I'm not certain, but for general formal verification tools this is to a reasonable extent true)
<catlos>
I suspect also there is a split between the tools that compare two high level designs (e.g. C2RTL/HECTOR) which can benefit more from SMT than the tools that verify synthesis where the post synth netlist naturally has no high level structure left
<ignaloidas>
right, but for software, BV is in a wide variety of cases not enough
<ignaloidas>
whereas for hardware, it's all that you need
<catlos>
array theory is useful for the case of memories
<catlos>
and depending on what you are verifying in software QF_ABV can be sufficient for software verification
<ignaloidas>
also there's the fact that the SAT solvers integrated into SMT solvers tend to lag behind quite a lot
<ignaloidas>
and like, a two evening project to port what's being done with SMT solvers 1-1 to SAT gave me almost 100x speedup
<ignaloidas>
there are overheads associated with SMT, and that's unavoidable
<catlos>
of the state of the art SAT solvers that I would consider stable enough to use practically, kissat is the best non-incremental and cadical the best incremental. bzla supports both, cvc5 and btor support cadical, and I would also add that it is relatively well known that modern SAT solvers are not necessarily better on hardware verification problems than minisat/glucose era solvers
<catlos>
its already been discussed but wq suggested that a lot of the SMT overheads in the project at the moment are probably avoidable/are to an extent justifiable
catlos has quit [Quit: Leaving]
Linouth has joined #prjunnamed
Linouth has quit [Quit: Client closed]
<whitequark[cis]>
a lot of the overhead is just "sending a command to the solver over a pipe one at a time and waiting for a reply"
<whitequark[cis]>
rushing to rewrite something in a way without even measuring where the overheads are is just foolish
<whitequark[cis]>
s/in a way//
<whitequark[cis]>
would be interesting to force bzla and some others who have it (cvc5?) to use kissat specifically and see if that improves runtimes over z3