| lkcl | what's cvc5? | 00:04 |
|---|---|---|
| lkcl | https://smtlib.cs.uiowa.edu/logics.shtml | 00:04 |
| lkcl | i tried yices-smt2 that was missing "(set-logic XXX)" | 00:04 |
| * lkcl found it | 00:04 | |
| lkcl | so 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 on | 00:06 | |
| programmerjake | the 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 has | 00:07 |
| programmerjake | basically 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 declared | 00:11 |
| lkcl | ah set-logic ALL should do it | 00:11 |
| lkcl | nope. | 00:12 |
| lkcl | still Float32 missing from yices2 | 00:12 |
| lkcl | although it stopped the complaints "BitVec undefined" on the (define-sort) | 00:12 |
| programmerjake | yices2 may not support smtlib2 fp... | 00:13 |
| lkcl | bleh | 00:15 |
| programmerjake | no fp support: https://github.com/SRI-CSL/yices2/search?q=float32&type= | 00:16 |
| lkcl | meh | 00:22 |
| lkcl | can i suggest adding an fp16 version of fpmul? | 00:22 |
| lkcl | and doing an fpadd | 00:22 |
| lkcl | just to see what happens on the completion time? | 00:22 |
| lkcl | going straight to "most complex and not completing" gives no sense of scale | 00:23 |
| lkcl | or, heck, even fp8 | 00:24 |
| programmerjake | fp16 fmul should be relatively easy, fadd is much harder to implement since you have to handle huge+tiny cases | 00:24 |
| lkcl | (which the AI team in India want to do) | 00:24 |
| programmerjake | f8 is small enough i'd probably just use exhaustive checking and not bother with smt | 00:24 |
| programmerjake | maybe | 00:25 |
| lkcl | it's still a good base for "if smt2 goes into brute-force at least it'll complete" | 00:25 |
| programmerjake | but we want to prove f64 code...if it has to use brute-force it fails | 00:26 |
| lkcl | the point of using correctness proofs on the smaller FP types is that the ieee754fp code is identical except for the parameterised mantissa/exponent | 11:26 |
| lkcl | with the exception that the number of stages chained together will vary, there's no difference - at all | 11:27 |
| lkcl | thus a proof at FP8, FP16 and BF16 does actually give us a confidence level at FP32, FP64 and even FP128 | 11:27 |
| *** littlebo1eep is now known as littlebobeep | 12:27 | |
| ghostmansd | * fneg FRT,FRB (Rc=0) | 12:29 |
| ghostmansd | * fneg. FRT,FRB (Rc=0) | 12:29 |
| ghostmansd | Shouldn't fneg. have Rc=1? | 12:29 |
| ghostmansd | I see several such records, it was my understanding that these opcodes differ by Rc only, being identical otherwise | 12:30 |
| lkcl | no not a bug in v3.0 spec, it'll be a cut/paste error somewhere | 13:17 |
| lkcl | ghostmansd, sorted | 13:18 |
| lkcl | thx | 13:18 |
| ghostmansd | lkcl, star | 13:19 |
| lkcl | found some more with a grep | 13:20 |
| ghostmansd | I suggest we add fsins/fcoss/ternlogi/grev* as standalone patch, outside of SVP64. Any objections? | 13:43 |
| ghostmansd | These will be available under -mfuture switch. | 13:43 |
| ghostmansd | I 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 |
| ghostmansd | Also, it'd be great if I had any pointers to the corresponding discussions with OpenPOWER Foundation. | 13:59 |
| tplaten | I tried to build https://git.libre-soc.org/?p=mesa.git;a=shortlog;h=refs/heads/libresoc_dev on my Talos II, it was unable to find some llvm headers | 14:31 |
| tplaten | ../src/libre-soc/vulkan/libresoc_llvm.h:5:10: fatal error: llvm-c/OrcBindings.h: No such file or directory | 14:31 |
| tplaten | my headers are in /usr/include/llvm-c-11/llvm-c/OrcBindings.h | 14:31 |
| lkcl | ghostmansd, no perfectly good idea, actually kinda important [to do as separate patch] | 15:44 |
| lkcl | [and associated bugreport] [and associated budget] | 15:44 |
| lkcl | the OPF email was a private one to the Board of Directors | 15:45 |
| ghostmansd | > the OPF email was a private | 16:09 |
| ghostmansd | Ah, OK, I thought there was some discussion publicly available, nevermind then. Just ping me when/if the opcodes are changed. | 16:09 |
| ghostmansd | What'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 |
| ghostmansd | Raised #834 | 16:56 |
| ghostmansd | Hell 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 |
| lkcl | EUR 500 sounds fine | 17:30 |
| lkcl | i sort-of summarised on binutils-dev | 17:31 |
| lkcl | i knew you could do 0xffff_8000_0000 | 17:32 |
| lkcl | it kinda makes sense that 0bnnn_nnn_nnn would also work | 17:32 |
| lkcl | converting to a dynamic-loadable-module system would be a separate bugreport btw | 17:37 |
| lkcl | dlopen / dlsym is really straightforward, i don't know if you've ever done it before? | 17:37 |
| lkcl | you 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 |
| tplaten | Still 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 |
| tplaten | ERROR: PIO 'X0/Y53/PIOB' does not appear to be a DQS site (expecting an 'A' pin). | 19:04 |
| tplaten | Only one of those four pins is an 'A' pin. | 19:04 |
| tplaten | When 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 |
| ghostmansd | Which is simpler to you? | 20:30 |
| ghostmansd | a) https://pastebin.com/yPGbzyMa | 20:30 |
| ghostmansd | b) https://pastebin.com/hVyTZ6Rv | 20:30 |
| ghostmansd | To me, the answer is obviously a) | 20:30 |
| ghostmansd | Because it's really obvious where each bit goes | 20:30 |
| ghostmansd | https://pastebin.com/By6cuFUL | 20:32 |
| ghostmansd | Is the whole `(instr << 6) vs (instr << 5)` debate caused by "64 takes 1 more bit"? Is it a right guess? | 20:33 |
| ghostmansd | Frankly, 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!~kvirc@broadband-188-32-220-29.ip.moscow.rt.ru> has left #libre-soc | 20:35 | |
| lkcl | ghostmansd[m], just planned: i'm anticipating the OPF to come back with "hmm" on adding non-approved instructions, upstream | 20:58 |
| lkcl | (a) | 21:01 |
| lkcl | (b) was written by programmerjake and he didn't follow the conventions set by other instructions | 21:01 |
| lkcl | where, yes, i very deliberately put the MSB0 numbering into the source code so that it could be compared against the spec | 21:02 |
| lkcl | and jacob hasn't done that, meaning that it will be harder to review | 21:02 |
| lkcl | and is unnecessarily more lines of code | 21:03 |
| lkcl | and doesn't contain comments | 21:03 |
| lkcl | programmerjake, can you please correct all those? | 21:03 |
| lkcl | fields are already ints, they do not need conversion to int | 21:03 |
| lkcl | constructing by shifting-then-shifting is not appropriate | 21:04 |
| lkcl | storage of fields[n] in a temporary variable as a means to avoid use of comments is not appropriate | 21:04 |
| lkcl | also can you add the relevant section cut/paste from fields.txt (i started doing that only a couple days ago) | 21:06 |
| lkcl | also please use yield ".long 0x%x" % insn | 21:06 |
| lkcl | the f"" format just pisses me off, it's the PHP nightmare all over again | 21:07 |
| lkcl | also, 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 | sorry | 21:09 |
| lkcl | yes | 21:10 |
| lkcl | ".long %x # %s" % (instr, insn) | 21:10 |
| lkcl | should reduce down by over 50% without the nonsense | 21:10 |
| ghostmansd | well, I have nothing against f strings, they simplify reading quite a lot, if used correctly | 21:11 |
| ghostmansd | actually the only thing which pisses me off is shifting | 21:11 |
| ghostmansd | because it's not explicit | 21:11 |
| ghostmansd | anyway, I already deduced how it works, it simply took more time I wanted :-) | 21:11 |
| lkcl | ghostmansd, exactly. non-standard, non-obvious convention, it wasted your time | 21:12 |
| ghostmansd | I can fix these, but perhaps it'd be better for programmerjake to take handle it, since he's the code owner | 21:13 |
| lkcl | the fact that you're forced to run functions *inside the string* if you want hex or other format is the nightmare of PHP | 21:13 |
| ghostmansd | cool, eh? https://pastebin.com/e0TUa9nE | 21:14 |
| * lkcl waits 15 seconds for DNS resolution at this end... | 21:14 | |
| lkcl | ooo prettyyy | 21:14 |
| ghostmansd | yeah, the more I dig this code the more I like it | 21:15 |
| ghostmansd | and, btw | 21:15 |
| ghostmansd | UIMM and UIM6 are already for granted | 21:15 |
| ghostmansd | as well as the rest of operands, obviously | 21:15 |
| ghostmansd | so cute | 21:15 |
| lkcl | what did you think of the idea of having the #defines (matching already-named fields) explicitly listed in sv_binutils.py? | 21:16 |
| lkcl | (perhaps even still auto-generate the template, but comment it out just like in opc-ppc.c) | 21:17 |
| lkcl | it'd avoid you having to parse opc-ppc.c | 21:17 |
| ghostmansd | This has one issue that we still can miss something updated in vanilla... | 21:18 |
| ghostmansd | I've been thinking, you know, perhaps a big regex?... | 21:18 |
| ghostmansd | Because name of that table won't change, it's exported stuff. | 21:19 |
| ghostmansd | But, 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-crap | 21:20 |
| ghostmansd | I haven't really given this topic a proper thought yet, TBH | 21:20 |
| ghostmansd | But for sure will, because I want to make as much automatically as possible | 21:20 |
| lkcl | ack | 21:23 |
| lkcl | btw i have a strange form of dyslexia which means regex's are pretty much unintelligable for me. | 21:24 |
| ghostmansd | here, perhaps, not even regex needed | 21:24 |
| ghostmansd | I mean, the name of this damned array is the same | 21:24 |
| ghostmansd | and C decl is the same always | 21:24 |
| lkcl | i can read the symbols fine, there's no "disordering" going on as with normal dyslexia. | 21:25 |
| ghostmansd | the only tricky part here are these `#define CRAP OTHER_CRAP + 1` macros | 21:25 |
| ghostmansd | they're virtually throughout the whole declaration set of this array | 21:26 |
| ghostmansd | and the parser, if we implement it, must keep track of these | 21:26 |
| ghostmansd | not unsolvable, but too much work for such a little shitty task | 21:27 |
| ghostmansd | so, any ideas are highly appreciated :-) | 21:27 |
| ghostmansd | I'd only like to ensure that we never ever miss a single #define in vanilla binutils | 21:27 |
| lkcl | yes, my idea was - to reiterate: don't bother parsing | 21:28 |
| lkcl | just have an explicit declartion "if encounter field named X then output #define X Y" | 21:28 |
| lkcl | straight dictionary. | 21:28 |
| lkcl | dead simple | 21:28 |
| ghostmansd | you mean, generate the whole set of fields for PPC? | 21:28 |
| lkcl | no, just have "those which are #defined" | 21:29 |
| ghostmansd | but names are not yet all | 21:29 |
| lkcl | a dictionary which if there is an entry you literally do print("#define %s %s\n" % (x_field, thedictionary[x_field]) | 21:29 |
| ghostmansd | e.g. let's consider https://pastebin.com/e0TUa9nE | 21:30 |
| ghostmansd | take a look at grev insn | 21:30 |
| lkcl | you'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 |
| ghostmansd | yeah | 21:31 |
| lkcl | well then have a dictionary with "{insert_name_of_new_field}" : "{insert_#define_name_of_original|}" | 21:31 |
| lkcl | done | 21:31 |
| lkcl | no pissing about | 21:31 |
| ghostmansd | not always simple :-) | 21:32 |
| ghostmansd | again, about grev | 21:32 |
| * lkcl paying attention | 21:32 | |
| ghostmansd | you see, the difference between grev/grevi is how they handle the immediates... | 21:33 |
| ghostmansd | or, well, how many bits do they allow for an immediate | 21:33 |
| lkcl | yes | 21:33 |
| ghostmansd | 5 or 6 | 21:33 |
| ghostmansd | and, well, binutils do allow to handle this... | 21:34 |
| ghostmansd | but, if we operate on our level, in python... | 21:34 |
| ghostmansd | we have these records: | 21:34 |
| ghostmansd | * grev RT, RA, RB (Rc=0) | 21:34 |
| ghostmansd | * grevi RT, RA, XBI (Rc=0) | 21:35 |
| lkcl | and 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 |
| ghostmansd | Ah, OK, maybe at that level we can... | 21:36 |
| ghostmansd | I've been mostly looking at svp64.py | 21:36 |
| ghostmansd | Where we simply do shifts and masks :-) | 21:36 |
| ghostmansd | (not to mention we do it in somewhat strange ways, but hey) | 21:36 |
| lkcl | uh-huhn | 21:37 |
| ghostmansd | OK, I'll dig more into it, sure | 21:37 |
| ghostmansd | thanks for tip! | 21:37 |
| lkcl | ISACaller uses them automatically | 21:37 |
| lkcl | https://git.libre-soc.org/?p=openpower-isa.git;a=blob;f=src/openpower/decoder/isa/caller.py;hb=HEAD#l786 | 21:38 |
| lkcl | formname: XXX-Form (from the markdown file) | 21:38 |
| ghostmansd | hm, after thinking about it... is `* grev RT, RA, RB (Rc=0)` record even correct? | 21:38 |
| ghostmansd | I mean, shouldn't it be `* grev RT, RA, UI (Rc=0)` | 21:38 |
| lkcl | op_fields: also from the markdown file (opname RT, RA, RB) | 21:39 |
| ghostmansd | the | 21:39 |
| ghostmansd | the difference between 64 and 32 drives me crazy | 21:39 |
| lkcl | https://libre-soc.org/openpower/sv/bitmanip/#index10h1 | 21:39 |
| lkcl | you're thinking of grevi if you're using "UI" | 21:41 |
| ghostmansd | hey, the page tells that grev is supercedet | 21:41 |
| ghostmansd | but I don't even see grevlut in openpower-isa | 21:41 |
| lkcl | yes, i know | 21:41 |
| ghostmansd | kinda confusing, eh? | 21:41 |
| lkcl | it's under discussion | 21:41 |
| ghostmansd | aaaah ok then | 21:42 |
| ghostmansd | ok, it clarifies things | 21:42 |
| lkcl | i 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 instruction | 21:42 |
| lkcl | 0x5555555, 0xaaaaaa, 0x55aa55aa55aa | 21:43 |
| lkcl | 0x11111 0x22222 0x101010101 0x1000100010001000 | 21:43 |
| lkcl | tons more | 21:43 |
| ghostmansd | OK, I'll take a look at it with a fresh head | 21:44 |
| lkcl | *and* it can do grev, gorc, and a ton more operations like gxorc, gnandc, etc. etc. | 21:44 |
| lkcl | ack | 21:44 |
| lkcl | but it's... expensive | 21:44 |
| ghostmansd | it's almost midnight here :-) | 21:44 |
| lkcl | how expensive we don't know yet | 21:44 |
| lkcl | ok yeah | 21:44 |
| lkcl | 21:44 here i think | 21:44 |
| ghostmansd | if you have stuff to add, please post here | 21:44 |
| ghostmansd | because I'm going to read it anyway, just not today :-) | 21:45 |
| lkcl | willdo. not tonight | 21:45 |
| lkcl | :) | 21:45 |
| ghostmansd | ack :-) | 21:45 |
| ghostmansd | ok bb! | 21:45 |
| ghostmansd | ttyl | 21:45 |
Generated by irclog2html.py 2.17.1 by Marius Gedminas - find it at https://mg.pov.lt/irclog2html/!