<jix>
so for fpmul_test.smt2 the bitwuzla -SE kissat I ran overnight made very little progress and now I need to reboot for updates (for fp16mul_test it was 9 times faster than z3 on my machine)
<programmerjake>
ok, as expected it's probably brute-forcing it to some extent
<jix>
yeah, even proving equivalence of different integer multipliers isn't handled very well by CDCL solvers
<programmerjake>
if you have time, could you look at my pr to see if i made any major mistakes? i don't want to merge it yet until i have modified nmigen to use it and can verify that works...it does have a test tho so at least it works in verilog
<programmerjake>
thx!
<jix>
so far I'm much more familiar with the formal parts (smtbmc, sby and specific yosys passes) than yosys overall (which is where part of my hesitation to add a cell for this comes from) but I can have a look
<programmerjake>
thx!
<programmerjake>
oh, should i escape the expression to avoid unintentionally producing smtbmc command comments?
<cr1901>
Ahhh, this would explain why sccache thinks nothing's up to date
<cr1901>
(I think)
<mwk>
I umm
<mwk>
I may have landed a... thing
<cr1901>
Yea, it's not a problem. I was just trying to benchmark something and now the results are gonna be thrown off :P
<cr1901>
More amused than anything that the one day I decide to do this, a new feature lands :D
<mwk>
do what?
<cr1901>
I upgraded to an SSD after my Windoze installation died. I wanted to benchmark how fast I can build yosys on this 11 year old Core i7 laptop when the hard drive bottleneck is removed 1/2
<cr1901>
with management engine on and off
<cr1901>
err not management engine
<cr1901>
Idk where my mind is tonight
<cr1901>
With MsMpEng.exe (Defender/Antivirus) turned on and off*.
<cr1901>
I git pulled thinking it wouldn't matter much, and to give a more realistic incremental build. Whoops :D
<mwk>
welp sorry I destroyed everything
<cr1901>
No worries. You landing a new feature is far more important than my silly benchmark :3.