Saturday, 2022-05-14

lkclwhat's cvc5?00:04
lkcli tried yices-smt2 that was missing "(set-logic XXX)"00:04
* lkcl found it00:04
lkclso i tried setting set-logic QF_BV and it complained "Float32 not found"00:05
* lkcl running z3 with "-v:3" option to see what's going on00:06
programmerjakethe smtlib2 standard didn't yet add any logic that has fp support, so i'm just relying on ALL or whatever equivalent each smt solver has00:07
programmerjakebasically setting a logic is limiting the set of operations supported to whatever value you specified.00:08
lkcl(define-sort xxx BitVec) won't work on yices-smt2 until a set-logic has been declared00:11
lkclah set-logic ALL should do it00:11
lkclstill Float32 missing from yices200:12
lkclalthough it stopped the complaints "BitVec undefined" on the (define-sort)00:12
programmerjakeyices2 may not support smtlib2 fp...00:13
programmerjakeno fp support:
lkclcan i suggest adding an fp16 version of fpmul?00:22
lkcland doing an fpadd00:22
lkcljust to see what happens on the completion time?00:22
lkclgoing straight to "most complex and not completing" gives no sense of scale00:23
lkclor, heck, even fp800:24
programmerjakefp16 fmul should be relatively easy, fadd is much harder to implement since you have to handle huge+tiny cases00:24
lkcl(which the AI team in India want to do)00:24
programmerjakef8 is small enough i'd probably just use exhaustive checking and not bother with smt00:24
lkclit's still a good base for "if smt2 goes into brute-force at least it'll complete"00:25
programmerjakebut we want to prove f64 code...if it has to use brute-force it fails00:26
lkclthe point of using correctness proofs on the smaller FP types is that the ieee754fp code is identical except for the parameterised mantissa/exponent11:26
lkclwith the exception that the number of stages chained together will vary, there's no difference - at all11:27
lkclthus a proof at FP8, FP16 and BF16 does actually give us a confidence level at FP32, FP64 and even FP12811:27
*** littlebo1eep is now known as littlebobeep12:27
ghostmansd* fneg FRT,FRB (Rc=0)12:29
ghostmansd* fneg. FRT,FRB (Rc=0)12:29
ghostmansdShouldn't fneg. have Rc=1?12:29
ghostmansdI see several such records, it was my understanding that these opcodes differ by Rc only, being identical otherwise12:30
lkclno not a bug in v3.0 spec, it'll be a cut/paste error somewhere13:17
lkclghostmansd, sorted13:18
ghostmansdlkcl, star13:19
lkclfound some more with a grep13:20
ghostmansdI suggest we add fsins/fcoss/ternlogi/grev* as standalone patch, outside of SVP64. Any objections?13:43
ghostmansdThese will be available under -mfuture switch.13:43
ghostmansdI also consider this to be outside of 550, and suggest to get a budget for it from 577 directly. These don't look as SVP64-specific, moreover, they can be submitted outside of SVP64 patch.13:49
ghostmansdAlso, it'd be great if I had any pointers to the corresponding discussions with OpenPOWER Foundation.13:59
tplatenI tried to build;a=shortlog;h=refs/heads/libresoc_dev on my Talos II, it was unable to find some llvm headers14:31
tplaten../src/libre-soc/vulkan/libresoc_llvm.h:5:10: fatal error: llvm-c/OrcBindings.h: No such file or directory14:31
tplatenmy headers are in /usr/include/llvm-c-11/llvm-c/OrcBindings.h14:31
lkclghostmansd, no perfectly good idea, actually kinda important [to do as separate patch]15:44
lkcl[and associated bugreport] [and associated budget]15:44
lkclthe OPF email was a private one to the Board of Directors15:45
ghostmansd> the OPF email was a private16:09
ghostmansdAh, OK, I thought there was some discussion publicly available, nevermind then. Just ping me when/if the opcodes are changed.16:09
ghostmansdWhat'd be the right bugreport? Is 577 OK? For all of these insns plus tests which check them in binutils, would 500 EUR be OK?16:11
ghostmansdRaised #83416:56
ghostmansdHell it's never a day without admitting there's stuff which I didn't know about Python. I had no idea one can write `0b1_0010_110` and make it work.17:04
lkclEUR 500 sounds fine17:30
lkcli sort-of summarised on binutils-dev17:31
lkcli knew you could do 0xffff_8000_000017:32
lkclit kinda makes sense that 0bnnn_nnn_nnn would also work17:32
lkclconverting to a dynamic-loadable-module system would be a separate bugreport btw17:37
lkcldlopen / dlsym is really straightforward, i don't know if you've ever done it before?17:37
lkclyou have one and only one function dlsym'd which is "return me a pointer to a table with more functions in it"17:38
ghostmansd[m]I've never implemented dlsym from scratch, but I dealt with relocations a bit, as well as jump tables and function pointers, and also debugged a proprietary dynamic loader. I hope this can simplify the stuff.18:51
ghostmansd[m]Do you have a link to the task about dynamic loadable module system?18:52
ghostmansd[m]Or is it just planned yet?18:52
tplatenStill trying out why I get an error in ecppack, is it only in ls2 not in microwatt. Both use the same output pins for the ddr3 ram.19:03
tplatenERROR: PIO 'X0/Y53/PIOB' does not appear to be a DQS site (expecting an 'A' pin).19:04
tplatenOnly one of those four pins is an 'A' pin.19:04
tplatenWhen I use DiffPairs("G18 H17", "B15 A16", dir="io"), I see that "B15 A16" does not appear in the lpf file generated by nmigen. Is this a bug in nmigen? I'm not sure.19:34
ghostmansdWhich is simpler to you?20:30
ghostmansdTo me, the answer is obviously a)20:30
ghostmansdBecause it's really obvious where each bit goes20:30
ghostmansdIs the whole `(instr << 6) vs (instr << 5)` debate caused by "64 takes 1 more bit"? Is it a right guess?20:33
ghostmansdFrankly, this is obscure way to write it. I cannot even decipher where the fields go without calculating it. This practically drops the bonus that there are additional variables like po and xo, which are helpful.20:34
*** ghostmansd <ghostmansd!> has left #libre-soc20:35
lkclghostmansd[m], just planned: i'm anticipating the OPF to come back with "hmm" on adding non-approved instructions, upstream20:58
lkcl(b) was written by programmerjake and he didn't follow the conventions set by other instructions21:01
lkclwhere, yes, i very deliberately put the MSB0 numbering into the source code so that it could be compared against the spec21:02
lkcland jacob hasn't done that, meaning that it will be harder to review21:02
lkcland is unnecessarily more lines of code21:03
lkcland doesn't contain comments21:03
lkclprogrammerjake, can you please correct all those?21:03
lkclfields are already ints, they do not need conversion to int21:03
lkclconstructing by shifting-then-shifting is not appropriate21:04
lkclstorage of fields[n] in a temporary variable as a means to avoid use of comments is not appropriate21:04
lkclalso can you add the relevant section cut/paste from fields.txt (i started doing that only a couple days ago)21:06
lkclalso please use yield ".long 0x%x" % insn21:06
lkclthe f"" format just pisses me off, it's the PHP nightmare all over again21:07
lkclalso, don't *reconstruct* the operation asm = f"bullshit PHP", just put the original operation!21:08
lkcl".long %x # %s" % (instr, insn)21:09
lkcl".long %x # %s" % (instr, insn)21:10
lkclshould reduce down by over 50% without the nonsense21:10
ghostmansdwell, I have nothing against f strings, they simplify reading quite a lot, if used correctly21:11
ghostmansdactually the only thing which pisses me off is shifting21:11
ghostmansdbecause it's not explicit21:11
ghostmansdanyway, I already deduced how it works, it simply took more time I wanted :-)21:11
lkclghostmansd, exactly. non-standard, non-obvious convention, it wasted your time21:12
ghostmansdI can fix these, but perhaps it'd be better for programmerjake to take handle it, since he's the code owner21:13
lkclthe fact that you're forced to run functions *inside the string* if you want hex or other format is the nightmare of PHP21:13
ghostmansdcool, eh?
* lkcl waits 15 seconds for DNS resolution at this end...21:14
lkclooo prettyyy21:14
ghostmansdyeah, the more I dig this code the more I like it21:15
ghostmansdand, btw21:15
ghostmansdUIMM and UIM6 are already for granted21:15
ghostmansdas well as the rest of operands, obviously21:15
ghostmansdso cute21:15
lkclwhat did you think of the idea of having the #defines (matching already-named fields) explicitly listed in
lkcl(perhaps even still auto-generate the template, but comment it out just like in opc-ppc.c)21:17
lkclit'd avoid you having to parse opc-ppc.c21:17
ghostmansdThis has one issue that we still can miss something updated in vanilla...21:18
ghostmansdI've been thinking, you know, perhaps a big regex?...21:18
ghostmansdBecause name of that table won't change, it's exported stuff.21:19
ghostmansdBut, frankly, all this deserves a standalone thought. Perhaps it's not even fully belong to sv_binutils, maybe some intermediate script which gets python/json/whatever-else-crap21:20
ghostmansdI haven't really given this topic a proper thought yet, TBH21:20
ghostmansdBut for sure will, because I want to make as much automatically as possible21:20
lkclbtw i have a strange form of dyslexia which means regex's are pretty much unintelligable for me.21:24
ghostmansdhere, perhaps, not even regex needed21:24
ghostmansdI mean, the name of this damned array is the same21:24
ghostmansdand C decl is the same always21:24
lkcli can read the symbols fine, there's no "disordering" going on as with normal dyslexia.21:25
ghostmansdthe only tricky part here are these `#define CRAP OTHER_CRAP + 1` macros21:25
ghostmansdthey're virtually throughout the whole declaration set of this array21:26
ghostmansdand the parser, if we implement it, must keep track of these21:26
ghostmansdnot unsolvable, but too much work for such a little shitty task21:27
ghostmansdso, any ideas are highly appreciated :-)21:27
ghostmansdI'd only like to ensure that we never ever miss a single #define in vanilla binutils21:27
lkclyes, my idea was - to reiterate: don't bother parsing21:28
lkcljust have an explicit declartion "if encounter field named X then output #define X Y"21:28
lkclstraight dictionary.21:28
lkcldead simple21:28
ghostmansdyou mean, generate the whole set of fields for PPC?21:28
lkclno, just have "those which are #defined"21:29
ghostmansdbut names are not yet all21:29
lkcla dictionary which if there is an entry you literally do print("#define %s %s\n" % (x_field, thedictionary[x_field])21:29
ghostmansde.g. let's consider
ghostmansdtake a look at grev insn21:30
lkclyou're creating entries only to find that the memcmp you showed me says "this exists already as field XXX", right?21:31
ghostmansd{RT, RA, RB, UIMM}21:31
lkclwell then have a dictionary with "{insert_name_of_new_field}" : "{insert_#define_name_of_original|}"21:31
lkclno pissing about21:31
ghostmansdnot always simple :-)21:32
ghostmansdagain, about grev21:32
* lkcl paying attention21:32
ghostmansdyou see, the difference between grev/grevi is how they handle the immediates...21:33
ghostmansdor, well, how many bits do they allow for an immediate21:33
ghostmansd5 or 621:33
ghostmansdand, well, binutils do allow to handle this...21:34
ghostmansdbut, if we operate on our level, in python...21:34
ghostmansdwe have these records:21:34
ghostmansd* grev RT, RA, RB (Rc=0)21:34
ghostmansd* grevi RT, RA, XBI (Rc=0)21:35
lkcland then there is DecodeFields which, in combination with the XYZ-Form, gives you the RB and the XBI etc.21:35
lkcl(in MSB0 order, as a SelectableInt)21:35
ghostmansdAh, OK, maybe at that level we can...21:36
ghostmansdI've been mostly looking at svp64.py21:36
ghostmansdWhere we simply do shifts and masks :-)21:36
ghostmansd(not to mention we do it in somewhat strange ways, but hey)21:36
ghostmansdOK, I'll dig more into it, sure21:37
ghostmansdthanks for tip!21:37
lkclISACaller uses them automatically21:37
lkclformname: XXX-Form (from the markdown file)21:38
ghostmansdhm, after thinking about it... is `* grev RT, RA, RB (Rc=0)` record even correct?21:38
ghostmansdI mean, shouldn't it be `* grev RT, RA, UI (Rc=0)`21:38
lkclop_fields: also from the markdown file (opname RT, RA, RB)21:39
ghostmansdthe difference between 64 and 32 drives me crazy21:39
lkclyou're thinking of grevi if you're using "UI"21:41
ghostmansdhey, the page tells that grev is supercedet21:41
ghostmansdbut I don't even see grevlut in openpower-isa21:41
lkclyes, i know21:41
ghostmansdkinda confusing, eh?21:41
lkclit's under discussion21:41
ghostmansdaaaah ok then21:42
ghostmansdok, it clarifies things21:42
lkcli want grev* gone and replaced with grevlut because it's way more powerful and the immediate version, grevluti, can create around a thousand patterned constants in a single 32-bit instruction21:42
lkcl0x5555555, 0xaaaaaa, 0x55aa55aa55aa21:43
lkcl0x11111 0x22222 0x101010101 0x100010001000100021:43
lkcltons more21:43
ghostmansdOK, I'll take a look at it with a fresh head21:44
lkcl*and* it can do grev, gorc, and a ton more operations like gxorc, gnandc, etc. etc.21:44
lkclbut it's... expensive21:44
ghostmansdit's almost midnight here :-)21:44
lkclhow expensive we don't know yet21:44
lkclok yeah21:44
lkcl21:44 here i think21:44
ghostmansdif you have stuff to add, please post here21:44
ghostmansdbecause I'm going to read it anyway, just not today :-)21:45
lkclwilldo. not tonight21:45
ghostmansdack :-)21:45
ghostmansdok bb!21:45

Generated by 2.17.1 by Marius Gedminas - find it at!